-- Simple Murphi model of an intersection with a two-way stop.
-- Traffic in the north-south direction has precedence.
-- Traffic in the east-west direction must stop until the way is clear.
--
-- Ian Mitchell for CPSC 513, 9/30/05

Const
  carCount: 3;
  -- Really doesn't make a difference; 2+ cars will disprove invariant.
  
Type
  direction: enum { n, e, w, s };
  carStatus: enum { not_exist, approaching, deciding, waiting, crossing, gone};
  carID: 1..carCount;

  car: Record
    status: carStatus; -- Should always be defined.
    dir: direction;    -- May not be defined for status = not_exist.
  End;


Var
  cars: Array[carID] of car;


Function clearToProceed1(d: direction): Boolean;

  -- North-south direction has precedence.
  If (d = n | d = s) Then return True; End;

  -- East-west may not proceed if there are north-south cars nearby.
  If (d = e | d = w) Then
    return Forall c:carID Do
      cars[c].status = not_exist
      | cars[c].status = gone
      | !(cars[c].dir = n | cars[c].dir = s)
    End;
  End;

  -- Ensures that we covered all the cases.
  Error "Invalid Direction"
End;


Ruleset c:carID; d:direction Do

  -- Ensures that the cars arrive in sequential order (not really necessary).
  Rule "New car approaches."
    cars[c].status = not_exist
    & ((c = 1) | cars[c-1].status != not_exist)
  ==>
    cars[c].status := approaching;
    cars[c].dir := d;
  End;

  -- If the intersection needed to detect cars in advance,
  -- it could test against the approaching state.
  Rule "Car arrives at intersection."
    cars[c].status = approaching
    & cars[c].dir = d
  ==>
    cars[c].status := deciding;
  End;

  Rule "Car enters intersection."
    (cars[c].status = deciding
     | cars[c].status = waiting)
    & cars[c].dir = d
    & clearToProceed1(d) = True
  ==>
    cars[c].status := crossing;
  End;

  Rule "Car must wait."
    cars[c].status = deciding
    & cars[c].dir = d
    & clearToProceed1(d) = False
  ==>
    cars[c].status := waiting;
  End;

EndRuleset;


Ruleset c:carID Do

  -- Direction of car does not matter at this stage.
  Rule "Car clears intersection."
    cars[c].status = crossing
  ==>
    cars[c].status := gone;
  End;

EndRuleset;

Startstate
  -- No cars yet.
  For c:carID Do
    cars[c].status := not_exist;
    Undefine cars[c].dir;
  End;

EndStartstate;


Invariant "No Collision"
  Forall c1:carID; c2:carID Do
    (c1 = c2) 
    | (cars[c1].status != crossing) 
    | (cars[c2].status != crossing) 
    | ((cars[c1].dir = n | cars[c1].dir = s)
       & (cars[c2].dir = n | cars[c2].dir = s))
    | ((cars[c1].dir = e | cars[c1].dir = w)
       & (cars[c2].dir = e | cars[c2].dir = w))
  End;
