Rich State Modelling
We harness Isabelle's type system to support state spaces with rich types. In this example, we are modelling a dwarf signal. The zstore command creates a state space with a number variables, and invariants over the state, in a similar style to a Z schema. This functionality is provided by the session Z_Toolkit and Z_Machines.
The operations specify the ways in which we can update the state. They operate over a named state space, and make use of parameters that are drawn from a suitable set. The body of the operation specifies a number of preconditions, which must be satisfied to execute the operation. An update specifies the changes that are made to variables when the operation executes.