Module Fix_engine_state
FIX 4.4 engine state type.
type manual_int_data
=
{
session_reset : bool;
}
Define set of actions + data for manual intervention by the user.
type session_data
=
{
dest_comp_id : Imandra_prelude.string;
Destination company ID.
reset_seq_num : bool;
Shall we reset sequence numbers?
}
Request to initiate a new session.
type fix_engine_int_inc_msg
=
|
IncIntMsg_TimeChange of TimeDefaults.fix_utctimestamp
Updates internal time of the engine.
|
IncIntMsg_CreateSession of session_data
Create sessions command.
|
IncIntMsg_EndSession
Terminate current active session.
|
IncIntMsg_ApplicationData of Full_app_messages.full_app_msg_data
App messages to be transmitted over.
|
IncIntMsg_ManualIntervention of manual_int_data
TODO: create 'richer' manual commands.
These are internal messages into the Engine.
type fix_engine_int_out_msg
=
|
OutIntMsg_ApplicationData of Full_app_messages.full_app_msg_data
Sending application message
|
OutIntMsg_ResendApplicationData of Full_app_messages.full_app_msg_data
Sending application message that was flagged as a possible resend
|
OutIntMsg_Reject
Rejecting internal message - when we cannot transmit or create new sessions, etc.
These are the outgoing internal messages - would be sent into the application model.
type fix_engine_status
=
|
Normal
|
SessRejectReceived
|
BusinessRejectReceived
|
TargetAppIsDown
|
ConnTerminatedWithoutLogoff
|
MaxNumLogonMsgsViolated
Represents 'status' of the engine.
type fix_engine_mode
=
Represents 'modes' of the engine.
type fix_engine_state
=
{
fe_curr_status : fix_engine_status;
Status.
fe_curr_mode : fix_engine_mode;
High-level mode of the engine.
fe_initiator : bool option;
initiator = True if we've received an internal message to initiate the connection. It's False if we've received a Logon request first. It's None by default prior to any Logon sequences.
fe_curr_time : TimeDefaults.fix_utctimestamp;
Need to define time so we're aware of heartbeat status.
fe_comp_id : Imandra_prelude.string;
Our company ID
fe_target_comp_id : Imandra_prelude.string;
Target company ID
fe_sender_location_id : Imandra_prelude.string option;
Location id string
fe_on_behalf_of_comp_id : Imandra_prelude.string option;
On behalf of string
incoming_int_msg : fix_engine_int_inc_msg option;
Incoming internal messages (application).
outgoing_int_msg : fix_engine_int_out_msg option;
These are messages we send back to our owner
incoming_seq_num : Imandra_prelude.int;
Sequence number of the last processed incoming message.
outgoing_seq_num : Imandra_prelude.int;
Sequence number of the last sent message.
incoming_fix_msg : Full_messages.full_top_level_msg option;
Messages we will send out
outgoing_fix_msg : Full_messages.full_top_level_msg option;
Messages we receive
fe_cache : Full_messages.full_valid_fix_msg list;
Maintain a cache of messages in case we detect out-of-sequence message(s).
fe_history : Full_messages.full_valid_fix_msg list;
We maintain history of our outgoing messages in case we're asked to retransmit.
fe_last_time_data_sent : TimeDefaults.fix_utctimestamp;
Last time we sent out data to the corresponding engine
fe_last_data_received : TimeDefaults.fix_utctimestamp;
Last time we received a heartbeat or other message.
fe_heartbeat_interval : Datetime.fix_duration;
Negotiated heartbeat interval.
fe_testreq_interval : Datetime.fix_duration;
Interval used to 'pad' heartbeat interval before a TestRequest message is sent out.
fe_retransmit_start_idx : Imandra_prelude.int;
Starting index of the retransmitting history.
fe_retransmit_end_idx : Imandra_prelude.int;
Ending index ...
fe_history_to_send : Full_messages.full_valid_fix_msg list;
Used in message retransmission.
fe_mode_after_resend : fix_engine_mode;
Which mode should we go to after resend is completed?
fe_application_up : bool;
Is the application that's receiving messages up and running? TODO: we might need to constitute a heartbeat to enforce this.
last_test_req_id : Imandra_prelude.string;
These are used to send out TestRequest messages that should be replied with Heartbeat messages containing the testrequest ID. Any string may be used, we use int's for now.
fe_num_logons_sent : Imandra_prelude.int;
Number of logons sent during session initialization. This is done to ensure that the engine does not go into infinite loop.
fe_max_num_logons_sent : Imandra_prelude.int;
Setting: maximum number of logons to be sent out.
fe_encrypt_method : Full_admin_enums.fix_encryption_method;
}
Engine state structure containing all of the information required for it operate.
val init_fix_engine_state : fix_engine_state
Initial engine state.
val engine_state_busy : fix_engine_state -> bool
THEOREM: one_step calls on busy state eventually terminate
val is_state_valid : fix_engine_state -> bool
Properties of a valid state.
TODO: augment these properties and verify that if we're in a good state, cannot transition out of it (i.e. new state would always be valid).
TODO: once we have the full library of checks for incoming messages we need to maintain that every state transition from a valid state would result in another valid state.