2.7.2 Machines

A machine describes the dynamic behavior of a model by means of variables whose values are changed by events. A central aspect of modelling a machine is to prove that the machine never reaches an invalid state, i.e. the variables always have values that satisfy the invariants. Here is a brief summary of the part that a machine contains:

Refines

A machine has the option of refining another one. We will see in Section 2.7.4 what that means.

Sees

We can use the context’s sets, constants and axioms in a machine by declaring it in the Sees section. The axioms can be used in every proof in the machine as hypotheses.

Variables

The variables’ values are determined by an initialisation event and can be changed by events. This constitutes the state of the machine. The type of each variable must be declared in the invariant section.

Invariants

These are predicates that should be true for every reachable state. Each invariant has a label.

Events

An event can assign new values to variables. The guards of an event specify the conditions under which it can be executed. The initialisation of the machine is a special case of an event.