Module Event

module Event: sig .. end
Event logging and communication


Every relevant event must be logged through the functions in this module whether in single-process or multi-process mode. The subprocesses must not produce any output in multi-process mode and shall send their output as messages to the invariant manager instead.
exception Terminate

Logging


include Log.Sig
Expose functions from logging module
include Log.SLog
Logging instantiated with an actual relay function
val set_relay_log : unit -> unit
Relay log messages to invariant manager (overrides function from Log)
val log_step_cex : Lib.kind_module ->
Lib.log_level ->
'a InputSystem.t ->
Analysis.param ->
TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
Logs a step counterexample.

Should only be used by step for sending the cex, and invariant manager to actually print it.

val log_disproved : Lib.kind_module ->
Lib.log_level ->
'a InputSystem.t ->
Analysis.param ->
TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
Log a disproved property

Should only be used by the invariant manager, other modules must use Event.prop_status to send it as a message.

val log_proved : Lib.kind_module ->
Lib.log_level -> TransSys.t -> int option -> string -> unit
Log a proved property

Should only be used by the invariant manager, other modules must use Event.prop_status to send it as a message.

val log_prop_status : Lib.log_level -> TransSys.t -> (string * Property.prop_status) list -> unit
Log summary of status of properties

Should only be used by the invariant manager, other modules must use Event.prop_status to send it as a message.

val log_stat : Lib.kind_module ->
Lib.log_level -> (string * Stat.stat_item list) list -> unit
Log statistics

Should only be used by the invariant manager, other modules must use Event.stat to send it as a message.

val terminate_log : unit -> unit
Terminate log, called at the very end of a run. Output closing tags for XML output.
val log_run_end : Analysis.result list -> unit
Logs the end of a run. log_run_start results logs the end of a run.
val log_analysis_start : TransSys.t -> Analysis.param -> unit
Logs the start of an analysis. log_analysis_start top abs logs the start of an analysis for top system top with abstraction abs.
val log_analysis_end : Analysis.result -> unit
Logs the end of an analysis. log_analysis_start result logs the end of an analysis.
val log_post_analysis_start : string -> string -> unit
Logs the start of a post-analysis treatment. Arguments: * name of the treatment (concise, for XML) * title of the treatment (verbose, for pt)
val log_post_analysis_end : unit -> unit
Logs the end of a post-analysis treatment.
val log_timeout : bool -> unit
Logs a timeout. Input should be true for wallclock, false for CPU.
val log_interruption : int -> unit
Logs an interruption for some signal.

Events



Events exposed to callers
type event = 
| Invariant of string list * Term.t * Certificate.t * bool
| PropStatus of string * Property.prop_status
| StepCex of string * (StateVar.t * Model.value list) list
val pp_print_event : Format.formatter -> event -> unit
Pretty-print an event
val all_stats : unit -> (Lib.kind_module * (string * Stat.stat_item list) list) list
Return the last statistics received
val stat : (string * Stat.stat_item list) list -> unit
Output the statistics of the module
val progress : int -> unit
Output the progress of the module
val invariant : string list -> Term.t -> Certificate.t -> bool -> unit
Broadcast a discovered top level invariant
val step_cex : 'a InputSystem.t ->
Analysis.param ->
TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
Broadcast a step cex
val prop_status : Property.prop_status ->
'a InputSystem.t -> Analysis.param -> TransSys.t -> string -> unit
Broadcast a property status
val execution_path : 'a InputSystem.t ->
Analysis.param -> TransSys.t -> (StateVar.t * Model.value list) list -> unit
Broadcast an execution path
val terminate : unit -> unit
Broadcast a termination message
val recv : unit -> (Lib.kind_module * event) list
Receive all queued events
val update_child_processes_list : (int * Lib.kind_module) list -> unit
Notifies the background thread of a new list of child processes. Used by the supervisor in a modular analysis when restarting.
val check_termination : unit -> unit
Terminates if a termination message was received. Does NOT modify received messages.
val update_trans_sys_sub : 'a InputSystem.t ->
Analysis.param ->
TransSys.t ->
(Lib.kind_module * event) list ->
(Term.TermSet.t * Term.TermSet.t) Scope.Map.t *
(Lib.kind_module * (string * Property.prop_status)) list
Update transition system from events and return new invariants INCLUDING subsystem ones, scoped and properties with changed status.

For a property status message the status saved in the transition system is updated if the status is more general (k-true for a greater k, k-false for a smaller k, etc.).

Received invariants are stored in the transition system, also proved properties are added as invariants.

Counterexamples are ignored.

val update_trans_sys : 'a InputSystem.t ->
Analysis.param ->
TransSys.t ->
(Lib.kind_module * event) list ->
(Term.TermSet.t * Term.TermSet.t) *
(Lib.kind_module * (string * Property.prop_status)) list
Update transition system from events and return new top level invariants and properties with changed status.

For a property status message the status saved in the transition system is updated if the status is more general (k-true for a greater k, k-false for a smaller k, etc.).

Received invariants are stored in the transition system, also proved properties are added as invariants.

Counterexamples are ignored.


Messaging


type messaging_setup 
Setup of the messaging system
type mthread 
Background thread of the messaging system
val setup : unit -> messaging_setup
Create contexts and bind ports for all processes
val run_im : messaging_setup ->
(int * Lib.kind_module) list -> (exn -> unit) -> unit
Start messaging for the invariant manager
val run_process : Lib.kind_module -> messaging_setup -> (exn -> unit) -> mthread
Start messaging for another process
val exit : mthread -> unit
Send all queued messages and exit the background thread
val pp_print_path_pt : 'a InputSystem.t ->
Analysis.param ->
TransSys.t ->
'a -> Format.formatter -> (StateVar.t * Model.value list) list -> unit