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 : float 
        OrdStatus:OrdStatus = OrdStatus.New;
        OrdType:OrdType 
        LeavesQty:Qty 
        CumQty:Qty 
        SpreadProportion:?float
        Parties:Parties
        ExecInst :* ExecInst = ExecInst.Held;
    }
    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

import FIX_4_4
@title: "Advanced Tutorial Model"

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

VerificationPacks[EmptyString,Venue]

precision(Price,2)

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

extend enum OrdType {
    StopSpread "s"
}

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

extend record Parties {
    req NoPartyIDs
    req PartyID
    PartyIndex "pi" : int
}

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 = Some [ExecInst.Held, ExecInst.AllOrNone]
    req Parties valid when it.PartyIndex > 0 && it.PartyIndex < 100
                valid when it.PartyID != ""
    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 {
        (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
    else
        state.OrdStatus = OrdStatus.PartiallyFilled

    send ExecutionReport { state with
        OrderID = "";
        ExecID = "";
        ExecType = ExecType.New;
    }
}
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
    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 
            else state.OrdStatus = OrdStatus.PendingNew
        else state.OrdStatus = OrdStatus.PendingNew
    }

     send ExecutionReport {state with 
        OrderID = msg.ClOrdID;
        ExecID = "";
        ExecType = ExecType.New;
    }
}

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

Generated Documentation

Click here to view the generated documentation for this model.