module vibha/elevator

sig Floor { floorNumber : Int,
                   AboveFloor : lone Floor,
                   LowerFloor: lone Floor}

sig HighestFloor extends Floor { }{ no AboveFloor}
sig LowestFloor extends Floor { }{no LowerFloor }

sig Direction { }
one sig Up extends Direction { }
one sig Down extends Direction  { }

sig Request { }

sig Lift {
      liftNumber : Int,
      currentFloor : Floor,
      directionOfMovement : Direction
}

sig RequestForFloor extends Request {
      requestedFloor : Floor, 
      lift : Lift
}

sig RequestForLift extends Request {
      requestedDirection : Direction,
      floor : Floor
}

sig ElevatorSystem {
      requestPool : set Request,
      lifts : set Lift,
      floors : set Floor
}

// some rules constraining floors
// floor above me cannot be me; floor below me cannot be me; floor above me can't be floor below me
fact { all f: Floor | (f.AboveFloor != f) && (f.LowerFloor != f) && (f.AboveFloor != f.LowerFloor) }

// two floors cannot share the same AboveFloor or LowerFloor
fact { all f, g: Floor | (f.AboveFloor = g.AboveFloor) => (no f.AboveFloor || f=g) }
fact { all f, g: Floor | (f.LowerFloor = g.LowerFloor) => (no f.LowerFloor || f = g) }

// lowest floor cannot be anyone's above floor
// highest floor cannot be anyone's lower floor
fact { no f: Floor, lf: LowestFloor | f.AboveFloor = lf }
fact { no f: Floor, hf: HighestFloor | f.LowerFloor = hf }

// must be at least two floors
fact { all es: ElevatorSystem | !(lone es.floors) } 
// must be at least one lift
fact { all es: ElevatorSystem | some es.lifts }

// lift must be in one elevator's set of lifts
// requested floor must be in one elevator's set of floors
fact { all r : RequestForFloor
         | one es: ElevatorSystem | ((r.lift in es.lifts)
         && (r.requestedFloor in es.floors)) }

// current floor must be in one elevator's set of floors
fact { all r : RequestForLift
         | one es: ElevatorSystem | (r.floor in es.floors) }

 // only one highest floor
fact { all es: ElevatorSystem | 
          all hf, f: HighestFloor |
         ( ((hf in es.floors) && (f in es.floors)) implies (hf = f)) }
     
// only one lowest floor
fact { all es: ElevatorSystem | 
          all lf, f: LowestFloor |
         ( ((lf in es.floors) && (f in es.floors)) implies (lf = f)) }

fact { all es: ElevatorSystem | one f: es.floors | f in HighestFloor }
fact { all es: ElevatorSystem | one f: es.floors | f in LowestFloor }

fact { all lf: LowestFloor | all r: RequestForLift | (lf = r.floor) implies (r.requestedDirection in Up) }

fact { all hf: HighestFloor | all r: RequestForLift | (hf = r.floor) implies (r.requestedDirection in Down) }

fact { all r: RequestForLift | ((r.requestedDirection in Up) || (r.requestedDirection in Down)) } 

pred addRequest( es, es': ElevatorSystem,   r: Request) {
         es'.requestPool = es.requestPool + r.requestedDirection 
         es'.lifts = es.lifts
         es'.floors = es.floors
}

// used in my asserts to help keep track of visited floors
sig Log  {
	floorsVisited : set Floor
}

fact {
      all f:Floor, es:ElevatorSystem | f in es.floors
}

// remove things from the request pool
pred arrivedAtFloor(l, l': Lift, es, es' : ElevatorSystem, log, log': Log) {
       l'.liftNumber = l.liftNumber
	 log'.floorsVisited = log.floorsVisited + l.currentFloor

       // identify requests for this floor and remove them from the pool
       let requestsForLiftAtThisFloor
               = { r : RequestForLift | (r in es.requestPool) && (l.currentFloor = r.floor) }, 
             requestsForThisFloorFromThisLift
               = { q: RequestForFloor | (q in es.requestPool) && (l.currentFloor = q.requestedFloor) && (l = q.lift) } |
        (#(requestsForLiftAtThisFloor + requestsForThisFloorFromThisLift) > 0) implies (es'.requestPool = es.requestPool - (requestsForLiftAtThisFloor + requestsForThisFloorFromThisLift))

	 // replace l with l', because l' will have the correct currentFloor
       es'.lifts = es.lifts - l + l' 
       es'.floors = es.floors

	 // determine l'.currentFloor and l'.directionOfMovement
	 l.currentFloor in HighestFloor implies  ((l'.directionOfMovement in Down) && (l'.currentFloor = l.currentFloor.LowerFloor))
       l.currentFloor in LowestFloor implies ((l'.directionOfMovement in Up) && (l'.currentFloor = l.currentFloor.AboveFloor))
       (l.currentFloor !in (HighestFloor + LowestFloor)) implies ((l'.directionOfMovement = l.directionOfMovement)
          && ((l.directionOfMovement in Down) implies (l'.currentFloor = l.currentFloor.LowerFloor)) && 
                 ((l.directionOfMovement in Up) implies  (l'.currentFloor = l.currentFloor.AboveFloor))
          )
}

pred initElevators (es : ElevatorSystem, log: Log) { 
	all l: es.lifts | ((l.currentFloor in LowestFloor) && (l.directionOfMovement in Up))
	no es.requestPool
	no log.floorsVisited
}

// expect this to pass
assert someFloorsVisited {
        all ele, ele',ele'': ElevatorSystem, lif, lif', lif'': Lift, logg, logg', logg'': Log | 
            (
            (initElevators(ele,logg)) && (#(ele.floors) = 3)  && (lif in ele.lifts)
              && (arrivedAtFloor(lif, lif', ele, ele', logg, logg'))
              && (arrivedAtFloor(lif', lif'', ele', ele'', logg', logg''))
             ) implies (
             (lif''.currentFloor.LowerFloor in logg''.floorsVisited ) &&
		(lif''.currentFloor.LowerFloor.LowerFloor in logg''.floorsVisited)
		)
}

// expect this to fail
assert  bogusNoFloorsVisited {
        all ele, ele',ele'': ElevatorSystem, lif, lif', lif'': Lift, logg, logg', logg'': Log | 
            (
            (initElevators(ele,logg)) && (#(ele.floors) = 3)  && (lif in ele.lifts)
              && (arrivedAtFloor(lif, lif', ele, ele', logg, logg'))
              && (arrivedAtFloor(lif', lif'', ele', ele'', logg', logg''))
             ) implies
          //   (l''.currentFloor.LowerFloor in logg''.floorsVisited )
	    (no logg''.floorsVisited)
}

// expect this to fail 
assert bogusInit {
        all es: ElevatorSystem, log: Log |            
            initElevators(es,log) => some log.floorsVisited
}

//check bogusInit for 3
//check bogusNoFloorsVisited for 3
check someFloorsVisited for 5