CristalCaveGem » LustreC

let reachtube = ref false (* used to produce a list of set iterates *)

  (* let mems = m.mmemory in *)

    let open Tiny.Load_domains in

    prepare_domains (List.map get_domain !domains)

  in

  let results = Tiny.Analyze.analyze

                  dom

                  (not !reachtube) (* when this argument is false, a

                                      simulation is performed*)

                  !descending

                  !unrolling

                  env

                  ast

  in

  (* if !Tiny.Report.verbosity > 1 then *)

  if !reachtube then (

    (* Print preamble *)

    report ~level:1 (Tiny_tube.export_to_csv env ast results);

    (* We produce in a folder: the csv file, the tiny file *)

    let destname = !Options.dest_dir ^ "/" ^ basename ^ "_" ^ node_name ^ ".csv" in

    report ~level:1 (fun fmt -> Format.fprintf fmt "Exporting resulting tube as %s@ " destname);

    let out = open_out destname in

    let fmt = Format.formatter_of_out_channel out in

    Format.fprintf fmt "%t@." (Tiny_tube.export_to_csv env ast results); 

    close_out out;

  )

  else

    let module Results = (val results: Tiny.Analyze.Results) in

    let module Dom = Results.Dom in

    let module PrintResults = Tiny.PrintResults.Make (Dom) in

    let m = Results.results in

    report ~level:1 (PrintResults.print m env ast)

    (* no !output_file *);

    (* else PrintResults.print_invariants m ast !output_file *)

    ()

    (* Enforce global inline from top node *)

    let get_normalization_params () =

      Options.global_inline := true;

      get_normalization_params ()

      ("-reachtube", Arg.Int (fun n -> unrolling :=n; reachtube:=true),

       "<n>  Unroll main loop <n> times to compute finite horizon analysis (default is invariant, with 0)");