This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
Machines
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



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.
