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

// E=2, F=3, N=6 generates 2 million traces in half a minute
val E:ℕ; // number of elevators
val F:ℕ; // number of floors
val N:ℕ; // number of execution steps
axiom notNull ⇔ E > 0 ∧ F > 0;

type Elevator = ℕ[E-1];
type Floor = ℕ[F-1];
type Direction = ℕ[2]; 
val none = 0; val up = 1; val down = 2;

type System = Record[
  call: Map[Direction,Set[Floor]],   // up/down-buttons pressed on floors
  button: Map[Elevator,Set[Floor]],  // floor-buttons pressed in elevators
  door:  Map[Elevator,Bool],         // is door of elevator open?
  floor: Map[Elevator,Floor],        // where is elevator?
  direction: Map[Elevator,Direction] // in which direction is it heading?
];

// the initial state
fun initial():System 
=
  ⟨
    call:Map[Direction,Set[Floor]](∅[Floor]),
    button:Map[Elevator,Set[Floor]](∅[Floor]),
    door: Map[Elevator,Bool](⊥),
    floor:Map[Elevator,Floor](0),
    direction:Map[Elevator,Floor](none)
  ⟩; 

// list elevator actions first to generate them early in executions
enumtype Action =
  Move(Elevator,Direction) | Door(Elevator,Bool) | 
  Call(Floor,Direction) | Button(Elevator,Floor)
;

// compute effect of action on system
fun execute(a:Action,s:System):System =
  match a with
  {
    Call(f:Floor,d:Direction) -> 
      // on floor 'f' button for direction 'd' is pressed
      // print "Call({1},{2})", f, d in
      s with .call = (s.call with [d] = s.call[d]∪{f});
    Button(e:Elevator,f:Floor) -> 
      // in elevator 'e' button for floor 'f' is pressed
      // print "Button({1},{2})", e, f in
      s with .button = (s.button with [e] = s.button[e]∪{f});
    Door(e:Elevator,door:Bool) ->
      // print "Door({1},{2})", e, door in
      if ¬door then
        // elevator 'e' closes door 
        s with .door = (s.door with [e] = door)
      else
        // elevator 'e' opens door and unlights the corresponding buttons
        let f = s.floor[e], d = s.direction[e] in
        let d0 = if d ≠ none then d else if f ∈ s.call[up] then up else down in
        s with .door = (s.door with [e] = door) 
          with .button = (s.button with [e] = s.button[e]\{f})
          with .call = (s.call with [d0] = s.call[d0]\{f});
    Move(e:Elevator,d:Direction) ->
      // elevator 'e' chooses direction 'd' and moves accordingly
      // print "Move({1},{2})", e, d in
      s with .direction = (s.direction with [e] = d)
        with .floor = (s.floor with [e] = 
          if d = up then s.floor[e]+1
          else if d = down then s.floor[e]-1
          else s.floor[e]);
  }
;
     
// is action a admissible in system?
pred admissible(a:Action,s:System) ⇔
  match a with
  {
    Call(f:Floor,d:Direction) -> 
      d ≠ none ∧ ⊤;
    Button(e:Elevator,f:Floor) -> 
      ⊤;
    Door(e:Elevator,door:Bool) ->
      ⊤;      
    Move(e:Elevator,d:Direction) -> 
      ⊤;
  }
;

// no elevator moves with an open door
pred safety(s:System, s0:System) ⇔
  ∀e:Elevator with (s.floor[e] ≠ s0.floor[e]).
    ¬(s.door[e] ∨ s0.door[e]);

// every elevator move makes progress towards some request
pred progress(s:System, s0:System) ⇔
  ∀e:Elevator with (s.floor[e] ≠ s0.floor[e]).
    ∃f:Floor with (f ∈ s.button[e] ∨ ∃d:Direction. f ∈ s.call[d]).
      (s.floor[e] > f ∧ s0.floor[e] < s.floor[e]) ∨
      (s.floor[e] < f ∧ s0.floor[e] > s.floor[e]);
 
// display an execution trace
proc display(trace:Array[N,Action],n:ℕ[N]): ()
{
  print "=== Start Run ===";
  for var i:ℕ[N] = 0; i < n; i ≔ i+1 do
  {
    match trace[i] with
    {
      Call(f:Floor,d:Direction) -> 
        print "Call({1},{2})", f, d;
      Button(e:Elevator,f:Floor) -> 
        print "Button({1},{2})", e, f;
      Door(e:Elevator,door:Bool) ->
        print "Door({1},{2})", e, door;
      Move(e:Elevator,d:Direction) -> 
        print "Move({1},{2})", e, d;
    }
  }
  print "=== End Run ===";
}

// execute N steps of the system
proc run(): Array[N,Action]
{
  val s0 = initial();
  var s:System ≔ s0;
  var trace:Array[N,Action] = Array[N,Action](Action!Call(0,none));
  for var i:ℕ[N] = 0; i < N; i ≔ i+1 do
  {
    choose a:Action with admissible(a,s);
    trace[i]:=a;
    val s1:System = execute(a,s);
    if ¬safety(s,s1) then 
    { display(trace,i+1); print s; print s1; assert ⊥; }
    if ¬progress(s,s1) then 
    { display(trace,i+1); print s; print s1; assert ⊥; }
    s := s1;
  }
  // display chosen run
  // display(trace,N);
  return trace;
}

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------