Advanced Features

We now have a full model which receives messages and actions, including custom fields, enum cases, and custom repeating group fields. In this last section we discuss more advanced functionality available.

Ambiguous optionality

It is possible to import a field in the assignable section of an internal state declaration which is declared both optionally and non-optionally in the model.

Mismatched optionality imported message fields

For example let us import the field ExecInst in NewOrderSingle:

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
}

and let us declare the field in the ExecutionReport as required, as we want to it to always be present in any outgoing message:

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

Adding ambiguous optionality fields to the state

Now if we add the ExecInst field to the state we need to use ambiguous notation for the type to denote that the field is both optional and non-optional. We do this using :* notation - such fields require stated initial values to be non-optional:

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

Declaring default values

In the situation above we must provide a default value for an optional field in an incoming message which corresponds to an assignable field - this is so that a value can be provided for a required value in an outgoing message. Failure to do see will result in the error

This message require needs a default value as it is optional but used to assign an ambiguous state value

For NewOrderSingle we thus write:

opt ExecInst default = Some Held

to provide such a value.

Verification Packs

A verification pack is something you might want to prove about your model. An example would be that any transition of the OrdStatus fields of the state is valid - for example that once an order is cancelled, it does not become reactivated. There are a set of such verification goals pre-written which users can activate for analysis by imandra. The existing set of such goals is

EmptyString - checks that no outbound string values are the empty string - which is not allowed in the FIX specs;
Venue - checks that any transition of OrdStatus field of the state is valid. The way to specify a verfication pack is

VerificationPacks[EmptyString,Venue]

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

import FIX_4_4

@title: "Advanced Tutorial Model"

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

VerificationPacks[EmptyString,Venue]

precision(Price,2)

internal state {
  assignable{
    Side                  :  Side
    Price                 :? Price
    OrderQtyData.OrderQty :  Qty
    OrdStatus             :  OrdStatus = 
    OrdStatus.PendingNew;
    OrdType               :  OrdType
    LeavesQty             :  Qty
    CumQty                :  Qty
    SpreadProportion      :? float
    Parties               :  Parties
    ExecInst              :  ExecInst
    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
}

extend record Parties {
  PartyIndex "10002" : int
}

repeatingGroup Parties {
  req NoPartyIDs
  req PartyID
  req PartyIndex
  req PtysSubGrp
}

repeatingGroup PtysSubGrp {
  opt NoPartySubIDs
  req PartySubIDType
  opt PartySubID
}

message NewOrderSingle {
  opt ClOrdID valid when it != (Some "N/A")
  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
  opt Account
  opt ExecInst default = {|ExecInst.Held, ExecInst.AllOrNone|}
  req Parties valid when it.PartyIndex > 0 && it.PartyIndex < 100
                valid when it.PartyID != "N/A"
  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}
                 )
  }
  validate {
    case(this.Parties.PtysSubGrp.PartySubID)
            {None:true}
            {Some x : this.Parties.PartyID != x}
  }
}

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

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()
  state.ExecType = ExecType.New
  assignFrom(msg,state)
  if msg.OrdType == StopSpread
    then
    case(msg.SpreadProportion)
    {Some x:
        if state.bestAsk != 0.0 then
      if 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.