Small HOW-TO for The Lift Spec from ACSD2001 paper

The lift has three floors: 0,1 and 2. The lift controller provides four methods (commands): init, closed, pressed and arriveAt. You type the methods to invoke in "Synchronization" field, then press the "Interpret" button to execute them. 

First thing to execute is the init method. The execution of init moves the controller in working state. Initially the cabin is supposed to be on floor 0 with doors opened. 

The method closed notifies the controller that the doors are closed. Doors of our lift are supposed to be closed by external actor after some timeout. Now interpret closed. Interpreted commands appear in "Trace" field. If the command was successful it will appear in black, failed methods appear in red. After the execution of two first commands the trace is composed of "init" and "closed", both in black. 

Now let's try to call the lift on floor 2. Execute pressed 2. That informs the controller that the lift was called to floor 2, either from the cabin or from the floor. New line appears in trace: "pressed 2 WITH (modify(UP))". That means: the execution of pressed 2 was successful and a modify UP command was emmited from the controller to the external equipment (motor). The cabin is now moving up. 

The last of four commands, arriveAt, notifies the controller that the cabin arrive on a floor. Execute arriveAt 1. The trace reports a failure: arriveAt 1 appears in red. Then execute arriveAt 2. The trace reports: arriveAt2 WITH (modify STOP // open). That means: the controller accepts the command and emmits two commands in parallel: stop the motor and open the doors. In our simple specification we don't care about the full stop of the cabin before open the doors. 

To resume: you typed 

• init 
• closed 
• pressed 2 
• arriveAt 1 
• arriveAt 2 

• init 
• closed 
• pressed 2 WITH (modify(UP)) 
• arriveAt 1 
• arriveAt 2 WITH ((modify(STOP))//(open))