Elevator
This case study is concerned with a system that manages a elevator system.
Here, we provide the following suplementary material:
- The UML diagrams used to model the case study
- The provenance templates generated
- The set of bindings extracted from the execution
- For each binding, its expansion in SVG and PROVN format
Such a case study has been modelled through the following UML Sequence and State Machine Diagrams.
UML Sequence diagrams



UML State Machine diagrams
CarPositionControl UML State Machine diagram

CarPositionIndicator UML State Machine diagram

Dispatcher UML State Machine diagram

Door UML State Machine diagram

DoorControl UML State Machine diagram

Drive UML State Machine diagram

DriveControl UML State Machine diagram



Passenger UML State Machine diagram
