module language/lights
sig Colour {}
one sig Red, Yellow, Green extends Colour {}
fun colourSequence (): Colour -> Colour {
	Colour <: iden + Red->Green + Green->Yellow + Yellow->Red
	}

sig Light {}
sig LightState {colour: Light -> one Colour}
sig Junction {lights: set Light}
 
fun redLights (s: LightState): set Light {s.colour.Red}
pred mostlyRed (s: LightState, j: Junction) {
	lone j.lights - redLights(s)
	}

pred trans (s, s': LightState, j: Junction) {
	lone x: j.lights | s.colour[x] != s'.colour[x]
	all x: j.lights |
		let step = s.colour[x]-> s'.colour[x] {
			step in colourSequence ()
--			step in Red->(Colour-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

assert ColourSequenceDeterministic {
	all c: Colour | lone c.colourSequence ()
	}
check ColourSequenceDeterministic