Basic Model

In our first complete example, we’ll create a simple model that accepts incoming NewOrderSingle messages (as defined in FIX 4.4) and acknowledges them using an Execution Report. We will learn how to specify correct behaviour of the model, introducing validity constraints which will check that an incoming message is valid for example. If the constraints are satisfied then the message is handled as described in Receiving Valid Messages below. If the constraints are not satisfied then a rejection message can be specified as described in Rejecting invalid messages below.

Setting the stage

We start by importing the correct FIX version.

import FIX_4_4

Declaring incoming messages

In this simple model, we will just import the NewOrderSingle incoming message. In order to specify the fields we expect to receive and those we send out we use the req, opt or ign directives.

For example, let us specify the following for NewOrderSingle

message NewOrderSingle {
    req ClOrdID
    req Side
    req TransactTime
    req OrdType valid when it in [ OrdType.Limit, OrdType.Market ]
    req OrderQtyData.OrderQty
}

which determines the fields which are required to be present. We can additionally import fields which are optional (opt) and ignored (ign):

message NewOrderSingle {
    req ClOrdID
    req Side
    req TransactTime
    req OrdType
    req OrderQtyData.OrderQty
    opt Price
    ign Account
}

see the section on Importing Messages for a description of req, opt and ign.

Imposing validity constraints on individual fields

For individual fields we can introduce validity constraints which will check the values of incoming fields. For example on a particular message field we can write

    req OrdType valid when it in [ OrdType.Limit, OrdType.Market ]

where Limit, Market are valid values from the OrdType Enum. This states that the value of the OrdType must be one of the values specified, and if not the message is rejected. See the section on Expressions for how to write more complex validation conditions.

It is not possible to write a validation condition on an ignored field.

Imposing general message validity constraints

It is possible to impose general validity constraints on a message. For example we may write the statement

validate {
         this.OrdType == OrdType.Market ==> !present(this.Price)
    }

which states that for a market order, the Price is not present. The this keyword here refers to the containing message – in this case NewOrderSingle. Also we could write that for a limit order the Price must be present and a valid value:

validate {
         this.OrdType == OrdType.Limit ==>
                (case this.Price
                    {Some price: price > 0.0}
                    {None: false}
                 )
    }

It is not possible to refer to an ignored field – in this case writing this.Account would result in an error.

Declaring outgoing messages

In order to declare a message used for sending we declare an outbound message, similarly to how we declare an inbound message:

outbound message ExecutionReport {
    req OrderID
    req ExecID
    req ExecType
    req OrdStatus
    req Side
    req OrderQtyData.OrderQty
    req LeavesQty
    req CumQty
    opt Text
}

In this case we do not declare any validation statements as the correct output is determined by the logic used to send out such messages. We can declare optionality of the fields using req, opt and ign as for incoming messages.

Handling incoming messages

An incoming message can be valid, in which case it is processed using the receive logic. Alternatively, the message can be invalid, in which case it is handled by the reject logic.

Receiving valid messages

When a message is received we can specify the desired behaviour. In this example we send out an execution report with certain fields set as desired. We have already declared an outbound message ExecutionReport which we will use to send an acknowledgment receipt of the message. We can write a receive block as follows:

receive ( msg : NewOrderSingle ) {
    send ExecutionReport {
        OrderID = msg.ClOrdID;
        ExecID = "";
        ExecType = ExecType.New;
        OrdStatus = OrdStatus.New;
        Side = msg.Side;
        LeavesQty = 0.0;
        OrderQtyData.OrderQty = msg.OrderQtyData.OrderQty;
    }
}

Rejecting invalid messages

In the case of received messages which are invalid with respect to the logic defined in their declaration, there are three possible rejection cases:

Missing Field - where a required field (annotated with req) is not present in the incoming message. In this case it is not possible to reference the incoming message parameter (msg below) as it is not a well-formed message.
Invalid Field - where a received field contravenes one of the validation constraints for that field;
Invalid - where the combination of fields received contravens one of the general message validity constraints

In this example, let us just handle the case where we want to report back with an Execution Report if a field is missing or a field is invalid:

