CristalCaveGem » LustreC

   This is a modified version that handle reset *)

open Format

open Lustre_types

open Machine_code_types

  in

  fprintf fmt "(declare-rel MAIN (%a))@."

    (List.map (fun v -> v.var_type) main_memory_next);

  (* Init case *)

      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";

      fprintf fmt "INIT_STATE@ ";

      fprintf fmt "(@[<v 0>%a %a@])" step_name node

        (step_vars_m_x machines machine);

      fprintf fmt "@]@ )@ ";

      fprintf fmt "(MAIN %a)@]@.))@.@."

        main_memory_next)

    else

      let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in

      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";

      fprintf fmt "INIT_STATE@ ";

      fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node

        (reset_vars machines machine);

      fprintf fmt "(@[<v 0>%a %a@])" step_name node

        (step_vars_m_x machines machine);

      fprintf fmt "@]@ )@ ";

      fprintf fmt "(MAIN %a)@]@.))@.@."

        main_memory_next

  in

  in

  fprintf fmt "; Inductive def@.";

    fmt main_output_dummy;

  fprintf fmt

    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN \

     %a)@]@.))@.@."

    main_memory_current step_name node

    (step_vars machines machine)

    main_memory_next

let check_prop machines fmt machine =

  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."

    (pp_conj (pp_horn_var machine))

    main_output

    main_memory_next;

  if !Options.horn_query then fprintf fmt "(query ERR)@."

  in

  fprintf fmt "(declare-rel CEX (Int %a))@.@."

    (List.map (fun v -> v.var_type) cex_memory_next);

  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";

  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";

  fprintf fmt "INIT_STATE_CEX@ ";

  fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node

    (reset_vars machines machine);

  fprintf fmt "(@[<v 0>%a %a@])" step_name node

    (step_vars_m_x machines machine);

  fprintf fmt "@]@ )@ ";

  fprintf fmt "(CEX 0 %a)@]@.))@.@."

    cex_memory_next;

  fprintf fmt "; Inductive def@.";

  (* Declare dummy inputs. Outputs should have been declared previously with

     collecting sem *)

    fmt cex_input_dummy;

  fprintf fmt "(declare-var cexcpt Int)@.";

  fprintf fmt

    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ \

     (CEX (+ 1 cexcpt) %a)@]@.))@.@."

    cex_memory_current step_name node

    (step_vars machines machine)

    cex_memory_next

let get_cex machines fmt machine =

    "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."

    (pp_conj (pp_horn_var machine))

    cex_output

    cex_memory_next;

  fprintf fmt "(query CEXTRACE)@."