Module InputSystem

module InputSystem: sig .. end
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(s): 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 trans_sys_of_analysis : ?preserve_sig:bool ->
'a t -> Analysis.param -> TransSys.t * 'a t
Return a transition system for an analysis run
val pp_print_path_pt : 'a t ->
TransSys.t ->
TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
Output a path in the input system
val pp_print_path_xml : 'a t ->
TransSys.t ->
TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
Output a path in the input system
val pp_print_path_json : 'a t ->
TransSys.t ->
TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
Output a path in the input system
val pp_print_path_in_csv : 'a t ->
TransSys.t ->
TransSys.instance list -> bool -> Format.formatter -> Model.path -> unit
Output a model as a sequnce of inputs in CSV.
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 reconstruct_lustre_streams : 'a t ->
StateVar.t list ->
(StateVar.t * (LustreIdent.t * int * LustreNode.call_cond list) list) list
StateVar.StateVarMap.t
val is_lustre_input : 'a t -> bool
val compile_to_rust : 'a t -> Scope.t -> string -> unit
Compiles a system (scope) to Rust to the folder specified as a crate.
val compile_oracle_to_rust : 'a 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 : 'a t -> Analysis.param * (Scope.t -> LustreNode.t)
Parameter for contract generation.
val unsliced_trans_sys_of : ?preserve_sig:bool ->
'a t -> Analysis.param -> TransSys.t * 'a t
Transition system for contract generation or interpreter, without any slicing.