Skip to content

Instantly share code, notes, and snippets.

@jmcph4

jmcph4/traffic.cfg

Created July 8, 2026 02:51
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jmcph4/035f33f35bf02f651425cb90dcf81d67 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jmcph4/035f33f35bf02f651425cb90dcf81d67 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
traffic.cfg
INIT Init
NEXT Next
INVARIANT TypeOK
Raw
traffic.tla
--------------------------- MODULE TrafficLight -----------------------------
EXTENDS Naturals
VARIABLE light
TypeOK == light \in {"red", "green", "yellow"}
ToGreen == /\ light = "red"
/\ light' = "green"
ToYellow == /\ light = "green"
/\ light' = "yellow"
ToRed == /\ light = "yellow"
/\ light' = "red"
Init == light = "red"
Next == \/ ToGreen
\/ ToYellow
\/ ToRed
NeverSkipYellow == (light = "green") => (light' # "red")
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment