Module `Fix_engine_transitions`

FIX 4.4 engine transition functions.

val logoff_and_shutdown : Fix_engine_state.fix_engine_state -> Fix_engine_state.fix_engine_state: In many abnormal cases we need to send out the Logout messages and transition to ShutdownInitiated state.

val make_resend_message : (Full_messages.full_valid_fix_msg * TimeDefaults.fix_utctimestamp * Imandra_prelude.int) -> Full_messages.full_valid_fix_msg

Before sending out a historic message, we need to:

move the sequence number if it is too low
set PossibleDuplicate flag
move historic SendingTime to OrigSendingTime
update SendingTime

val run_retransmit : Fix_engine_state.fix_engine_state -> Fix_engine_state.fix_engine_state: We're in the middle of retransmitting historic messages. Note: when we transition into Retransmit mode, we set up a queue with messages that should be sent out. These messages are a function of the parameters that were sent to the engine.

val run_no_active_session : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: Here we will only accept an incoming Logon message to establish a connection.

val run_logon_sequence : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state
val initiate_Resend : (Fix_engine_state.fix_engine_mode * Full_admin_messages.full_msg_resend_request_data * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: Response to resend request. Note that we're copyng over the whole list of historic messages - we will use the starting/ending indexes to ensure we're only sending out the right ones. Perhaps there's a better way to do this - it's important that we always maintain the spirit of 'one_step' - all operations are are atomic.

val attempt_sequence_reset : (Fix_engine_state.fix_engine_state * Imandra_prelude.int * Imandra_prelude.int) -> Fix_engine_state.fix_engine_state
val run_active_session : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: We're operating in a normal mode.

val run_wait_heartbeat : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: We've force-requested a heartbeat message from the other end and waiting for it to come. TODO: We're ignoring all other messages -- check the specs if that is a correct behavior

val run_gap_detected : Fix_engine_state.fix_engine_state -> Fix_engine_state.fix_engine_state: We're in a GapDetected state. Sending out resend request and transitioning into Recovery.

val replay_single_msg : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: Here we can only handle a subset of the FIX messages.

val run_cache_replay : Fix_engine_state.fix_engine_state -> Fix_engine_state.fix_engine_state

Run the engine through the replay messages. This is used during recovery.

Note that the only session-level message we should receive at this point should be a Reject message. We need to ensure that this function cannot lead to another Recovery state.

val no_seq_gaps : (Full_messages.full_valid_fix_msg list * Imandra_prelude.int) -> bool: Check to make sure there're no sequence gaps

val is_cache_complete : (Full_messages.full_valid_fix_msg list * Imandra_prelude.int) -> bool

Is cache valid so that we can transition from recovery?

Cache is considered valid when: 1. It is non-empty 2. The sequence IDs of the messages within cache are continuous (i.e. there're no gaps) 3. First sequence ID (of the cache) is next message from the last one correctly processed.

val add_to_cache : (Full_messages.full_valid_fix_msg * Full_messages.full_valid_fix_msg list) -> Full_messages.full_valid_fix_msg list: Add message to cache so that ordering is maintained.

val run_recovery : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: We're in recovery mode. Logoff and ResendRequest messages must be processed. We should add any other received messages are addted to the cache. Transition to CacheReplay when the cahce is complete.

val run_shutdown : (Full_messages.full_valid_fix_msg * Fix_engine_state.fix_engine_state) -> Fix_engine_state.fix_engine_state: We've sent out a Logout message and are now waiting for a confirmation of logout.