We now extend our model with messages and actions by adding actions. Actions are constrained, asynchronous events which are produced by a trading venue (for example) which affect the state of the system.
Defining an action
We now introduce two simple actions which correspond to an internal constrained input from the venue or trading system, both of which can update the state.
Let us first define, for example a fill action:
In this action we represent a fill event from the venue, meaning an order has been processed with a certain fill quantity and fill price. This is represented by the fields fill_price and fill_qty. These two fields do not require initial values as actions are constrained inputs which are assumed to have these values provided by the venue. As well as the fields there are validation statements which ensure that an incoming action is valid. In this case we check that fill price and fill quantity are non-zero and positive. We also check that the price is consistent with the price fields held in the state. For a better explanation of this expression see Option cases.
Book state update
Another action we could define is a message which updates the best bid and best ask of the stock relating to the order on the venue.
This action validates that the price updates make sense and rejects the action otherwise.
If an action is valid (has passed all the validation statements in its definition) then we can write code which receives the action in the same as we did for receiving a message.
Receiving a fill action
This action updates the state information about the order in question according to information coming from a fill action event. It then send an ExeuctionReport as an outbound message with the relevant fill information.
Receiving a bookstate action
This actions updates the state book best bid and best ask values according to the book state.
Full Model – Imandra Analysis
Click on the image below for an interactive analysis of this model performed by imandra.
Full Model - IPL Code
Click here to view the generated documentation for this model.