Example Data: tmp_elevator_spec_cabmot.gen

Dot-processed graph as SVG-image

Token IO

% Elevator exanple: specification (cabin motion)

<Generator>
"E_cabmot"

<Alphabet>
"c_arlw"	
"c_arup"
"c_up"
"c_down"
"c_stp"
</Alphabet>

<States>
"Idle"
"Down"
"Up"
"Stop"
</States>

<TransRel>
% Idle 
"Idle" "c_down" "Down"
"Idle" "c_up" "Up"
"Idle" "c_arlw" "Idle"
"Idle" "c_arup" "Idle"

% Moving down
"Down" "c_arlw" "Stop"

% Moving up
"Up"   "c_arup" "Stop"

% Moving up
"Stop"   "c_stp" "Idle"

</TransRel>

<InitStates>
"Idle"
</InitStates>

<MarkedStates>
"Idle"
</MarkedStates>

</Generator>

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