Elevator Example - Details

This page gathers detailed models, specifications and supervisors related to the elevator example from the iodevice plug-in. Corresponding files are located in libfaudes/plugin/iodevice/tutorial/data.

Signals and Events

The LRT laboratory set-up uses a simple analog circuit to simulate the behaviour of the elevator plant. Relevant digital signals (over continuous time) are given in the below table. The bit address in the first column refers to the wiring of the laboratory set-up.

Output Signals Input Signals
Name Comments (active) Addr.
Y_CM_UP cabin motor on, upwards #0
Y_CM_DN cabin motor on, downwards #2
Y_DM_OP door motor on, open #4
Y_DM_CL door motor on, close #6
Y_OL_UP button led, upper level, on#8
Y_OL_LW button led, lower level, on#10
 
Name Comments (active) Addr.
U_CS_UP cabin sensor, upper position#6
U_CS_LW cabin sensor, lower position#4
U_DS_OP door sensor, open #10
U_DS_CL door sensor, closed #8
U_OB_UP upper button pressed #12
U_OB_LW lower button pressed #14
U_DS_LB light barrier occupied #16

Relevant discrete events by definition correspond to edges on the above signals. An event that is triggered by the plant is called an input event. An event that must be triggered externally (e.g. by the supervisor) is called an output event. The below tables specify the correspondence between edges of signals and output- and input events.

Cabin

Event TypeTrigger/Action Comments
c_up output clear Y_CM_DN, set Y_CM_UP activate cabin motor, upwards
c_down output clear Y_CM_UP, set Y_CM_UP activate cabin motor, downwards
c_stp output clear Y_CM_DN, clear Y_CM_UP stop cabin motor
c_arup input pos. edge on U_CS_UP cabin arrives at upper sensor
c_lvup input neg. edge on U_CS_UP cabin leaves upper sensor
c_arlw input pos. edge on U_CS_LW cabin arrives at lower sensor
c_lvlw input neg. edge on U_CS_LW cabin leaves lower sensor

Door

Event TypeTrigger/Action Comments
d_open output clear Y_DM_OP, set Y_DM_CL activate door motor to open
d_close output clear Y_DM_CL, set Y_DM_OP activate door motor to close
d_stp output clear Y_DM_OP, clear Y_DM_CL stop door motor
d_arop input pos. edge on U_DS_OP door arrives at sensor open
d_lvop input neg. edge on U_DS_OP door leaves sensor open
d_arcl input pos. edge on U_DS_CL door arrives at sensor closed
d_lvcl input neg. edge on U_DS_CL door leaves sensor closed
d_lbbl input pos. edge on U_DS_LB light barrier blocked
d_lbrl input neg. edge on U_DS_LB light barrier released

Operator

Event TypeTrigger/Action Comments
o_upb input pos. edge on U_OB_UP upper button pressed
o_lwb input pos. edge on U_OB_LW lower button pressed
o_uplon output set U_OL_UP illuminate upper button
o_uploff output clear U_OL_UP turn off upper button light
o_lwlon output set U_OL_LW illuminate lower button
o_lwlnoff output clear U_OL_LW turn off lower button light

Device Configuration

The LRT laboratory set-up uses two Advantech PCI boards for digital IO, one of them providing 64 input signals, the other 64 output signals. Signals are accessed through the comedi framework, where we use the system device files /dev/comedi0 and /dev/comedi1. The below iodevice configuration introduces events to libFAUDES according to the above definition. Signals referenced by a bits address, where each board uses a range from 0 to 63. 

<DeviceContainer name="LrtElevatorPIO"> 

<!-- Common time scale in ms/ftiu -->
<TimeScale value="10"/> 

<!-- List of devices -->
<Devices> 

<!-- Device for Input signals resp. events -->
<ComediDevice name="LrtElevatorInput"> 

<!-- Sample interval for edge detection in ns -->
<SampleInterval value="100"/> 

<!-- Sytem device file -->
<DeviceFile value="/dev/comedi0"/> 

<!-- Trigger based event definitition to follow -->
<EventConfiguration> 

<!-- Cabin sensor: arrive at upper position -->
<Event name="c_arup" iotype="input"> 
<Triggers> <PositiveEdge address="6"/> </Triggers> 
</Event> 

<!-- Cabin sensor: leave upper position -->
<Event name="c_lvup" iotype="input"> 
<Triggers> <NegativeEdge address="6"/> </Triggers> 
</Event> 

<!-- Cabin sensor: arrive at lower position -->
<Event name="c_arlw" iotype="input"> 
<Triggers> <PositiveEdge address="4"/> </Triggers> 
</Event> 

