Introducing State
We now extend our basic model with the concept of a state. The way to conceptualize the model as a whole is a state transition system. This means that for any event (see Messages and Actions) the state can be updated. Remember that the state here represents information pertaining to one order. There is no current requirement to provide initial values in the state, but it should be noted that those fields which have no explicit initial value are provided with a generated value. It is recommended that values with no initial value are either those which are initialised via an incoming message, or are initialised via an action as discussed for example in the Adding Actions section.
State initialisation
Let us first construct a state in our basic model (here we use the canonical name state but there can be many such global states with any name):
Here we have introduced two fields: side
which is of type Side
, which is not optional, and price
of type Price
which is optional. It is important to note that initial values on fields are not required and if are not present, a candidate is generated upon analysis. In this example, live_order
has been given an initial value of false
, where are Side
and Price
don’t have initial values specified.
Assignment to and from state
In the basic model we can now use the declared state variable as a way of storing information. For example in the message receive block we can write
Note here how state
has been updated with values from the incoming message, and state can be used to populated values of the outbound ExecutionReport
.
Automatic assignment using state
It is possible to define a special subset of state variables which can be used to automatically update to and from the state. In order to do this we create an assignable
section which contains fields which have been imported via messages. For example we can create the following state:
where we declare fields common to both outgoing and incoming messages in the assignable
section of the state. It is now possible to exploit this when processing messages. For example we could rewrite the message receive to be:
Note here using this syntax the fields declared in the assignable
section of state are automatically updated using the assignFrom
directive. In the send command, the insertion of the {state with
syntax uses the fields from the assignable
section of state to automatically set the fields of ExecutionReport
. In this case the fields Side
and OrderQtyData.OrderQty
are set automatically.
Errors and Warnings
As before it is possible to encounter errors and warnings in this model. Those that are most pertinent here to the creation of an internal state are
- Assignable field errors
The only fields that can exist in the assignable section of state are fields that have been imported in a message. One cannot place an arbitrary field such as live_order
in the assignable section and the following error will appear if it is placed there:
Couldn't resolve reference to MessageRequire 'live_order'
- Assignable field optionality errors
If the optionality of an assignable field does not match the corresponding message field, then an error will occur. For example if the assignable field
Then the following error will be given:
This field should be defined as optional.
It is possible to deal with the situation where a field is imported both non-optionally and optionally in messages. This is discussed in the advanced section Ambiguous optionality
Full Model – Imandra Analysis
Click on the image below for an interactive analysis of this model performed by imandra.
Full Model - IPL Code
Generated Documentation
Click here to view the generated documentation for this model.