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:

// Basic Property

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

// Changing Direction

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