KEvent (kind2dev@731decdf5fb1.KEvent)

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.

author Christoph Sticksel

exception Terminate

Logging

Expose functions from logging module

include Log.Sig

type 'a log_printer =
  Lib.log_level ->
  ('a, Stdlib.Format.formatter, unit) Stdlib.format ->
  'a

type 'a m_log_printer = Lib.kind_module -> 'a log_printer

Logging

val set_module : Lib.kind_module -> unit

Set module currently running

val get_module : unit -> Lib.kind_module

Get module currently running

type log_format =

| F_pt
(*
Plain text
*)
| F_xml
(*
XML
*)
| F_json
(*
JSON
*)
| F_ijson
(*
Incremental JSON object stream
*)
| F_relay
(*
Relayed
*)

Format of log messages

val get_log_format : unit -> log_format

Returns the log format

val set_log_format : log_format -> unit

Chooses the log format

val set_log_format_pt : unit -> unit

Set log format to plain text

val set_log_format_xml : unit -> unit

Set log format to XML

val set_log_format_json : unit -> unit

Set log format to JSON

val set_log_format_ijson : unit -> unit

Set log format to incremental JSON

val print_json_sep : Stdlib.Format.formatter -> unit

Print the separator between JSON objects (could be nothing for incremental json, or comma for standard json)

val get_show_props : unit -> bool

Returns whether to show properties' constraints

val set_show_props : bool -> unit

Set whether to show properties' constraints

val unset_relay_log : unit -> unit

Cancel relaying of log messages

Auxiliary functions

val pp_print_kind_module_xml_src : 
  Stdlib.Format.formatter ->
  Lib.kind_module ->
  unit

val print_xml_trailer : unit -> unit

val printf_xml : 'a m_log_printer

val printf_json : 'a m_log_printer

val parse_log_xml : Lib.log_level -> Lib.position -> string -> unit

val parse_log_json : Lib.log_level -> Lib.position -> string -> unit

Logging instantiated with an actual relay function

include Log.SLog

val log : 'a Log.log_printer

log m l f v ... outputs a message from module m on level l, formatted with the parameterized string f and the values v ...

val log_uncond : ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

log_uncond m f v ... outputs a message from module m unconditionally, formatted with the parameterized string f and the values v ...

val log_result : 
  (Stdlib.Format.formatter -> 'a -> unit) ->
  (Stdlib.Format.formatter -> 'a -> unit) ->
  (Stdlib.Format.formatter -> 'a -> unit) ->
  'a ->
  unit

log_result pt xml json a outputs a result (for instance, for a post analysis) by choosing the right printing function depending on the output format

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 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 prop_status to send it as a message.

val log_with_tag : 
  Lib.log_level ->
  (Stdlib.Format.formatter -> unit) ->
  string ->
  unit

val log_prop_status : 
  Lib.log_level ->
  TransSys.t ->
  (string * Property.prop_status * Property.prop_kind) list ->
  unit

Log summary of status of properties

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

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

Log statistics

Should only be used by the invariant manager, other modules must use 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 : _ InputSystem.t -> Analysis.result list -> unit

Logs the end of a run. log_run_start results logs the end of a run.

val log_analysis_start : 
  'a InputSystem.t ->
  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_contractck_analysis_start : 'a InputSystem.t -> Scope.t -> unit

Logs the start of an analysis. Simplified version of log_analysis_start that is used for contract checking

val log_analysis_end : unit -> unit

Logs the end of an analysis. log_analysis_end 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.

val pp_print_trace_pt : 
  ?title:string ->
  ?color:string ->
  bool ->
  Lib.log_level ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  string option ->
  bool ->
  Stdlib.Format.formatter ->
  (StateVar.t * Model.value list) list ->
  unit

val pp_print_trace_xml : 
  ?tag:string ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  string option ->
  bool ->
  Stdlib.Format.formatter ->
  (StateVar.t * Model.value list) list ->
  unit

val pp_print_trace_json : 
  ?object_name:string ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  string option ->
  bool ->
  Stdlib.Format.formatter ->
  (StateVar.t * Model.value list) list ->
  unit

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 : Stdlib.Format.formatter -> event -> unit

Pretty-print an event

val all_stats : 
  unit ->
  (Lib.kind_module * (string * Stat.snapshot 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 prop_invariant : TransSys.t -> string -> Certificate.t -> Term.TermSet.t

Broadcast a property is invariant, and return a set of logical consequences that are also invariant

val cex_wam : 
  (StateVar.t * Model.value list) list ->
  (string * bool) list ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  string ->
  unit

val proved_wam : Certificate.t -> TransSys.t -> string -> unit

val unknown_wam : TransSys.t -> string -> unit

val execution_path : 
  ?full_contract:bool ->
  'a InputSystem.t ->
  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 wait_for_message : unit -> unit

Block until an event is queued for the calling domain. Returns immediately if there are queued events. Termination requests arrive as messages too, so a waiting engine is woken up on shutdown and raises Terminate in its next call to recv.

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 mworker

Registration of the mailbox of an engine

val setup : unit -> messaging_setup

Create the messaging system in the supervisor

val run_im : messaging_setup -> unit

Take the supervisor role in the calling domain

val purge_im : messaging_setup -> unit

Purge the invariant manager mailbox. Should be called between two analyses, after all engines of the previous analysis have exited, to get rid of messages from the previous analysis.

val register_worker : Lib.kind_module -> int -> messaging_setup -> mworker

Create and register the mailbox of an engine with the given identifier. Must be called in the supervisor, before the engine domain is spawned, so that no message sent from then on is missed.

val run_process : mworker -> mworker

Start messaging for a process. Must be called in the domain of the engine with the registration returned by register_worker.

val unregister_worker : mworker -> unit

Unregister the mailbox of an engine that never ran because its domain could not be spawned

val terminate_worker : int -> unit

Send a termination message to the engine with the given identifier

val exit : mworker -> unit

Unregister the mailbox of an engine

val pp_print_user_node_name : 
  'a InputSystem.t ->
  Stdlib.Format.formatter ->
  Scope.t ->
  unit

val pp_print_path_pt : 
  ?full_contract:bool ->
  'a InputSystem.t ->
  TransSys.t ->
  Stdlib.Format.formatter ->
  (StateVar.t * Model.value list) list ->
  unit