Custom Message Fields and Cases

For specific venues and trading systems, it is important to allow the creation of extra message fields, record field and enum cases. This section shows declaring such artifacts can be done, and how it integrates with the rest of the specification.

Custom Enum cases

In our model we have make use of the OrdType enum in order to refer to the type of order. Let us say we want to introduce a new order type called StopSpread which is a type of limit order intended to only be entered onto an order book once the spread is less than a certain preset amount defined as a proportion of the best bid price. After a fill the rest of the order is set as a normal limit order at the price of the fill.

In order to extend the OrdStatus enum we write a custom extension:

extend enum OrdType {
    StopSpread "s"
}

here we define a new tag “s” which will indicate this type of order on the wire.

Once a StopSpread order has been entered onto the book, the OrdStatus field of the state becomes OrdStatus.New and remains as this even if the spread changes.

Custom Message Fields

In order to incorporate the custom enum case into the model, we need to extend the NewOrderSingle message to add a field which records the spread proportion figure. We do this first by extending the message declaration:

extend message NewOrderSingle {
    SpreadProportion "10001" :? float
}

Then we can import it into the message and add some validation to the inclusion of the field, adding some validation conditions - that the proportion is strictly between 0 and 1, also we ensure that a price is present for this type of order.

message NewOrderSingle {
    req ClOrdID
    req Side
    req TransactTime
    req OrdType valid when it in [ OrdType.Limit, OrdType.Market, StopSpread ]
    req OrderQtyData.OrderQty
    opt SpreadProportion valid when case(it){None:true}{Some x: x>0.0 &&  x<1.0}
    opt Price 
    ign Account

     validate {
         (this.OrdType == OrdType.Market <==> !present(this.Price)) &&
         (this.OrdType == OrdType.Limit ==> present(this.Price)) &&
         (this.OrdType == OrdType.StopSpread ==> present(this.Price))
    }

     validate {
        this.OrdType == StopSpread ==>
            present(this.SpreadProportion)
    }

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

Updating the state

We now need to update the state so that the spread proportion can be recorded throughout the life of the order:

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

Updating receive code

Now we are adding order types which have a more complex logic, we need to update the code we write when receiving a NewOrderSingle message, and a bookState action.

Updating `NewOrderSingle` receive code

We update the receive code to change the OrdStatus of the state if the spread between the current best bid and best ask is already within that specified by the SpreadProportion of the initial order.

receive (msg:NewOrderSingle) {
    state.live_order = true
    state.LeavesQty = msg.OrderQtyData.OrderQty
    state.OrderID = fresh()
    assignFrom(msg,state)
    if msg.OrdType == StopSpread
    then
        case(msg.SpreadProportion)
        {Some x:
        if state.bestAsk != 0.0 &&
            x >= (state.bestAsk - state.bestBid)/state.bestAsk
            then
            {
                state.OrdStatus = OrdStatus.New
                state.ExecType = ExecType.New
            }
    }
    send ExecutionReport {
        state with
        ExecID = fresh();
    }
}

If the spread is already within the specified SpreadProportion then the OrdStatus is updated to New otherwise is it set as PendingNew.

Updating the `bookState` action receive code

When the best bid and best ask prices are updated we check whether the order is of type StopSpread and if so we determine if the OrdStatus of the state should be updated:

receive (ba:bookState){
    state.bestBid = ba.bestBid
    state.bestAsk = ba.bestAsk

    let spread = (state.bestAsk - state.bestBid)/state.bestAsk
    if 
    (case(state.SpreadProportion){None:false}{Some x: x >= spread}) &&
        state.OrdStatus == OrdStatus.PendingNew
        then state.OrdStatus = OrdStatus.New
}

Updating `fill` action validation

An order with OrdStatus == OrdStatus.PendingNew indicates that it is not eligible to be filled. We add a validation to ensure that the action is not taken in this case:

action fill {
    fill_price : Price
    fill_qty : Qty
    validate {
        state.OrdStatus != OrdStatus.PendingNew
    }
    validate {
        this.fill_qty > 0.0
    }
    validate {
        this.fill_qty <= state.LeavesQty
    }
    validate {
        this.fill_price > 0.0
    }
    validate {
        if ( state.Side == Side.Buy ) 
        then ( this.fill_price >= state.bestAsk )
        else ( this.fill_price <= state.bestBid )
    }
    validate {
        (state.OrdType != OrdType.Market) ==>
        ( case state.Price
              { Some p:
                    if ( state.Side == Side.Buy ) then
                        ( this.fill_price <= p )
                    else ( this.fill_price >= p )
              }
              { None: true }
        )
    }
}

Errors and Warnings

Ipl will check that tags are consistent. This means that if you use a field tag which corresponds to an existing field with a different name, it will error. It also does this check for enum case tags. This is crucial to ensure the resulting system is sound when executed as a simulator. If for example you were to add the custom field as

extend message NewOrderSingle {
    SpreadProportion "11" :? float
}

you would receive an error saying:

Field SpreadProportion has tag 11, but a field with the same tag but name ClOrdID already exists.

this ensuring the correctness of the generated model.

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 'Custom Extensions Tutorial Model'
// 
//   
//  For further info see https://docs.imandra.ai
// 
// 

import FIX_4_4

@title: "Custom Extensions Tutorial Model"

messageFlows {
  NewOrderFill {
    name "NewOrderFill"
    description "Initialise Book State, send NewOrderSingle Message then receive a fill action"
    template[bookState, NewOrderSingle, fill]
  }
}

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

extend enum OrdType {
  StopSpread "s"
}

extend message NewOrderSingle {
  SpreadProportion "10001" :? float
}

message NewOrderSingle {
  req ClOrdID
  req Side
  req TransactTime
  req OrdType valid when it in [ OrdType.Limit, OrdType.Market, StopSpread ]
  req OrderQtyData.OrderQty
  opt SpreadProportion valid when case(it){None:true}{Some x: x>0.0 &&  x<=1.0}
  opt Price
  ign Account
  opt ExecInst default = {|ExecInst.Held|}
  validate {
    (this.OrdType == OrdType.Market <==> !present(this.Price)) &&
         (this.OrdType == OrdType.Limit ==> present(this.Price)) &&
         (this.OrdType == OrdType.StopSpread ==> present(this.Price))
  }
  validate {
    this.OrdType == StopSpread <==>
            present(this.SpreadProportion)
  }
  validate {
    this.OrdType != OrdType.Market ==>
                (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
}

action fill {
  fill_price : Price
  fill_qty : Qty
  validate {
    state.OrdStatus != OrdStatus.PendingNew
  }
  validate {
    this.fill_qty > 0.0
  }
  validate {
    this.fill_qty <= state.LeavesQty
  }
  validate {
    this.fill_price > 0.0
  }
  validate {
    if ( state.Side == Side.Buy ) 
        then ( this.fill_price >= state.bestAsk )
        else ( this.fill_price <= state.bestBid )
  }
  validate {
    (state.OrdType != OrdType.Market) ==>
        ( case state.Price
              { Some p:
                    if ( state.Side == Side.Buy ) then
                        ( this.fill_price <= p )
                    else ( this.fill_price >= p )
              }
              { None: true }
        )
  }
}

action bookState {
  bestBid : Price
  bestAsk : Price
  validate{
    this.bestAsk > this.bestBid &&
        this.bestBid > 0.0 &&
        this.bestAsk > 0.0
  }
}

receive (f:fill) {
  state.LeavesQty = state.LeavesQty - f.fill_qty
  state.AvgPx = ( state.AvgPx * state.CumQty + f.fill_qty * f.fill_price ) / ( f.fill_qty + state.CumQty )
  state.CumQty = state.CumQty + f.fill_qty
  if state.LeavesQty == 0.0 then
    {
      state.OrdStatus = OrdStatus.Filled
      state.ExecType = ExecType.Trade
    }
  else
    {
      state.OrdStatus = OrdStatus.PartiallyFilled
      state.ExecType = ExecType.Trade
    }
  send ExecutionReport {
    state with
    ExecID = fresh();
  }
}

receive (ba:bookState){
  state.bestBid = ba.bestBid
  state.bestAsk = ba.bestAsk
  let spread = (state.bestAsk - state.bestBid)/state.bestAsk
  if 
    (case(state.SpreadProportion){None:false}{Some x: x >= spread}) &&
        state.OrdStatus == OrdStatus.PendingNew
        then
    state.OrdStatus = OrdStatus.New
}

receive (msg:NewOrderSingle) {
  state.live_order = true
  state.LeavesQty = msg.OrderQtyData.OrderQty
  state.OrderID = fresh()
  assignFrom(msg,state)
  if msg.OrdType == StopSpread
    then
    case(msg.SpreadProportion)
    {Some x:
        if state.bestAsk != 0.0 &&
            x >= (state.bestAsk - state.bestBid)/state.bestAsk
            then
      {
        state.OrdStatus = OrdStatus.New
        state.ExecType = ExecType.New
      }
    }
  send ExecutionReport {
    state with
    ExecID = fresh();
  }
}

reject (msg:NewOrderSingle, text:string)
{
  missingfield:{
    state.ExecType = ExecType.Rejected
    state.OrdStatus = OrdStatus.Rejected
    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.