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.

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 ->
  _ t ->
  TransSys.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Output a path in the input system

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

Output a path in the input system

val pp_print_path_json : 
  _ 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 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