tutorialAdvanced.ipl

//
//  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;
    }
  }
}