reject (msg:NewOrderSingle, text:string){
    missingfield:{
        send ExecutionReport {
            OrderID = "";
            ExecID = "";
            ExecType = ExecType.New;
            OrdStatus = OrdStatus.New;
            Side = Side.Buy;
            OrderQtyData.OrderQty = 0.0;
            LeavesQty = 0.0;
            CumQty = 0.0;
            Text = Some text;
        }
    }
    invalidfield:{
         send ExecutionReport {
            OrderID = msg.ClOrdID;
            ExecID = "";
            ExecType = ExecType.New;
            OrdStatus = OrdStatus.New;
            Side = Side.Buy;
            OrderQtyData.OrderQty = 0.0;
            LeavesQty = 0.0;
            CumQty = 0.0;
            Text = Some text;
        }
    }
    invalid:{
    }
}

Errors and Warnings

Even in this very simple model it is possible to get errors and warnings. In general these should be interpreted as follows:

Errors: if these occur in the model, then there is a logical inconsistency which means an executable simulator cannot be created.
Warnings: these are advisory pieces of information usually questioning an unusual behaviour.

Examples of errors in this model, are if not all required fields of a sent message are present in a send statement. For example the receive block:

receive ( msg : NewOrderSingle ) {
    send ExecutionReport {
        OrderID = msg.ClOrdID;
        ExecID = "";
        ExecType = ExecType.New;
        OrdStatus = OrdStatus.New;
        OrderQtyData.OrderQty = msg.OrderQtyData.OrderQty;
    }
}

would error with the message:

Not all required fields of the message ExecutionReport
                have been assigned - for example - Side

Examples of a warning would be if we defined ExecutionReport as

outbound message ExecutionReport {
    req OrderID
    opt ExecID
    req ExecType
    req OrdStatus
    req Side
    req OrderQtyData.OrderQty
    opt Text
}

would produce the warning:

The field ExecID is required in the FIX specs, but you are marking it as optional.
Are you sure this is the intended behaviour?

Full Model – Imandra Analysis

Click on the image below for an interactive analysis of this model performed by imandra.

Full Model - IPL Code

The full text of this model for this tutorial section is:

//
//  Imandra Inc.
//  Copyright (c) 2024
//
//  Code for 'Basic Model'
// 
//   
//  For further info see https://docs.imandra.ai
// 
// 


import FIX_4_4

@title: "Basic Model"

messageFlows {
  NewOrderOnly {
      name "NewOrderOnly"
      description "Send NewOrderSingle Message"
	template[NewOrderSingle]
  }
}

message NewOrderSingle {
  req ClOrdID
  req Side
  req TransactTime
  req OrdType valid when it in [ OrdType.Limit, OrdType.Market ]
  req OrderQtyData.OrderQty
  opt Price
  ign Account
  validate {
    (this.OrdType == OrdType.Market <==> !present(this.Price)) &&
         (this.OrdType == OrdType.Limit ==> present(this.Price))
  }
  validate {
    this.OrdType == OrdType.Limit ==>
                (case this.Price
                    {Some price: price > 0.0}
                    {None: false}
                 )
  }
}

outbound message ExecutionReport {
  req OrderID
  req ExecID
  req ExecType
  req OrdStatus
  req Side
  req OrderQtyData.OrderQty
  req LeavesQty
  req CumQty
  opt Text
}

receive (msg:NewOrderSingle){
  send ExecutionReport {
    OrderID = msg.ClOrdID;
    ExecID = fresh();
    ExecType = ExecType.New;
    OrdStatus = OrdStatus.New;
    Side = msg.Side;
    OrderQtyData.OrderQty = msg.OrderQtyData.OrderQty;
    LeavesQty = msg.OrderQtyData.OrderQty;
    CumQty = 0.0;
  }
}

reject (msg:NewOrderSingle, text:string)
{
  missingfield:{
    send ExecutionReport {
      OrderID = fresh();
      ExecID = fresh();
      ExecType = ExecType.New;
      OrdStatus = OrdStatus.New;
      /* we don't have access to the message here as it is
       * incomplete, so we must put in a dummy value as it
       is required in ExecutionReport */
      Side = Side.Buy;
      OrderQtyData.OrderQty = 0.0;
      LeavesQty = 0.0;
      CumQty = 0.0;
      Text = Some text;
    }
  }
    invalidfield, invalid:{
         send ExecutionReport {
            OrderID = msg.ClOrdID;
            ExecID = "REJECTID";
            ExecType = ExecType.New;
            OrdStatus = OrdStatus.New;
            Side = msg.Side;
            OrderQtyData.OrderQty = msg.OrderQtyData.OrderQty;
            LeavesQty = msg.OrderQtyData.OrderQty;
            CumQty = 0.0;
            Text = Some text;
        }
    }
}

Generated Documentation

Click here to view the generated documentation for this model.