tutorialState.ipl

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

import FIX_4_4

@title: "Tutorial State Model"

messageFlows {
  NewOrderOnly {
    name "NewOrderOnly"
    description "Send NewOrderSingle Message"
    template[NewOrderSingle]
  }
}

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

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
}

receive (msg:NewOrderSingle){
  state.live_order = true
  state.LeavesQty = msg.OrderQtyData.OrderQty
  state.OrderID = fresh()
  state.OrdStatus = OrdStatus.New
  assignFrom(msg,state)
  send ExecutionReport {
    state with
    ExecID = fresh();
    ExecType = ExecType.New;
  }
}

reject (msg:NewOrderSingle, text:string)
{
  missingfield:{
    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;
        }
    }
}