These tutorials will show incrementally how to create an ipl file, which represents the correct protocol for receving and sending FIX messages for a particular venue or trading system. We show how we model the ipl file as a state transition system which tracks the progress of a particular order. In the state of the system it is important to remember that all the information pertains to one order for the examples we show here. It is possible to model more complicated systems, but for the purposes of our exposition it is most useful to simply consider one order.

Declaring Scenarios

Scenarios are a way of declaring a common sequence of events which are of interest for analysis. imandra can automatically produce test cases and regions for analysis - these are particular when analysing scenarios. The way to define a scenario is as follows:

scenario NewOrderFill {
	name "NewOrderFill"
	description "Send NewOrderSingle Message then receive a fill action"
	events[NewOrderSingle, fill]

The name and description here are optional. The analysis explores the different ways in which the values of fields in the events can affect the state of the system.

In each section of the tutorial we define a scenario, which allows us to link the model to a browser demonstrating graphically an analysis performed by imandra.