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 {
        if ( state.Side == Side.Buy ) 
        then ( this.fill_price >= state.bestAsk )
        else ( this.fill_price <= state.bestBid )
    }
    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
            state.ExecType = ExecType.Trade
       }
    else
        {
            state.OrdStatus = OrdStatus.PartiallyFilled
            state.ExecType = ExecType.Trade
        }
    send ExecutionReport {
        state with
        ExecID = fresh();
    }
}

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

//
//  Imandra Inc.
//  Copyright (c) 2024
//
//  Code for 'Tutorial Model with Actions'
//   
//  For further info see https://docs.imandra.ai
// 
// 
//


import FIX_4_4

@title: "Tutorial Model with Actions"

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

internal state {
  assignable{
    Side                  :  Side      = Side.Buy;
    Price                 :? Price
    OrderQtyData.OrderQty :  Qty       = 0.0;
    OrdStatus             :  OrdStatus = OrdStatus.PendingNew;
    OrdType               :  OrdType   = OrdType.Market;
    LeavesQty             :  Qty       = 0.0;
    CumQty                :  Qty       = 0.0;
    OrderID               :  string
    ExecType              :  ExecType  = ExecType.PendingNew;
  }
  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 {
    if ( state.Side == Side.Buy ) 
    then ( this.fill_price >= state.bestAsk )
    else ( this.fill_price <= state.bestBid )
  }
  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
      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
}

receive (msg:NewOrderSingle) {
  state.live_order = true
  state.LeavesQty = msg.OrderQtyData.OrderQty
  state.OrderID = fresh()
  state.OrdStatus = OrdStatus.New
  state.ExecType = ExecType.New
  assignFrom(msg,state)
  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.