<!-- Cabin sensor: leave lower position -->
<Event name="c_lvlw" iotype="input"> 
<Triggers> <NegativeEdge address="4"/> </Triggers> 
</Event> 

<!-- Door sensor: door reached closed position -->
<Event name="d_arcl" iotype="input"> 
<Triggers> <PositiveEdge address="8"/> </Triggers> 
</Event> 

<!-- Door sensor: door leaving closed position -->
<Event name="d_lvcl" iotype="input"> 
<Triggers> <NegativeEdge address="8"/> </Triggers> 
</Event> 

<!-- Door sensor: door recahed open position -->
<Event name="d_arop" iotype="input"> 
<Triggers> <PositiveEdge address="10"/> </Triggers> 
</Event> 

<!-- Door sensor: door leaving open position -->
<Event name="d_lvop" iotype="input"> 
<Triggers> <NegativeEdge address="10"/> </Triggers> 
</Event> 

<!-- Door sensor: light break occupied -->
<Event name="d_lbbl" iotype="input"> 
<Triggers> <PositiveEdge address="16"/> </Triggers> 
</Event> 

<!-- Door sensor: light break released -->
<Event name="d_lbrl" iotype="input"> 
<Triggers> <NegativeEdge address="16"/> </Triggers> 
</Event> 

<!-- Opertor sensor: upper button pressed -->
<Event name="o_upb" iotype="input"> 
<Triggers> <NegativeEdge address="12"/> </Triggers> 
</Event> 

<!-- Opertor sensor: lower button pressed -->
<Event name="o_lwb" iotype="input"> 
<Triggers> <NegativeEdge address="14"/> </Triggers> 
</Event> 

</EventConfiguration> 
</ComediDevice> 



<!-- Device for Output signals resp. events -->
<ComediDevice name="LrtElevatorOuput"> 

<!-- Sample interval for edge detection in ns -->
<SampleInterval value="100"/> 

<!-- Sytem device file -->
<DeviceFile value="/dev/comedi1"/> 

<!-- Action based event definitition to follow -->
<EventConfiguration> 

<!-- Cabin actuator: stop motor  -->
<Event name="c_stp" iotype="output"> 
<Actions> <Clr address="0"/> <Clr address="2"/> </Actions> 
</Event> 

<!-- Cabin actuator: move upwards -->
<Event name="c_up" iotype="output"> 
<Actions> <Clr address="2"/> <Set address="0"/> </Actions> 
</Event> 

<!-- Cabin actuator: move downwards -->
<Event name="c_down" iotype="output"> 
<Actions> <Clr address="0"/> <Set address="2"/> </Actions> 
</Event> 

<!-- Door actuator: stop motor  -->
<Event name="d_stp" iotype="output"> 
<Actions> <Clr address="4"/> <Clr address="6"/> </Actions> 
</Event> 

<!-- Door actuator: run motor to open  -->
<Event name="d_open" iotype="output"> 
<Actions> <Clr address="6"/> <Set address="4"/> </Actions> 
</Event> 

<!-- Door actuator: run motor to close  -->
<Event name="d_close" iotype="output"> 
<Actions> <Clr address="4"/> <Set address="6"/> </Actions> 
</Event> 

<!-- Operator actuator: illuminate button upstairs -->
<Event name="o_uplon" iotype="output"> 
<Actions> <Set address="8"/> </Actions> 
</Event> 

<!-- Operator actuator: turn of upstairs button-light -->
<Event name="o_uploff" iotype="output"> 
<Actions> <Clr address="8"/> </Actions> 
</Event> 

<!-- Operator actuator: illuminate button downstairs -->
<Event name="o_lwlon" iotype="output"> 
<Actions> <Set address="10"/> </Actions> 
</Event> 

<!-- Operator actuator: turn off downstairs button-light -->
<Event name="o_lwloff" iotype="output"> 
<Actions> <Clr address="10"/> </Actions> 
</Event> 

</EventConfiguration> 
</ComediDevice> 

</Devices> 
</DeviceContainer>

Plant Model

Our plant model is organized in four components, namely G_cabin, G_door, and G_lbarrier, and G, each referring to the respective alphabet.

Cabin G_cabin
Door G_door
Light barrier G_lbarrier

Operator events are the push buttons incl. illumination. The operator model G realises the corresponding full language.

Specification

E_opcmds: We sense the operator button to enable cabin activity. The internal events a_* are introduced to simplify synchronisation with further specification components.

E_cabmot: Cabin movement must not be interupted until the upper or lower position is reached. Note that this specification also introduces that a_done can only occur after the cabin did perform some shuttle operation.

