Traffic light simulator where dangerous states are ruled out by typing.
DoneSprint S9+S35 · 8 points
In short, no jargonfor non-developersRead the summaryClose
What it is
A crossroads with traffic lights, which you operate on the page, whose program makes an accident impossible: two roads can never be green at the same time.
What it is for
This is the method of software where a mistake is costly: aviation, railways, medicine.
What it shows
Safe programming, and the mathematical proof that a program cannot go wrong, in the Ada language.
The Ada program computed every state its controller can reach, and what a second or a crossing request changes in it. This page only follows those transitions: ask to cross on one axis and watch the other's green get shorter, never below 10 seconds, without the two axes ever open at once.
Timing diagram of the last 60 seconds
30 s of green north-south and 20 s east-west, 3 s of amber, 2 s of all red, as in the program's simulation. Typing, contracts and the SPARK proof guarantee the rest (see the README).
Tech stack
Ada
SPARK
GNAT
AUnit
Alire
Who does what
Ada
The traffic light controller: phases are an enumerated type, so a "both axes green" state cannot be written; the program also exports the automaton the project page replays.
SPARK
Proves the absence of run-time errors, the contracts, and that at least one axis is always red.
GNAT
The Ada compiler, warnings treated as errors, on Linux, Windows and macOS.
AUnit
The tests: full cycle, crossing requests, out-of-range durations refused, the project page's automaton safe.
Alire
Installs the same GNAT toolchain and dependencies (AUnit, gnatprove), locally and in CI.
Definition of Done
Code reviewed, diff by diff
Unit and integration tests green
Green CI on Linux, Windows and macOS when compiled