4.1.2 The Formal Model

We are going to create a visualization for a simple lift system that allows movement of a single lift cage between three floors. The door of the lift can be closed and opened - all in response to the pressing of floor call and cage send buttons.

You can download the Event-B model here. Decompress the archive and put the files into a new folder called model relative to your index.html file.