Анализатор сплавов не предоставляет экземпляр

Question

Я пытаюсь сделать модель светофора в сплаве. Проблема в том, что я не очень хорошо это понимаю. Я читал пример светофора, найденный с помощью анализатора, но по какой-то причине он не дает мне никаких примеров. Это пример кода.

`module chapter4/lights ----- The model from page 127 

abstract sig Color {} 

one sig Red, Yellow, Green extends Color {} 

sig Light {} 
sig LightState {color: Light -> one Color} 
sig Junction {lights: set Light} 

fun redLights [s: LightState]: set Light { s.color.Red } 
fun colorSequence: Color -> Color { 
Color <: iden + Red->Green + Green->Yellow + Yellow->Red 
} 

pred mostlyRed [s: LightState, j: Junction] { 
lone j.lights - redLights[s] 
} 

pred trans [s, s': LightState, j: Junction] { 
lone x: j.lights | s.color[x] != s'.color[x] 
all x: j.lights | 
    let step = s.color[x] -> s'.color[x] { 
     step in colorSequence 
     step in Red->(Color-Red) => j.lights in redLights[s] 
    } 
} 

assert Safe { 
all s, s': LightState, j: Junction | 
    mostlyRed [s, j] and trans [s, s', j] => mostlyRed [s', j] 
} 

check Safe for 3 but 1 Junction` 

Если кто-то может объяснить это, я был бы очень признателен.

Answer 1

Чтобы увидеть экземпляр, вам необходимо включить команду run. Единственная команда, которую вы здесь имеете, - это команда проверки, и если проверенное свойство имеет значение true, контрпример не будет найден.