---------------------------- MODULE TrafficLight ----------------------------
(* A central controller commands a phase; N intersection lights follow it
   asynchronously. The controller's clock runs regardless, but it only
   advances once every light has caught up. Time is in abstract ticks.   *)
EXTENDS Naturals

CONSTANTS N, RedTicks, GreenTicks, YellowTicks

Intersections == 1..N
Phases == {"Red", "Green", "Yellow"}

NextPhase(p) == CASE p = "Red"    -> "Green"
                  [] p = "Green"  -> "Yellow"
                  [] p = "Yellow" -> "Red"

Duration(p) == CASE p = "Red"    -> RedTicks
                 [] p = "Green"  -> GreenTicks
                 [] p = "Yellow" -> YellowTicks

VARIABLES phase, timer, light
vars == <<phase, timer, light>>

TypeOK == /\ phase \in Phases
          /\ timer \in 0..(RedTicks + GreenTicks + YellowTicks)
          /\ light \in [Intersections -> Phases]

AllCaughtUp == \A i \in Intersections : light[i] = phase

Init == /\ phase = "Red"
        /\ timer = Duration("Red")
        /\ light = [i \in Intersections |-> "Red"]

Tick == /\ timer > 0
        /\ timer' = timer - 1
        /\ UNCHANGED <<phase, light>>

Advance == /\ timer = 0
           /\ AllCaughtUp
           /\ phase' = NextPhase(phase)
           /\ timer' = Duration(NextPhase(phase))
           /\ UNCHANGED light

Follow(i) == /\ light[i] # phase
             /\ light' = [light EXCEPT ![i] = phase]
             /\ UNCHANGED <<phase, timer>>

Next == Tick \/ Advance \/ \E i \in Intersections : Follow(i)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Every light shows the commanded phase or is exactly one step behind it.
InSynch == \A i \in Intersections : light[i] = phase \/ NextPhase(light[i]) = phase

\* No light goes straight from Green to Red.
NoGreenToRed == [][\A i \in Intersections :
                     light[i] = "Green" => light'[i] \in {"Green", "Yellow"}]_vars

\* Every light turns green infinitely often.
AlwaysEventuallyGreen == \A i \in Intersections : []<>(light[i] = "Green")
=============================================================================

-------------------------- MODULE PriorityProtocol --------------------------
EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS Nodes, Priorities, Cap, MsgIds
ASSUME Priorities \subseteq Nat /\ Cap \in Nat /\ Cap > 0

Range(s) == {s[i] : i \in DOMAIN s}

(* --algorithm PriorityProtocol
variables
  route \in [MsgIds -> [src : Nodes, dst : Nodes, pri : Priorities]],
  pending = MsgIds,
  buf = [n \in Nodes |-> [p \in Priorities |-> <<>>]],
  delivered = [n \in Nodes |-> <<>>],
  dropped = {};

define
  Buffered(n) == UNION {Range(buf[n][p]) : p \in Priorities}
  Top(n) == CHOOSE p \in Priorities :
              /\ buf[n][p] # <<>>
              /\ \A q \in Priorities : q < p => buf[n][q] = <<>>
  Busy(n) == \/ \E m \in pending : route[m].src = n \/ route[m].dst = n
             \/ Buffered(n) # {}
end define;

fair process node \in Nodes
begin
Loop:
  while Busy(self) do
    either
      with m \in {x \in pending : route[x].src = self} do
        pending := pending \ {m};
        if Len(buf[route[m].dst][route[m].pri]) < Cap then
          buf[route[m].dst][route[m].pri] :=
            Append(buf[route[m].dst][route[m].pri], m);
        else
          dropped := dropped \union {m};
        end if;
      end with;
    or
      await Buffered(self) # {};
      with p = Top(self) do
        delivered[self] := Append(delivered[self], Head(buf[self][p]));
        buf[self][p] := Tail(buf[self][p]);
      end with;
    end either;
  end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
\* END TRANSLATION

TypeOK == /\ pending \subseteq MsgIds
          /\ dropped \subseteq MsgIds
          /\ \A n \in Nodes : Range(delivered[n]) \subseteq MsgIds

BoundedBuffers == \A n \in Nodes, p \in Priorities : Len(buf[n][p]) <= Cap

\* Every message is in exactly one place: pending, buffered at its
\* destination, delivered at its destination, or dropped.
Conservation ==
  \A m \in MsgIds :
    LET d == route[m].dst IN
      (IF m \in pending THEN 1 ELSE 0)
    + (IF m \in Buffered(d) THEN 1 ELSE 0)
    + (IF m \in Range(delivered[d]) THEN 1 ELSE 0)
    + (IF m \in dropped THEN 1 ELSE 0) = 1

NoDuplicates == \A n \in Nodes : Len(delivered[n]) = Cardinality(Range(delivered[n]))

\* A delivery never skips over a more urgent buffered message.
PriorityRespected ==
  [][\A n \in Nodes :
       Len(delivered'[n]) > Len(delivered[n]) =>
         \A q \in Priorities :
           q < route[delivered'[n][Len(delivered'[n])]].pri => buf[n][q] = <<>>]_vars

\* Eventually nothing is pending or buffered: every message is delivered or dropped.
Settles == <>[](pending = {} /\ \A n \in Nodes : Buffered(n) = {})
=============================================================================