Module LustrePath

module LustrePath: sig .. end
Conversion of a counterexample to a Lustre model
Author(s): Kevin Clancy, Christoph Sticksel

val pp_print_path_xml : TransSys.t ->
TransSys.instance list ->
LustreNode.t SubSystem.t -> bool -> Format.formatter -> Model.path -> unit
Output a counterexample as a Lustre execution in XML format
val pp_print_path_pt : TransSys.t ->
TransSys.instance list ->
LustreNode.t SubSystem.t -> bool -> Format.formatter -> Model.path -> unit
Output a counterexample as a Lustre execution as plain text with pre-processing reverted
val pp_print_path_json : TransSys.t ->
TransSys.instance list ->
LustreNode.t SubSystem.t -> bool -> Format.formatter -> Model.path -> unit
Output a counterexample as a Lustre execution in JSON format
val pp_print_path_in_csv : TransSys.t ->
TransSys.instance list ->
LustreNode.t SubSystem.t -> bool -> Format.formatter -> Model.path -> unit
Outputs a model as a sequence of inputs in CSV.
val substitute_definitions_in_expr : LustreNode.equation list -> LustreExpr.t -> LustreExpr.t
Recursively substitute the state variables in a term with their definition in equations.
val reconstruct_lustre_streams : LustreNode.t SubSystem.t ->
StateVar.t list ->
(StateVar.t * (LustreIdent.t * int * LustreNode.call_cond list) list) list
StateVar.StateVarMap.t
Reconstruct Lustre streams from state variables