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 "sp" :? 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.New;
        OrdType:OrdType 
        LeavesQty:Qty 
        CumQty:Qty 
        SpreadProportion:?float
    }
    live_order : bool = false;
    AvgPx : float 
    bestBid: Price 
    bestAsk: Price 
}

Updaing 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
    assignFrom(msg,state)

    if msg.OrdType == StopSpread
    then case(msg.SpreadProportion){Some x:
        if state.bestAsk != 0.0 then
        if x >= (state.bestBid - state.bestAsk)/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;
    }
}

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 a fill action to ensure that the action not be produces for such an order:

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.Limit) ==>
        ( 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

import FIX_4_4
@title: "Custom Extensions Tutorial Model"

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

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

extend enum OrdType {
    StopSpread "s"
}

extend message NewOrderSingle {
    SpreadProportion "sp" :? 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 = Some [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 {
        (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 = "";
            ExecID = "";
            ExecType = ExecType.New;
            Text = Some text;
        }
    }
    invalidfield:{
         send ExecutionReport {state with
            OrderID = msg.ClOrdID;
            ExecID = "";
            ExecType = ExecType.New;
            Text = Some text;
        }
    }
    invalid:{
    }
}

Generated Documentation

Click here to view the generated documentation for this model.