LustrePath (kind2dev@731decdf5fb1.LustrePath)

val pp_print_path_xml : 
  TransSys.t ->
  LustreGlobals.t ->
  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 : 
  ?full_contract:bool ->
  TransSys.t ->
  LustreGlobals.t ->
  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 ->
  LustreGlobals.t ->
  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_json_testgen : 
  TransSys.t ->
  LustreGlobals.t ->
  LustreNode.t SubSystem.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

val pp_print_path_in_csv : 
  TransSys.t ->
  LustreGlobals.t ->
  LustreNode.t SubSystem.t ->
  bool ->
  Stdlib.Format.formatter ->
  Model.path ->
  unit

Outputs a model as a sequence of inputs in CSV.

val reconstruct_lustre_streams : 
  LustreNode.t SubSystem.t list ->
  StateVar.t list ->
  (StateVar.t * (LustreIdent.t * int * LustreNode.call_cond list) list) list
    StateVar.StateVarMap.t

Reconstruct Lustre streams from state variables