Tutorials
These tutorials show incrementally how to create an IPL file that represents the correct protocol for receiving and sending FIX messages for a particular venue or trading system.
We model the IPL file as a state transition system tracking the progress of a particular order. In the state of the system, all information pertains to one order for the examples shown here.
It is possible to model more complicated systems, but for this exposition we consider one order.
Declaring Message Flows
Imandra can automatically produce test cases and regions for analysis. Message Flows are a way of declaring a sequence of events that are of interest for analysis.
In each tutorial section we define a message flow, linking the model to a browser view that graphically demonstrates analysis performed by Imandra.