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

sig Street {}
sig Light {street: Street}
sig LightState {colour: Light -> one Colour}
	{all l, l': Light | l.street = l'.street => l.colour = l'.colour}
sig Junction {lights: set Light}
fact {lights: Junction lone -> 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 Red->(Colour-Red) => j.lights in redLights(s)
		}
	}

/*
pred traces () {
	all s: LightState - last () | all j: Junction | trans (s, next (s), j)
	}
run traces for exactly 2 Junction, exactly 2 Street, 3 Colour, 5 LightState, exactly 4 Light
*/

assert Safe {
	all s, s': LightState, j: Junction | 
		mostlyRed (s, j) and trans (s, s', j) => mostlyRed (s', j)
	}
check Safe for 3 but exactly 2 Junction, 2 Street

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