We now have a full model which receives messages and actions, including custom fields, enum cases, and custom repeating group fields. In this last section we discuss more advanced functionality available.
It is possible to import a field in the assignable section of an internal state declaration which is declared both optionally and non-optionally in the model.
Mismatched optionality imported message fields
For example let us import the field ExecInst in NewOrderSingle:
and let us declare the field in the ExecutionReport as required, as we want to it to always be present in any outgoing message:
Adding ambiguous optionality fields to the state
Now if we add the ExecInst field to the state we need to use ambiguous notation for the type to denote that the field is both optional and non-optional. We do this using :* notation - such fields require stated initial values to be non-optional:
Declaring default values
In the situation above we must provide a default value for an optional field in an incoming message which corresponds to an assignable field - this is so that a value can be provided for a required value in an outgoing message. Failure to do see will result in the error
This message require needs a default value as it is optional but used to assign an ambiguous state value
For NewOrderSingle we thus write:
to provide such a value.
A verification pack is something you might want to prove about your model. An example would be that any transition of the OrdStatus fields of the state is valid - for example that once an order is cancelled, it does not become reactivated. There are a set of such verification goals pre-written which users can activate for analysis by imandra. The existing set of such goals is
EmptyString - checks that no outbound string values are the empty string - which is not allowed in the FIX specs;
Venue - checks that any transition of OrdStatus field of the state is valid. The way to specify a verfication pack is
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.