ordersWithFillsSet.ipl

//
//  Imandra Inc.
//  Copyright (c) 2024
//
//  Minimal FIX 4.4 model with fills
//
// 
//  For further info see https://docs.imandra.ai
//
//

import FIX_4_4

// This makes no sense in a real circumstance
// but demonstrates how multiple values can be overridden and defined
@encoding: MultipleValueChar
extend enum OrdType {
}

// Import inbound NewOrderSingle message
message NewOrderSingle {
    req ClOrdID valid when it in ["a","n"]
    req Side
    req TransactTime
    req OrdType
         valid when it in [{| OrdType.Limit, OrdType.Market |},{|OrdType.Limit|},{|OrdType.Market|}]
         valid when subset(it,{| OrdType.Limit, OrdType.Market |})
    req OrderQtyData.OrderQty valid when it > 0.0
    opt Price

    validate { state.live_order == false }

    validate { state.OrdStatus in [ OrdStatus.New ]}

    // For Limit orders, Price must be positive.
    validate {
         OrdType.Limit in this.OrdType ==>
                (case this.Price
                    {Some price: price > 0.0}
                    {None: false}
                 )
    }


    // For Market orders, Price must not be present.
    validate {
         OrdType.Market in this.OrdType  ==> !present(this.Price)
    }
}

// Import an outbound message ExecutionReport
outbound message ExecutionReport {
    req OrderID
    req ExecID
    req ExecType
    req OrdStatus
    req Side
    req LeavesQty
    req CumQty
    req AvgPx
}

// Define the interface state
internal state {

    // The following fields would be assigned to
    assignable {
        OrdStatus   : OrdStatus = OrdStatus.New;
        Side        : Side = Side.Buy;
        OrderID     : string = "";
        LeavesQty   : Qty = 0.0;
        CumQty      : Qty = 0.0;
        AvgPx       : Price = 0.0;
        Price       :? Price = None;
        OrdType     : OrdType
        OrderQtyData.OrderQty : Qty
    }

    live_order : bool = false;

    // These are not required within the orders, etc...
    filledQty : Qty = 0.0;
    current_time : UTCTimeOnly = UTCTimeOnly (8, 0, 0, None);

    // Define the opening and closing times
    opening_time : UTCTimeOnly = UTCTimeOnly (8, 0, 0, None);
    closing_time : UTCTimeOnly = UTCTimeOnly (16, 0, 0, None);
}

//  Define how the model should process a validated
//  incoming NewOrderSingle message
receive ( msg : NewOrderSingle ) {

    // Extract all relevant fields from within the message
    assignFrom (msg, state)

    state.LeavesQty = msg.OrderQtyData.OrderQty
    state.live_order = true

    send ExecutionReport {
        state with
            ExecID = "";
            ExecType = ExecType.New;
    }

}

// Handle rejections for 'NewOrderSingle'
reject ( msg : NewOrderSingle, rejectReason : string ) {

    // A field is missing
    missingfield : {
         send ExecutionReport {
            state with
                ExecID = "";
                ExecType = ExecType.Rejected;
        }
    }

    invalidfield : {
        send ExecutionReport {
            state with
                ExecID = "";
                ExecType = ExecType.Rejected;
        }
    }

    // One or more 'validate' statements is invalid
    invalid : {
        send ExecutionReport {
            state with
                ExecID = "";
                ExecType = ExecType.Rejected;
        }
   }
}

// Define action 'time_change'
action time_change {
    new_time : UTCTimeOnly

    validate { this.new_time <= state.closing_time }

    validate { this.new_time >= state.current_time }
}

// Define logic for handling this 'time_change' action
receive ( act : time_change ) {
    // Save the new time into internal state
    state.current_time = act.new_time

    // If it's past closing time, then cancel the order and send
    // out the ExecutionReport
    if ( act.new_time >= state.closing_time && state.OrdStatus != OrdStatus.Filled ) then {
        state.OrdStatus = OrdStatus.Expired
        state.live_order = false

        send ExecutionReport {
            state with
                ExecID = "";
                ExecType = ExecType.New;
        }
    }
}

//
// Define action 'fill'
//
action fill {

    fill_price : Price
    fill_qty : Qty

    validate { this.fill_qty > 0.0 && this.fill_qty <= state.LeavesQty }

    validate { this.fill_price > 0.0 }

    validate {
        (OrdType.Limit in state.OrdType) ==>
        ( case state.Price
              { Some p:
                    if ( state.Side == Side.Buy ) then
                        ( this.fill_price <= p )
                    else ( this.fill_price >= p )
              }
              { None: true }
        )
    }

}

// Receiving fills and sending out
receive ( f : fill ) {

    state.LeavesQty = state.LeavesQty - f.fill_qty
    state.filledQty = state.filledQty + f.fill_qty

    state.AvgPx = ( state.AvgPx * state.filledQty + f.fill_qty * f.fill_price ) / ( f.fill_qty + state.filledQty )

    if state.LeavesQty == 0.0 then
        state.OrdStatus = OrdStatus.Filled
    else
        state.OrdStatus = OrdStatus.PartiallyFilled

    send ExecutionReport { state with
        ExecID = "";
        ExecType = ExecType.New;
    }
}