E_drmot1: Similar to the cabin motion as specified by E_cabmot, the door motion specification requires the door to either open or close and to stop once the goal is accomplished. However, the we allow the closing operation to fail to accomodate for the light barrier. The internal events a_close and a_open to indicate the outcome of a door operation.

E_scheds: The top level schedule enables cabin movement once the door has been closed. After cabin movement, the door is to be opened.

E_drsaf1: The first safety requirement to the door is that it must not be open when the cabin moves.

E_drsaf2: The second safety requirement to the door is that it must re-open when the light barrier becomes blocked during closing.

Controller Synthesis

Controller synthesis for the entire elevator setup is performed by the luafaudes script elevator_synthesis.lua from the iodevice plug-in tutorial. 

-------------------------------------------------------------------------------
-- read files
-------------------------------------------------------------------------------

-- report
print("elevator: reading plant and specification data")

-- load plant components from file
plant_cabin    = faudes.Generator("data/elevator_plant_cabin.gen")
plant_door     = faudes.Generator("data/elevator_plant_door.gen")
plant_lbarrier = faudes.Generator("data/elevator_plant_lbarrier.gen")
plant_buttons  = faudes.Generator("data/elevator_plant_buttons.gen")
plant_leds     = faudes.Generator("data/elevator_plant_leds.gen")

-- load specification components from file
spec_opcmd   = faudes.Generator("data/elevator_spec_opcmd.gen")
spec_opcmds  = faudes.Generator("data/elevator_spec_opcmds.gen")
spec_opled   = faudes.Generator("data/elevator_spec_opled.gen")
spec_cabmot  = faudes.Generator("data/elevator_spec_cabmot.gen")
spec_cabmots = faudes.Generator("data/elevator_spec_cabmots.gen")
spec_drmot1  = faudes.Generator("data/elevator_spec_drmot1.gen")
spec_drsaf1  = faudes.Generator("data/elevator_spec_drsaf1.gen")
spec_drsaf2  = faudes.Generator("data/elevator_spec_drsaf2.gen")
spec_scheds  = faudes.Generator("data/elevator_spec_scheds.gen")

-- dont name states
faudes.StateNamesOff();

-------------------------------------------------------------------------------
-- build plant model
-------------------------------------------------------------------------------

-- report
print("elevator: build pant model")

-- prepare plant model
plant_full = faudes.Generator() 
plant_full_min = faudes.Generator()

-- build full model consisting of cabin, door and operator
faudes.Parallel(plant_full,plant_cabin,plant_full)
faudes.Parallel(plant_full,plant_door,plant_full)
faudes.Parallel(plant_full,plant_lbarrier,plant_full)
faudes.Parallel(plant_full,plant_buttons,plant_full)
faudes.Parallel(plant_full,plant_leds,plant_full)

-- have a sensible name
plant_full:Name("elevator full plant (cabin plus buttons)")

-- get eventset of plant model
plant_full_alphabet = faudes.EventSet(plant_full:Alphabet())

-- reduce state space 
faudes.StateMin(plant_full,plant_full_min)

-- write to file
plant_full_min:Write("tmp_elevator_plant_full.gen")

-------------------------------------------------------------------------------
-- build specification
-------------------------------------------------------------------------------

-- report
print("elevator: build specification")

-- prepare overall specification
spec_full = faudes.Generator()
spec_full_min = faudes.Generator()

-- compose overall specification
faudes.Parallel(spec_full,spec_opcmds,spec_full)
faudes.Parallel(spec_full,spec_scheds,spec_full)
faudes.Parallel(spec_full,spec_opled,spec_full)
faudes.Parallel(spec_full,spec_cabmots,spec_full)
faudes.Parallel(spec_full,spec_drmot1,spec_full)
faudes.Parallel(spec_full,spec_drsaf1,spec_full)
faudes.Parallel(spec_full,spec_drsaf2,spec_full)
faudes.StateMin(spec_full,spec_full_min)

-- write to file
spec_full_min:Write("tmp_elevator_spec_full.gen")


-------------------------------------------------------------------------------
-- build synthesis
-------------------------------------------------------------------------------

-- report
print("elevator: synthesis")

-- match plant and spec alphabets
alphabet_full = faudes.EventSet();
alphabet_plant_extra = faudes.EventSet();
faudes.AlphabetUnion(plant_full:Alphabet(),spec_full:Alphabet(),alphabet_full);
faudes.AlphabetDifference(alphabet_full,plant_full:Alphabet(),alphabet_plant_extra);
faudes.InvProject(spec_full_min,alphabet_full);
faudes.InvProject(plant_full_min,alphabet_full);

-- extra events in the specification are controllable
plant_full_min:SetControllable(alphabet_plant_extra);

