LustrePath (kind2dev@731decdf5fb1.LustrePath)

val pp_print_path_xml : 
  ?prop_name:string ->
  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.

prop_name names the property the counterexample belongs to, if any. A node instance whose outputs are dead is only shown for a property that comes from it (see LustreSlicing.keep_inline_call).

val pp_print_path_pt : 
  ?full_contract:bool ->
  ?prop_name:string ->
  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 : 
  ?prop_name:string ->
  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. See pp_print_path_xml for prop_name.

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