Alloy Analyzer not providing an instance

Question

I am trying to make a traffic light model in Alloy. The problem is that I don't really understand it well. I have been reading the traffic light example found with the analyzer, but for some reason it's not giving me any instance. This is the example code.

`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`

If someone can please explain this, I would really appreciate it.

Answer 1

To see an instance, you need to include a run command. The only command you have here is a check command, and if the property checked is true, no counterexample will be found.