module elevator
open util/ordering[Floor] as floors
open util/ordering[System] as systems

//Possible movement directions (two)
abstract sig Move { }
one sig Up, Down extends Move { }

//Floors
sig Floor { }

//Elevator system states
sig System {
  curFloor: Floor,
  curDirection: Move,
  intRequests: set Floor,
  extRequests: Floor -> Move,
  destFloor: lone Floor
}
{
  //Representation invariant	
  Down !in extRequests[floors/first[]]
  Up !in extRequests[floors/last[]]

  //Scheduler outcome
  destFloor = theDestFloor[curDirection, curFloor, intRequests, extRequests]
}

//Definition of the scheduler

fun priTopUp[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | floors/gte[f, curFloor] && (f in intRequest || Up in extRequest[f]) }
}

fun priMidUp[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | (floors/lt[f, curFloor] && f in intRequest) || Down in extRequest[f] }
}

fun priLowUp[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | floors/lt[f, curFloor] && Up in extRequest[f] }
}

fun priTopDown[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | floors/lte[f, curFloor] && (f in intRequest || Down in extRequest[f]) }
}

fun priMidDown[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | (floors/gt[f, curFloor] && f in intRequest) || Up in extRequest[f] }
}

fun priLowDown[curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: set Floor {
  { f: Floor | floors/gt[f, curFloor] && Down in extRequest[f] }
}

pred minFloor[f: Floor, fs: set Floor] {
  f in fs && (no f': Floor | f' in fs && floors/lt[f', f])
}

pred maxFloor[f: Floor, fs: set Floor] {
  f in fs && (no f': Floor | f' in fs && floors/lt[f, f'])
}

pred isTheDestFloor[destFloor: lone Floor, curDirection: Move, curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move] {
  curDirection = Up => (
    (some priTopUp[curFloor, intRequest, extRequest] && some destFloor && minFloor[destFloor, priTopUp[curFloor, intRequest, extRequest]]) ||
    (no priTopUp[curFloor, intRequest, extRequest] && some priMidUp[curFloor, intRequest, extRequest] && some destFloor && maxFloor[destFloor, priMidUp[curFloor, intRequest, extRequest]]) ||
    (no priTopUp[curFloor, intRequest, extRequest] && no priMidUp[curFloor, intRequest, extRequest] && some priLowUp[curFloor, intRequest, extRequest] && some destFloor && minFloor[destFloor, priLowUp[curFloor, intRequest, extRequest]]) ||
    (no priTopUp[curFloor, intRequest, extRequest] && no priMidUp[curFloor, intRequest, extRequest] && no priLowUp[curFloor, intRequest, extRequest] && no destFloor)
  )
  curDirection = Down => (
    (some priTopDown[curFloor, intRequest, extRequest] && some destFloor && maxFloor[destFloor, priTopDown[curFloor, intRequest, extRequest]]) ||
    (no priTopDown[curFloor, intRequest, extRequest] && some priMidDown[curFloor, intRequest, extRequest] && some destFloor && minFloor[destFloor, priMidDown[curFloor, intRequest, extRequest]]) ||
    (no priTopDown[curFloor, intRequest, extRequest] && no priMidDown[curFloor, intRequest, extRequest] && some priLowDown[curFloor, intRequest, extRequest] && some destFloor && maxFloor[destFloor, priLowDown[curFloor, intRequest, extRequest]]) ||
    (no priTopDown[curFloor, intRequest, extRequest] && no priMidDown[curFloor, intRequest, extRequest] && no priLowDown[curFloor, intRequest, extRequest] && no destFloor)
  )
}

fun theDestFloor[curDirection: Move, curFloor: Floor, intRequest: set Floor, extRequest: Floor -> Move]: lone Floor {
  { destFloor: Floor | isTheDestFloor[destFloor, curDirection, curFloor, intRequest, extRequest] }
}

//Ausiliary functions for hypothetical direction calculation

fun hypotheticalDest[s: System]: lone Floor {
  theDestFloor[s.curDirection, s.curFloor, s.intRequests, s.extRequests - (s.curFloor -> Move)]
}

fun hypotheticalDir[s: System]: lone Move {
  some hypotheticalDest[s] => (
    floors/lt[s.curFloor, hypotheticalDest[s]] =>
      Up
    else
      Down)
  else
    none
}

//Actions

//Someone pushes a cabin button
pred InternalPush[s, s': System, f: Floor] {
  //Precondition
  f !in s.intRequests //no stutter

  //Postcondition
  s'.curFloor = s.curFloor
  s'.curDirection = s.curDirection
  s'.intRequests = s.intRequests + f
  s'.extRequests = s.extRequests
   //No postcondition for destFloor (determined by the scheduler)
}

//Someone pushes a floor button
pred ExternalPush[s, s': System, f: Floor, m: Move] {
  //Precondition
  f -> m !in s.extRequests //no stutter

  //Postcondition
  s'.curFloor = s.curFloor
  s'.curDirection = s.curDirection
  s'.intRequests = s.intRequests
  s'.extRequests = s.extRequests + (f -> m)
  //No postcondition for destFloor (determined by the scheduler)
}

//Spontaneous move to the next floor
pred MoveToNextFloor[s, s': System] {
  //Precondition
  some s.destFloor
  s.curFloor != s.destFloor

  //Postcondition
  floors/lt[s.destFloor, s.curFloor] =>
    (s'.curFloor = floors/prev[s.curFloor] && s'.curDirection = Down) 
    else
    (s'.curFloor = floors/next[s.curFloor] && s'.curDirection = Up)
  s'.intRequests = s.intRequests
  s'.extRequests = s.extRequests
}

//Spontaneous move to serve an internal request after halting at destination floor
pred ServeIntRequest[s, s': System] {
  //Precondition
  s.curFloor = s.destFloor
  s.curFloor in s.intRequests

  //Postcondition
  s'.curFloor = s.curFloor
  s'.curDirection = s.curDirection
  s'.intRequests = s.intRequests - s.curFloor
  s'.extRequests = s.extRequests
}

//Spontaneous move to serve an internal request in the hypothetical next direction if still at destination floor after ServeIntRequest
pred ServeExtRequestHypotheticalDir[s, s': System] {
  //Precondition
  s.curFloor = s.destFloor
  s.curFloor !in s.intRequests //already served internal request
  some hypotheticalDir[s]
  hypotheticalDir[s] in s.extRequests[s.curFloor]

  //Postcondition
  s'.curFloor = s.curFloor
  s'.curDirection = s.curDirection
  s'.intRequests = s.intRequests
  s'.extRequests = s.extRequests - (s.curFloor -> hypotheticalDir[s])
}

//Spontaneous move to eliminate the residual internal request if still at destination floor after ServeExtRequestHypotheticalDir
pred ServeExtRequestStuck[s, s': System] {
  //Precondition
  s.curFloor = s.destFloor
  s.curFloor !in s.intRequests //already served internal request
  no hypotheticalDir[s] || hypotheticalDir[s] !in s.extRequests[s.curFloor] //already served external request in the hypothetical direction

  //Postcondition
  s'.curFloor = s.curFloor
  s'.curDirection = s.curDirection
  s'.intRequests = s.intRequests
  s'.extRequests = s.extRequests - (s.curFloor ->Move)
}

//Initial system condition
pred Init[s: System] {
  //Postcondition
  s.curFloor = floors/first[]
  s.curDirection = Up
  no s.intRequests
  no s.extRequests
  no s.destFloor
}

//Predicates used by assertions
pred Step[s, s': System] {
    ( some f: Floor | InternalPush[s, s', f] ) ||
    ( some f: Floor, m: Move | ExternalPush[s, s', f, m] ) ||
    MoveToNextFloor[s, s'] ||
    ServeIntRequest[s, s'] ||
    ServeExtRequestHypotheticalDir[s, s'] ||
    ServeExtRequestStuck[s, s']
}

//A computation starting from an arbitrary state
pred ComputeFromAny[] {
  all s, s': System | s' = systems/next[s] => Step[s, s']
}

//An unconstrained computation
pred Compute[] {
  Init[systems/first[]]
  ComputeFromAny[]
}

//A computation without additional requests
pred ComputeFromAnyNoReq[] {
  ComputeFromAny[]

  //No additional requests
  all s, s': System | s' = systems/next[s] =>
    no f: Floor, m: Move | 
    ( InternalPush[s, s', f] || ExternalPush[s, s', f, m] )
}

//Requirements, static
pred Consistent[] { }
systemIsConsistent: run Consistent for 5 Floor, exactly 1 System

assert DestIsRequested {
  all s: System | s.destFloor in (s.intRequests + s.extRequests.Move)
}
destIsRequested: check DestIsRequested for 5 Floor, exactly 1 System

assert NoDestImpliesNoRequest {
  all s: System | no s.destFloor => (no s.intRequests && no s.extRequests)
}
noDestImpliesNoRequest: check NoDestImpliesNoRequest for 5 Floor, exactly 1 System

assert SchedulerIsDeterministic {
  all s1, s2: System | (disj[s1, s2] && s1.curFloor = s2.curFloor && s1.curDirection = s2.curDirection && s1.intRequests = s2.intRequests && s1.extRequests = s2.extRequests) => (s1.destFloor = s2.destFloor)
}
schedulerIsDeterministic: check SchedulerIsDeterministic for 5 Floor, exactly 2 System

//Requirements, dynamic
systemHasComputations: run Compute for 5 Floor, exactly 11 System

assert ReqStaysScheduledUntilServed { 
  ComputeFromAnyNoReq[] => (some s1: System | s1.destFloor != systems/first[].destFloor && (all s2: systems/prevs[s1] | s1.destFloor = s2.destFloor))

}
reqStaysScheduledUntilServed: check ReqStaysScheduledUntilServed for exactly 5 Floor, 15 System

assert NotStuckAtDestFloor {
  ComputeFromAny[] && systems/first[].curFloor = systems/first[].destFloor && some (systems/first[].intRequests + systems/first[].extRequests.Move) - systems/first[].curFloor => some s: systems/nexts[systems/first[]] | s.destFloor != systems/first[].destFloor
}
notStuckAtDestFloor: check NotStuckAtDestFloor for exactly 3 Floor, 10 System