An IPL model can define an set of global internal declarations which constitute the state of the model. Typically, we just define one state internal declaration, and use this to reason. The resulting IPL model then represents a state transition system which allows us to reason using Imandra.
Declaration of the state is done by defining internal variables:
Here it is not necessary to define a field as optional, or to give an initial value. It is important to note that should an initial value not be given, a candidate is generated internally to calculate the initial state when analysing the model as state machine. This may provide unexpected results, so it is advised to give initial values where applicable.
In a typical use case, we would want to store the order, cumulative and leaves quantities, and the average executed price thus far, the side of an order (typically buy or sell), and the limit price, if present:
In this case we explicitly initialise the
CumQty field with the value
One can define records in the internal state also, and give initial values. For example a user may wish to record the opening and closing times of the venue as a record:
In order to import this into the state with initial values we extend our state by writing:
The meaning of
UTCTimeOnly (8, 0, 0, None) is explained in greater detail in the Expressions.
Messages, both inbound and outgoing, contain many fields that can be saved into the state variable or, the opposite, set from the values of the state. To make this more straightforward, we have introduced the concept of
assignable fields that may be automatically assigned from a message or assigned to an outbound message.
Let’s modify slightly the internal state definition from above by attributing four
assignable fields. We’ll revisit this example when we come to discuss receiving and rejecting messages in the messages section, but for now let us assume that the optionality of each field in the assignable section of the state is shared between every message. We can then write :
now the fields in the
assignable section are marked specifically to correspond to fields which will be sent or received from messages in the model. When sending a message one can, for example, write
which automatically assigns the values of any fields in the outgoing
ExecutionReport message, with the values from state. Equally it is possible to assign to the state from an incoming message. For example in the following excerpt, any fields from the state coinciding between those in the incoming
NewOrderSingle message are automatically assigned to the values of the respective field in the message.
It is possible for the optionality of fields to differ and for them still to form part of the assignable section of state. We refer to this as ambiguous optionality and such fields are defined in the state using the
:* notation in the field declaration. For example if the
Side field was optional in the ExecutionReport, but required in the
NewOrderSingle message the state would be defined as
We will revisit this concept in the section of Messages and Actions.