For specific venues and trading systems, it is important to allow the creation of extra message fields, record field and enum cases. This section shows declaring such artifacts can be done, and how it integrates with the rest of the specification.
Custom Enum cases
In our model we have make use of the OrdType enum in order to refer to the type of order. Let us say we want to introduce a new order type called StopSpread which is a type of limit order intended to only be entered onto an order book once the spread is less than a certain preset amount defined as a proportion of the best bid price. After a fill the rest of the order is set as a normal limit order at the price of the fill.
In order to extend the OrdStatus enum we write a custom extension:
here we define a new tag “s” which will indicate this type of order on the wire.
Once a StopSpread order has been entered onto the book, the OrdStatus field of the state becomes OrdStatus.New and remains as this even if the spread changes.
Custom Message Fields
In order to incorporate the custom enum case into the model, we need to extend the NewOrderSingle message to add a field which records the spread proportion figure. We do this first by extending the message declaration:
Then we can import it into the message and add some validation to the inclusion of the field, adding some validation conditions - that the proportion is strictly between 0 and 1, also we ensure that a price is present for this type of order.
Updating the state
We now need to update the state so that the spread proportion can be recorded throughout the life of the order:
Updaing receive code
Now we are adding order types which have a more complex logic, we need to update the code we write when receiving a NewOrderSingle message, and a bookState action.
Updating NewOrderSingle receive code
We update the receive code to change the OrdStatus of the state if the spread between the current best bid and best ask is already within that specified by the SpreadProportion of the initial order.
If the spread is already within the specified SpreadProportion then the OrdStatus is updated to New otherwise is it set as PendingNew.
Updating the bookState action receive code
When the best bid and best ask prices are updated we check whether the order is of type StopSpread and if so we determine if the OrdStatus of the state should be updated:
Updating fill action validation
An order with OrdStatus==OrdStatus.PendingNew indicates that it is not eligible to be filled. We add a validation to a fill action to ensure that the action not be produces for such an order:
Errors and Warnings
Ipl will check that tags are consistent. This means that if you use a field tag which corresponds to an existing field with a different name, it will error. It also does this check for enum case tags. This is crucial to ensure the resulting system is sound when executed as a simulator. If for example you were to add the custom field as
you would receive an error saying:
Field SpreadProportion has tag 11, but a field with the same tag but name ClOrdID already exists.
this ensuring the correctness of the generated model.
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.