-
Notifications
You must be signed in to change notification settings - Fork 1
/
ambiguousOptionalitySimple.ipl
102 lines (82 loc) · 2.5 KB
/
ambiguousOptionalitySimple.ipl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
//
// Imandra Inc.
// Copyright (c) 2024
//
// Minimal FIX 4.4 model with minimal example optional
// and ambiguous import logic
//
// For further info see https://docs.imandra.ai
//
//
import FIX_4_4
// Import inbound NewOrderSingle message
message NewOrderSingle {
req ClOrdID
req Side
req TransactTime
req OrdType valid when it in [ OrdType.Limit, OrdType.Market ]
req OrderQtyData.OrderQty
// Price is imported non-optionally
req Price
validate { state.live_order == false }
validate { state.OrdStatus in [ OrdStatus.New ]}
}
// Import an outbound message ExecutionReport
outbound message ExecutionReport {
req OrderID
req ExecID
req ExecType
req OrdStatus
req Side
req LeavesQty
req CumQty
req AvgPx
// Price and DayAvgPx are optionally imported
opt Price
opt DayAvgPx
}
// Define the interface state
internal state {
// The following fields would be assigned to
assignable {
OrdStatus : OrdStatus = OrdStatus.New;
Side : Side
OrderID : string
LeavesQty : Qty
CumQty : Qty
AvgPx : Price
// Price is imported optionally and non-optionally
// It can be used in assignable and has "ambiguous type (:*)"
// which means it can only be set using a non-optional value
Price :* Price = 0.0;
OrdType : OrdType = OrdType.Limit;
// DayAvgPx is imported optionally (:?)
DayAvgPx :? Price
}
live_order : bool = false;
// These are not required within the orders, etc...
OrdQty : Qty = 0.0;
filledQty : Qty = 0.0;
current_time : UTCTimeOnly = UTCTimeOnly (8, 0, 0, None);
temp_Price : Price = 0.0;
// 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.live_order = true
// reset the DayAvgPx if below a certain figure
state.temp_Price = case (state.DayAvgPx) {Some x : x} {None : 0.0}
if state.temp_Price > 10.0
then state.DayAvgPx = Some state.temp_Price
else state.DayAvgPx = None
send ExecutionReport {
state with
ExecID = "";
ExecType = ExecType.New;
}
}