Module Fix_global_state
type incoming_event
=
|
FIX_Message of Full_messages.full_top_level_msg
|
Internal_Message of Fix_engine_state.fix_engine_int_inc_msg
|
ModelAction of Actions.fix_action
|
Terminate
type fix_global_state
=
{
incoming : incoming_event Lwt_mvar.t;
pub_callback : (Model_messages.model_msg -> Imandra_prelude.unit Lwt.t) option;
engine_state : Fix_engine_state.fix_engine_state;
model_state : State.model_state;
fix_callback : Full_messages.full_top_level_msg -> Imandra_prelude.unit Lwt.t;
}
Global state contains a fix_engine state and model_state
val _pp_incoming : incoming_event -> Imandra_prelude.String.t
val send_all_outgoing_fix : Fix_engine_state.fix_engine_state -> (Full_messages.full_top_level_msg -> Imandra_prelude.unit Lwt.t) -> Fix_engine_state.fix_engine_state Lwt.t
Running Fix_engine.one_step while there are outgoing messages and calling the fix_callback function for each
val send_messages_list : Model_messages.model_msg list -> Fix_engine_state.fix_engine_state -> (Full_messages.full_top_level_msg -> Imandra_prelude.unit Lwt.t) -> (Model_messages.model_msg -> Imandra_prelude.unit Lwt.t) option -> Fix_engine_state.fix_engine_state Lwt.t
Iterating over a list of model messages, pass each into fix_eigine and send anything that fix_engine produces
val while_busy_loop : fix_global_state -> fix_global_state Lwt.t
val main_loop : fix_global_state -> unit Lwt.t
val start : ?pub:(Model_messages.model_msg -> Imandra_prelude.unit Lwt.t) option -> Fix_engine_state.fix_engine_state -> State.model_state -> (Full_messages.full_top_level_msg -> Imandra_prelude.unit Lwt.t) -> incoming_event Lwt_mvar.t * unit Lwt.t