// -----------------------------------------------------------------
// Elevator algorithm
// https://www.popularmechanics.com/technology/infrastructure/a20986/the-hidden-science-of-elevators/
// https://en.wikipedia.org/wiki/Elevator_algorithm
// -----------------------------------------------------------------

val E:ℕ; // maximum elevator number (0..E)
val F:ℕ; // maximum floor number (0..F)

type Elevator = ℕ[E];
type Floor = ℕ[F];
type Direction = ℕ[2]; 

val none = 0; val up = 1; val down = 2;

shared system Elevator
{
  // ---------------------------------------------------------------------------
  // the system state
  // ---------------------------------------------------------------------------

  // call buttons for up/down pressed on floors
  var call: Map[Floor,Set[Direction]] = Map[Floor,Set[Direction]](∅[Direction]);
  
  // buttons for floors pressed in elevators
  var button: Map[Elevator,Set[Floor]] = Map[Elevator,Set[Floor]](∅[Floor]);
  
  // in which direction is the elevator to move?
  var direction: Map[Elevator,Direction] = Map[Elevator,Direction](none);
  
  // is the motor of the elvator on?
  var motor: Map[Elevator,Bool] = Map[Elevator,Bool](⊥);
  
  // is the door of the elevator open?
  var door: Map[Elevator,Bool] = Map[Elevator,Bool](⊥);

  // where is the elevator?
  var floor: Map[Elevator,Floor] = Map[Elevator,Floor](0);
  
  // ---------------------------------------------------------------------------
  // the safety properties
  // ---------------------------------------------------------------------------
  
  // no elevator moves with an open door
  invariant ∀e:Elevator. motor[e] ⇒ ¬door[e];

  // print some/every run leading to a situation where all elevators are at the top floor and have their doors opened
  // invariant (∀e:Elevator. floor[e] = F ∧ door[e]) ⇒ printtrace in false; // "true" for printing every run
  
  // ---------------------------------------------------------------------------
  // the system actions (add guard conditions here)
  // ---------------------------------------------------------------------------
  
  // elevator e opens its door
  action DoorOpen(e:Elevator) with ¬door[e] ∧
    true
  ;
  {
    door[e] ≔ true;
  } 
  
  // elevator e closes its door
  action DoorClose(e:Elevator) with door[e] ∧
    true
  ;
  {
    door[e] ≔ false;
  } 
  
  // system resets call button (button ligth turns off)
  action CallOff(f:Floor,d:Direction) with d ≠ none ∧ d ∈ call[f] ∧
    true
  ;
  { call[f] ≔ call[f]\{d}; }
  
  // elevator e resets button for floor f (button light turns off)
  action ButtonOff(e:Elevator,f:Floor) with f ∈ button[e] ∧
    true
  ;
  { button[e] ≔ button[e]\{f}; }
  
  // elevator e switches motor on
  action MotorOn(e:Elevator) with ¬motor[e] ∧
    true
  ;
  { motor[e] ≔ true; }
  
  // elevator e switches motor off
  action MotorOff(e:Elevator) with motor[e] ∧
    true
  ;
  { motor[e] ≔ false; }
  
  // elevator e moves one floor up
  action Up(e:Elevator) with floor[e] < F ∧
    true
  ;
  { floor[e] ≔ floor[e]+1; }
  
  // elevator e moves one floor down 
  action Down(e:Elevator) with floor[e] > 0 ∧
    true
  ;
  { floor[e] ≔ floor[e]-1; }

  // elevator e sets its direction to d
  action Direction(e:Elevator,d:Direction) with d ≠ direction[e] ∧
    true  
  ;
  { direction[e] ≔ d; }
  
  // ---------------------------------------------------------------------------
  // the user actions (nothing to change here)
  // ---------------------------------------------------------------------------
  
  // user presses on floor f call button for direction d (button light turns on)
  action CallOn(f:Floor,d:Direction) with d ≠ none ∧ d ∉ call[f] ∧ (f = 0 ⇒ d ≠ down) ∧ (f = F ⇒ d ≠ up);
  { call[f] ≔ call[f] ∪ {d}; }
  
  // user presses in elevator e button for floor f (button light turns on)
  action ButtonOn(e:Elevator,f:Floor) with f ∉ button[e] ;
  { button[e] ≔ button[e] ∪ {f}; }
}