Adding Actions

We now extend our model with messages and actions by adding actions. Actions are constrained, asynchronous events which are produced by a trading venue (for example) which affect the state of the system.

Defining an action

We now introduce two simple actions which correspond to an internal constrained input from the venue or trading system, both of which can update the state.

Fill action

Let us first define, for example a fill action:

action fill {
    fill_price : Price
    fill_qty : Qty

    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 }
        )
    }
}

In this action we represent a fill event from the venue, meaning an order has been processed with a certain fill quantity and fill price. This is represented by the fields fill_price and fill_qty. These two fields do not require initial values as actions are constrained inputs which are assumed to have these values provided by the venue. As well as the fields there are validation statements which ensure that an incoming action is valid. In this case we check that fill price and fill quantity are non-zero and positive. We also check that the price is consistent with the price fields held in the state. For a better explanation of this expression see Option cases.

Book state update

Another action we could define is a message which updates the best bid and best ask of the stock relating to the order on the venue.

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

This action validates that the price updates make sense and rejects the action otherwise.

Receiving Actions

If an action is valid (has passed all the validation statements in its definition) then we can write code which receives the action in the same as we did for receiving a message.

Receiving a fill action

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
        ExecID = "";
        ExecType = ExecType.New;
    }

This action updates the state information about the order in question according to information coming from a fill action event. It then send an ExeuctionReport as an outbound message with the relevant fill information.

Receiving a bookstate action

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

This actions updates the state book best bid and best ask values according to the book state.

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: "Tutorial Model with Actions"

scenario NewOrderFill {
	name "NewOrderFill"
	description "Send NewOrderSingle Message then receive a fill action"
	events[NewOrderSingle, fill]
}

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


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
}

action fill {
    fill_price : Price
    fill_qty : Qty

    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 }
        )
    }
}

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
}

receive (msg:NewOrderSingle) {
    state.live_order = true
    state.LeavesQty = msg.OrderQtyData.OrderQty
    assignFrom(msg,state)

     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.