Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
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 modeling a machine is to prove that the machine never reaches an invalid state, i.e. the variables always have values that satisfy the invariant. First we briefly summarize of which parts a machine consists:
- Refines
Optionally a machine can refine another one. We’ll 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 hypothesis.
- Variables
The variables’ values are determined by an initialization and can be changed by events. Together they constitute the state of the machine. Each variable must be given a type by the invariants.
- Invariants
This 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 under which conditions it might occur. The initialization of the machine is a special case of an event.
|
|
|
|
|
|