CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

(* The compilation presented here was first defined in Garoche, Gurfinkel,

   Kahsai, HCSV'14.

open Format

open Horn_backend_printers

let collecting_semantics machines fmt node machine =

  fprintf fmt "; Collecting semantics for node %s@.@." node;

  (* We print the types of the main node "memory tree" TODO: add the output *)

  let main_output =

    rename_machine_list machine.mname.node_id machine.mstep.step_outputs

  in

  let main_output_dummy =

      ("dummy" ^ machine.mname.node_id)

      machine.mstep.step_outputs

  let main_memory_next =

      (* machine.mname.node_id *)

      (full_memory_vars machines machine)

    @ main_output

  let main_memory_current =

      (* machine.mname.node_id *)

      (full_memory_vars machines machine)

    @ main_output_dummy

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

    (Utils.fprintf_list ~sep:" " pp_type)

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

      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";

      fprintf fmt "(declare-rel INIT_STATE ())@.";

      fprintf fmt "(rule INIT_STATE)@.";

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

      fprintf fmt "INIT_STATE@ ";

        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

        (step_vars_m_x machines machine);

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

        main_memory_next)

    else

      let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in

      fprintf fmt "(declare-rel INIT_STATE ())@.";

      fprintf fmt "(rule INIT_STATE)@.";

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

      fprintf fmt "INIT_STATE@ ";

        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

        (reset_vars machines machine);

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

        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

        (step_vars_m_x machines machine);

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

        main_memory_next

    if Machine_code_common.is_stateless machine then pp_machine_stateless_name

    else pp_machine_step_name

    fmt main_output_dummy;

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

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    main_memory_current step_name node

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    (step_vars machines machine)

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    main_memory_next

    rename_machine_list machine.mname.node_id machine.mstep.step_outputs

  in

  let main_memory_next =

  fprintf fmt "; Property def@.";

  fprintf fmt "(declare-rel ERR ())@.";

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

    main_output

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    main_memory_next;

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

let cex_computation machines fmt node machine =

  fprintf fmt "; CounterExample computation for node %s@.@." node;

    rename_machine_list machine.mname.node_id machine.mstep.step_inputs

  in

  let cex_input_dummy =

      ("dummy" ^ machine.mname.node_id)

      machine.mstep.step_inputs

  let cex_output =

    rename_machine_list machine.mname.node_id machine.mstep.step_outputs

  in

  let cex_output_dummy =

      ("dummy" ^ machine.mname.node_id)

      machine.mstep.step_outputs

  let cex_memory_next =

    @ rename_next_list (full_memory_vars machines machine)

    @ cex_output

  let cex_memory_current =

    @ rename_current_list (full_memory_vars machines machine)

    @ cex_output_dummy

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

    (Utils.fprintf_list ~sep:" " pp_type)

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

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

  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";

  fprintf fmt "(rule INIT_STATE_CEX)@.";

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

  fprintf fmt "INIT_STATE_CEX@ ";

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    (reset_vars machines machine);

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

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    (step_vars_m_x machines machine);

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

    cex_memory_next;

  fprintf fmt "; Inductive def@.";

     collecting sem *)

  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))

    fmt cex_input_dummy;

  fprintf fmt

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

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    cex_memory_current step_name node

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    (step_vars machines machine)

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    cex_memory_next

    rename_machine_list machine.mname.node_id machine.mstep.step_inputs

  in

  let cex_output =

    rename_machine_list machine.mname.node_id machine.mstep.step_outputs

  in

    @ rename_next_list (full_memory_vars machines machine)

    @ cex_output

  fprintf fmt "; Property def@.";

  fprintf fmt "(declare-rel CEXTRACE ())@.";

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

    (pp_conj (pp_horn_var machine))

    cex_output

    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))

    cex_memory_next;

(* Local Variables: *)

(* compile-command:"make -C ../.." *)

(* End: *)