-- compute supervisor for full elevator setup
super_full = faudes.Generator();
super_full_min = faudes.Generator();
faudes.SupConNB(plant_full_min,spec_full_min,super_full)
super_full:Name("elevator supervisor (full)")
faudes.StateMin(super_full,super_full_min)

-- write to file
super_full_min:Write("tmp_elevator_super_full.gen")

-- report
print("elevator: full supervisor statistics")
super_full_min:WriteStatistics()
Resulting Supervisor S_full

Simulation

A shell script elevator_simulation.sh and a configuration file elevator_supervisor.sim are prepared to run a simulation on the supervisor. The simulation also includes the plant components Gcabin and Gdoor to monitor the plant state. The below log shows the elevator moving from the the lower level to the upper level incl. door operations. 

$ cd ./libfaudes/plugins/iodevice/tutorial
$ ./elevator_simulation.sh -v
% simfaudes: ========================================== found generator #1: cabin
% simfaudes: ========================================== found generator #2: door
% simfaudes: ========================================== found generator #3: supervisor (full)
...
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleOp"      1              </DiscreteState> 
% simfaudes: ========================================== enabled events:
<EnabledEvents> "d_lbbl"      "o_upb"       "o_lwb"        </EnabledEvents> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command:

The simulator starts in its initial state, where the first two components refer to the cabin and the door respectively. The third component is the supervisor state. All enabled events are input events and cofigured to have a negative priority. Hence, the simulation will not propose to execute either of them automatically. We decide to manually issue a o_upb event, i.e. the operator presses the upper button. The simulator proposes to execute the synchronisation event a_start and to turn on the button lights. We accept the proposal by hitting the return key. 

% simfaudes: ========================================== enter command: o_upb
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleOp"      34             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "a_start" </ProposedEvent>
% simfaudes: ========================================== enter command: a_start
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleOp"      69             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "o_uplon" </ProposedEvent>
% simfaudes: ========================================== enter command: o_uplon
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleOp"      30             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "o_lwlon" </ProposedEvent>
% simfaudes: ========================================== enter command: o_lwlon
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleOp"      64             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "d_close" </ProposedEvent>
% simfaudes: ========================================== enter command:

In the remaining log, the simulator closes the door, drives the cabin upstairs and opens the door again. As above, input events must be chosen manually, output events are proposed by the simulator. The simulation ends with door opened and the cabin upstairs, while waiting for input events (e.g. an operator button). 

% simfaudes: ========================================== execute event: d_close
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "CloseOp"     16             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: d_lvop
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "CloseMd"     55             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: d_arcl
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "CloseCl"     26             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "d_stp" </ProposedEvent>
% simfaudes: ========================================== enter command: d_stp
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleCl"      27             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "a_close" </ProposedEvent>
% simfaudes: ========================================== enter command: a_close
% simfaudes: ========================================== current state:
<DiscreteState> "IdleLw"      "IdleCl"      2              </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "c_up" </ProposedEvent>
% simfaudes: ========================================== enter command: c_up
% simfaudes: ========================================== current state:
<DiscreteState> "UpLw"        "IdleCl"      8              </DiscreteState> 
% simfaudes: ========================================== proposed action: 
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: c_lvlw
% simfaudes: ========================================== current state:
<DiscreteState> "UpMd"        "IdleCl"      81             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: c_arup
% simfaudes: ========================================== current state:
<DiscreteState> "UpUp"        "IdleCl"      100            </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "c_stp" </ProposedEvent>
% simfaudes: ========================================== enter command: c_stp
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleCl"      25             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "d_open" </ProposedEvent>
% simfaudes: ========================================== enter command: d_open
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "OpenCl"      98             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: d_lvcl
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "OpenMd"      57             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command: d_arop
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "OpenOp"      90             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "d_stp" </ProposedEvent>
% simfaudes: ========================================== enter command: d_stp
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleOp"      40             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "a_open" </ProposedEvent>
% simfaudes: ========================================== enter command: a_open
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleOp"      82             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "a_done" </ProposedEvent>
% simfaudes: ========================================== enter command: a_done
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleOp"      49             </DiscreteState> 
% simfaudes: ========================================== proposed action: 
<ProposedEvent> "o_uploff" </ProposedEvent>
% simfaudes: ========================================== enter command: o_uploff
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleOp"      76             </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedEvent> "o_lwloff" </ProposedEvent>
% simfaudes: ========================================== enter command: o_lwloff
% simfaudes: ========================================== current state:
<DiscreteState> "IdleUp"      "IdleOp"      3              </DiscreteState> 
% simfaudes: ========================================== proposed action:
<ProposedTime> inf </ProposedTime>
% simfaudes: ========================================== enter command:

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"

>>