InputSystem (kind2dev@731decdf5fb1.InputSystem)

type _ t

module IntSet : Stdlib.Set.S with type elt = int

exception UnsupportedFileFormat of string

val read_input_lustre : bool -> string -> LustreNode.t t option

read_input_lustre only_parse filename read input from filename and returns None if only_parse is true, or an input system otherwise.

See LustreInput.of_file for potential exceptions thrown by this function.

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 read_input_moxi : string -> TransSys.t t option

Read MoXI input from file

val ordered_scopes_of : 'a t -> Scope.t list

Returns the scopes of all the systems in an input systems, in topological order.

val analyzable_subsystems : 'a t -> 'a SubSystem.t list

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 with modes.

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 monitor_param : 'a t -> Analysis.param

val mcs_params : 'a t -> Analysis.param list

val contract_check_params : 'a t -> (Analysis.param * bool) list

Return analysis parameters for all systems without an implementation

If the system has a contract, the boolean argument is true

val moxi_params : 'a t -> Analysis.param list

val trans_sys_of_analysis : 
  ?preserve_sig:bool ->
  ?slice_nodes:Flags.slice_nodes ->
  ?add_functional_constraints:bool ->
  ?slice_to_prop:Property.t ->
  'a t ->
  Analysis.param ->
  TransSys.t * 'a t

Return a transition system for an analysis run

val pp_print_path_pt : 
  ?full_contract:bool ->
  ?prop_name:string ->
  _ t ->
  TransSys.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Output a path in the input system

val pp_print_path_xml : 
  ?prop_name:string ->
  _ t ->
  TransSys.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Output a path in the input system. prop_name names the property a counterexample belongs to, if any; see LustrePath.pp_print_path_xml.

val pp_print_path_json : 
  ?prop_name:string ->
  _ t ->
  TransSys.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Output a path in the input system

val pp_print_path_json_testgen : 
  _ t ->
  TransSys.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Output a path in the input system. The format for this path is the same format that the Interpreter module expects as input.

val pp_print_path_in_csv : 
  _ t ->
  TransSys.t ->
  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 * LustreNode.state_var_def list

val lustre_source_ast : 'a t -> LustreAst.t

val pp_print_term_as_expr : 
  _ t ->
  TransSys.t ->
  Stdlib.Format.formatter ->
  Term.t ->
  unit

val slice_to_abstraction : 'a t -> Analysis.param -> TransSys.t -> 'a 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 retrieve_lustre_nodes_of_scope : _ t -> Scope.t -> LustreNode.t list

val contain_partially_defined_system : _ t -> Scope.t -> bool

val contain_call_applied_to_quant_vars : _ t -> Scope.t -> bool

true if the model has a call applied to quantified variables, which is compiled to an application of the functional symbol of the callee rather than to an instance of it (see GeneratedIdentifiers.t.qcalls). The analyses that build their system without functional constraints have nothing to interpret such a call with, and decline a model that has one.

val get_lustre_node : _ t -> Scope.t -> LustreNode.t option

Return the lustre node associated to the given scope, or None if there is no lustre node associated to 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 call_state_var_to_lustre_reference : 
  _ t ->
  StateVar.t list ->
  string StateVar.StateVarMap.t

Returns a map from call state variables to lustre-like names

val is_lustre_input : _ t -> bool

val is_moxi_input : _ t -> bool

val contract_gen_param : 
  _ t ->
  Scope.t ->
  Analysis.param * (Scope.t -> LustreNode.t)

Parameter for contract generation.

val state_var_dependencies : 
  _ t ->
  StateVar.StateVarSet.t StateVar.StateVarMap.t Scope.Map.t

Return the set of dependencies of each state variable for all systems

val get_bv_sizes : _ t -> IntSet.t

val get_ubv_sizes : _ t -> IntSet.t

val get_node_internal_name : _ t -> Scope.t -> LustreIdent.t

val get_node_user_name : _ t -> Scope.t -> LustreIdent.t

val get_node_id : _ t -> Scope.t -> NodeId.t

val current_state_props : _ t -> Scope.t -> string list

val prefix_system : 'a t -> string -> 'a t