module Event:sig
..end
exception Terminate
include Log.Sig
include Log.SLog
val set_relay_log : unit -> unit
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
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
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
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
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
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
val log_run_end : Analysis.result list -> unit
log_run_start results
logs the end of a run.val log_analysis_start : TransSys.t -> Analysis.param -> unit
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
log_analysis_start result
logs the end of an analysis.val log_post_analysis_start : string -> string -> unit
val log_post_analysis_end : unit -> unit
val log_timeout : bool -> unit
true
for wallclock, false
for CPU.val log_interruption : int -> unit
type
event =
| |
Invariant of |
| |
PropStatus of |
| |
StepCex of |
val pp_print_event : Format.formatter -> event -> unit
val all_stats : unit -> (Lib.kind_module * (string * Stat.stat_item list) list) list
val stat : (string * Stat.stat_item list) list -> unit
val progress : int -> unit
val invariant : string list -> Term.t -> Certificate.t -> bool -> unit
val step_cex : 'a InputSystem.t ->
Analysis.param ->
TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit
val prop_status : Property.prop_status ->
'a InputSystem.t -> Analysis.param -> TransSys.t -> string -> unit
val execution_path : 'a InputSystem.t ->
Analysis.param -> TransSys.t -> (StateVar.t * Model.value list) list -> unit
val terminate : unit -> unit
val recv : unit -> (Lib.kind_module * event) list
val update_child_processes_list : (int * Lib.kind_module) list -> unit
val check_termination : unit -> unit
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
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
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.
type
messaging_setup
type
mthread
val setup : unit -> messaging_setup
val run_im : messaging_setup ->
(int * Lib.kind_module) list -> (exn -> unit) -> unit
val run_process : Lib.kind_module -> messaging_setup -> (exn -> unit) -> mthread
val exit : mthread -> unit
val pp_print_path_pt : 'a InputSystem.t ->
Analysis.param ->
TransSys.t ->
'a -> Format.formatter -> (StateVar.t * Model.value list) list -> unit