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 =
| NoActiveSession

State of the engine before logon.

| LogonInitiated

Middle of logon session.

| ActiveSession

Application messages are now processed.

| GapDetected

Detected out-of-sequence message. Sending out ResendRequest.

| Recovery

RequestResend has been sent out. Waiting to recover the messages, filling int the cache..

| CacheReplay

Replaying the cache.

| Retransmit

Retransmitting sequence of messages because we were asked to retransmit.

| ShuttingDown

We'll nees to send a logoff message adn transition to ShutdownInitiated.

| ShutdownInitiated

Shutting-down protocol.

| Error
| WaitingForHeartbeat

Sent out TestRequest message.

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.