Introducing State

We now extend our basic model with the concept of a state. The way to conceptualize the model as a whole is a state transition system. This means that for any event (see Messages and Actions) the state can be updated. Remember that the state here represents information pertaining to one order. There is no current requirement to provide initial values in the state, but it should be noted that those fields which have no explicit initial value are provided with a generated value. It is recommended that values with no initial value are either those which are initialised via an incoming message, or are initialised via an action as discussed for example in the Adding Actions section.

State initialisation

Let us first construct a state in our basic model (here we use the canonical name state but there can be many such global states with any name):

internal state {
    Side : Side
    Price :? Price
    live_order : bool = false;
}

Here we have introduced two fields: side which is of type Side, which is not optional, and price of type Price which is optional. It is important to note that initial values on fields are not required and if are not present, a candidate is generated upon analysis. In this example, live_order has been given an initial value of false, where are Side and Price don’t have initial values specified.

Assignment to and from state

In the basic model we can now use the declared state variable as a way of storing information. For example in the message receive block we can write

receive (msg:NewOrderSingle){
    state.live_order = true
    state.Side = msg.Side
    state.Price = msg.Price

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

Note here how state has been updated with values from the incoming message, and state can be used to populated values of the outbound ExecutionReport.

Automatic assignment using state

It is possible to define a special subset of state variables which can be used to automatically update to and from the state. In order to do this we create an assignable section which contains fields which have been imported via messages. For example we can create the following state:

internal state {
    assignable{
        Side                  :  Side
        Price                 :? Price
        OrderQtyData.OrderQty :  Qty
        OrdType               :  OrdType
        OrdStatus             :  OrdStatus = OrdStatus.PendingNew;
        ExecType              :  ExecType  = ExecType.PendingNew;
        LeavesQty             :  Qty
        CumQty                :  Qty
        OrderID               :  string
    }
    live_order : bool = false;
    AvgPx : float
    bestBid : float
    bestAsk : float
}

where we declare fields common to both outgoing and incoming messages in the assignable section of the state. It is now possible to exploit this when processing messages. For example we could rewrite the message receive to be:

receive (msg:NewOrderSingle){
    state.live_order = true
    state.LeavesQty = msg.OrderQtyData.OrderQty
    state.OrderID = fresh()
    state.OrdStatus = OrdStatus.New
    assignFrom(msg,state)
    send ExecutionReport {
        state with
        ExecID = fresh();
        ExecType = ExecType.New;
    }
}

Note here using this syntax the fields declared in the assignable section of state are automatically updated using the assignFrom directive. In the send command, the insertion of the {state with syntax uses the fields from the assignable section of state to automatically set the fields of ExecutionReport. In this case the fields Side and OrderQtyData.OrderQty are set automatically.

Errors and Warnings

As before it is possible to encounter errors and warnings in this model. Those that are most pertinent here to the creation of an internal state are

Assignable field errors

The only fields that can exist in the assignable section of state are fields that have been imported in a message. One cannot place an arbitrary field such as live_order in the assignable section and the following error will appear if it is placed there:

Couldn't resolve reference to MessageRequire 'live_order'

Assignable field optionality errors

If the optionality of an assignable field does not match the corresponding message field, then an error will occur. For example if the assignable field

 Price:Price = 0.0;

Then the following error will be given:

This field should be defined as optional.

It is possible to deal with the situation where a field is imported both non-optionally and optionally in messages. This is discussed in the advanced section Ambiguous optionality

Full Model – Imandra Analysis

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

Full Model - IPL Code

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

import FIX_4_4

@title: "Tutorial State Model"

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

internal state {
  assignable{
    Side                  :  Side
    Price                 :? Price
    OrderQtyData.OrderQty :  Qty
    OrdType               :  OrdType
    OrdStatus             :  OrdStatus = OrdStatus.PendingNew;
    ExecType              :  ExecType  = ExecType.PendingNew;
    LeavesQty             :  Qty
    CumQty                :  Qty
    OrderID               :  string
  }
  live_order : bool = false;
  AvgPx : float
  bestBid : float
  bestAsk : float
}

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){
  state.live_order = true
  state.LeavesQty = msg.OrderQtyData.OrderQty
  state.OrderID = fresh()
  state.OrdStatus = OrdStatus.New
  assignFrom(msg,state)
  send ExecutionReport {
    state with
    ExecID = fresh();
    ExecType = ExecType.New;
  }
}

reject (msg:NewOrderSingle, text:string)
{
  missingfield:{
    send ExecutionReport {
      state with
      ExecID = fresh();
      Text = Some text;
    }
  }
    invalidfield, invalid:{
        state.ExecType = ExecType.Rejected
        state.OrdStatus = OrdStatus.Rejected
        send ExecutionReport {
            state with
            ExecID = fresh();
            Text = Some text;
        }
    }
}

Generated Documentation

Click here to view the generated documentation for this model.