Module `InputSystem`

Delegate to concrete functions for input formats.

All functionality outside this module should be agnostic of the input format, with the exception of modules specialized to a particular input. Only here we distinguish the actual input format and delegate to the respective functions.

author: Christoph Sticksel

type _ t

exception UnsupportedFileFormat of string

val read_input_lustre : string -> LustreNode.t t: Read input from file

val translate_contracts_lustre : string -> string -> unit: Translate lustre contracts to properties.

val read_input_native : string -> TransSys.t t: Read native input from file

val silent_contracts_of : 'a t -> (Scope.t * string list) list: Returns the silent contract associated to each system.

val ordered_scopes_of : 'a t -> Scope.t list: Returns the scopes of all the systems in an input systems, in topological order.

val maximal_abstraction_for_testgen : 'a t -> Scope.t -> Analysis.assumptions -> Analysis.param option: Returns the analysis param for top that abstracts all its abstractable subsystems if top has a contract.

val next_analysis_of_strategy : 'a t -> Analysis.results -> Analysis.param option: Return the next system to analyze and the systems to abstract

val interpreter_param : 'a t -> Analysis.param
val mcs_params : 'a t -> Analysis.param list
val trans_sys_of_analysis : ?⁠preserve_sig:bool -> ?⁠slice_nodes:bool -> 'a t -> Analysis.param -> TransSys.t * 'a t: Return a transition system for an analysis run

val pp_print_path_pt : _ t -> TransSys.t -> TransSys.instance list -> bool -> Stdlib.Format.formatter -> Model.path -> unit: Output a path in the input system

val pp_print_path_xml : _ t -> TransSys.t -> TransSys.instance list -> bool -> Stdlib.Format.formatter -> Model.path -> unit: Output a path in the input system

val pp_print_path_json : _ t -> TransSys.t -> TransSys.instance list -> bool -> Stdlib.Format.formatter -> Model.path -> unit: Output a path in the input system

val pp_print_path_in_csv : _ t -> TransSys.t -> TransSys.instance list -> bool -> Stdlib.Format.formatter -> Model.path -> unit: Output a model as a sequnce of inputs in CSV.

val pp_print_subsystems_debug : Stdlib.Format.formatter -> 'a t -> unit: Output all subsystems of the input system *

val pp_print_state_var_instances_debug : Stdlib.Format.formatter -> 'a t -> unit

val pp_print_state_var_defs_debug : Stdlib.Format.formatter -> 'a t -> unit

val lustre_definitions_of_state_var : 'a t -> StateVar.t -> LustreNode.state_var_def list

val lustre_source_ast : 'a t -> LustreAst.t

val slice_to_abstraction_and_property : 'a t -> Analysis.param -> TransSys.t -> (StateVar.t * Model.value list) list -> Property.t -> TransSys.t * TransSys.instance list * (StateVar.t * Model.value list) list * Term.t * 'a t

val retrieve_lustre_nodes : _ t -> LustreNode.t list

val find_lustre_node : Scope.t -> _ t -> LustreNode.t

Return the lustre node of the given scope

Raise Not_found if there is no subsystem of that scope

val reconstruct_lustre_streams : _ t -> StateVar.t list -> (StateVar.t * (LustreIdent.t * int * LustreNode.call_cond list) list) list StateVar.StateVarMap.t
val mk_state_var_to_lustre_name_map : _ t -> StateVar.t list -> string StateVar.StateVarMap.t: Returns a map from state variables to lustre-like names

val is_lustre_input : _ t -> bool
val compile_to_rust : _ t -> Scope.t -> string -> unit: Compiles a system (scope) to Rust to the folder specified as a crate.

val compile_oracle_to_rust : _ t -> Scope.t -> string -> string * (Lib.position * int) list * (string * Lib.position * int) list: Compiles a system (scope) to Rust as an oracle to the folder specified as a crate.

val contract_gen_param : _ t -> Analysis.param * (Scope.t -> LustreNode.t): Parameter for contract generation.