
'1' for 3 seconds, '2' for 5 seconds, '3' for 10 seconds and '4' for 20 seconds.
 \n
CLOCK GUARANTEES AND ASSUMPTIONS
 \n
DESIGNATED FLOOR GUARANTEES
 \n
Doors Movement Gars
 \n
EMERGENCY GUARANTEES AND ASSUMPIONS
 \n
ENVIROMENT'S DESCRIPTION ASSUMPTIONS
 \n
G(fullyOpenedStateAtDesignatedFloor&(seconds5)&!memEmergency&!sabbathMode)->closingDoors;
 \n
INIT ASSUMPTIONS
 \n
INIT GUARANTEES
 \n
Movement Gars
 \n
REACH TO DESIGNATED FLOORS
 \n
RETURN TO FLOOR0 GUARANTEES AND ASSUMPTIONS
 \n
REWARD SHOULD BE BY THE NUMBER OF THE FLOOR
 \n
SABBATH MODE GUARANTEES AND ASSUMPIONS
 \n
SOUND GUARANTEES
 \n
Safety Guarantees
 \n
Signal indicating that 3,5,10 and 20 seconds have passed (since the last
 \n
System's motors and timer commands
 \n
Those env variables are being connected to the controller, reporting
 \n
Used for 2 cases: 1.if standing in a floor and it calls. 2.if standing in a designated floor don't move.
 \n
Used to make sure that an unfair user won't stuck the elevator at one floor
 \n
activation of the boolean variable 'countTime_c')
 \n
current floor\door state.
 \n
env variables indicating calls (from floors).
 \n
gar 
 \n
inputs
 \n
no further comments on the spec, as every gar and asm has a symbolic name.
 \n
pRespondsToS(atEmergencyFloor&!doorsWereFullyOpened,doorsAreFullyOpened);
 \n
type \n
type definitions
 \n
