Example: Elevator Problem

Browse:  Elevator.csv

Add: Elevator:1.current_floor,Elevator:1.direction,Elevator:1.up,Elevator:1.down 

Abbreviations: 

Elevator:1.current_floor=f, Elevator:1.direction=d, Elevator:1.up=up, Elevator:1.down=down

Properties:

// Revised Basic, when up and down are included:

G [ up=up' && down=down'
     ->
     (d == "down"  &&  d' == "down" -> f > f')  &&
     (d == "up"  &&  d' == "up" -> f < f')  &&
     (d != d' -> f == f')
  ];

// Change directions from down to up

G [ up=up' && down=down'
     ->
    ( d = "down" && 
      f <= up#min &&
      f <= down#min
       -> d' = "up" ) 
   ];

G [ up=up' && down=down'
     ->
    ( d == "up" && 
      f >= up#max &&
      f >= down#max
       -> d' = "down")
   ];

// Lists are in sorted order

G [ up#size > 1 -> for(n, 0:up#size-2,  up[n] < up[n+1]) ];

G [ down#size > 1 -> for(n, 0:down#size-2,  down[n] > down[n+1]) ];

//  Properties of lists and floors

G [ f in up && !(f in up') -> f' = f ];

G [ f in down && !(f in down') -> f' = f ];

G [ all(n, up, F[f = n]) ];

G [ all(n, down, F[f = n]) ];

// When a floor is reached

G [ down#size > down'#size && up=up' 
	-> (d = "down" && down != "[]" 
		     -> (f = down[0] -> !(f in down') && f = f'))];

G [ up#size > up'#size && down=down' 
	-> (d = "up" && up != "[]" 
		     -> (f = up[0] -> !(f in up') && f = f'))]