Module LustrePath

Conversion of a counterexample to a Lustre model

author
Kevin Clancy, Christoph Sticksel
val pp_print_path_xml : TransSys.t -> TransSys.instance list -> LustreNode.t SubSystem.t -> bool -> Stdlib.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 -> Stdlib.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 -> Stdlib.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 -> Stdlib.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