Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_collecting_sem.ml @ ca88e660

History | View | Annotate | Download (6.93 KB)

1 0dee2bc1 ploc
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14
15
   This is a modified version that handle reset
16
*)
17
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22
23
open Horn_backend_common
24
open Horn_backend_printers
25
26
let collecting_semantics machines fmt node machine =
27
  fprintf fmt "; Collecting semantics for node %s@.@." node;
28
  (* We print the types of the main node "memory tree" TODO: add the output *)
29
  let main_output =
30
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
31
  in
32
  let main_output_dummy =
33
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
34
  in
35
  let main_memory_next =
36
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
37
      main_output
38
  in
39
  let main_memory_current =
40
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
41
      main_output_dummy
42
  in
43
44
  (* Special case when the main node is stateless *)
45
  let reset_name, step_name =
46
    if is_stateless machine then
47
      pp_machine_stateless_name, pp_machine_stateless_name
48
    else
49
      pp_machine_reset_name, pp_machine_step_name
50
  in
51
52
  fprintf fmt "(declare-rel MAIN (%a))@."
53
    (Utils.fprintf_list ~sep:" " pp_type)
54
    (List.map (fun v -> v.var_type) main_memory_next);
55
56
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
57
  fprintf fmt "(declare-rel INIT_STATE ())@.";
58
  fprintf fmt "(rule INIT_STATE)@.";
59
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
60
  fprintf fmt "INIT_STATE@ ";
61
  fprintf fmt "(@[<v 0>%a %a@])@ "
62
    reset_name node
63
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
64
  fprintf fmt "(@[<v 0>%a %a@])"
65
    step_name node
66
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
67
    
68
  fprintf fmt "@]@ )@ ";
69
  fprintf fmt "(MAIN %a)@]@.))@.@."
70
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
71
72
  fprintf fmt "; Inductive def@.";
73
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
74
  fprintf fmt
75
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
76
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current
77
    step_name node
78
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
79
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
80
81
82
let check_prop machines fmt node machine =
83
  let main_output =
84
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
85
  in
86
  let main_memory_next =
87
    (rename_next_list (full_memory_vars machines machine)) @ main_output
88
  in
89
  fprintf fmt "; Property def@.";
90
  fprintf fmt "(declare-rel ERR ())@.";
91
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
92
    (pp_conj (pp_horn_var machine)) main_output
93
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
94
    ;
95 ca88e660 Ploc
   if !Options.horn_queries then fprintf fmt "(query ERR)@."
96 0dee2bc1 ploc
97
98
let cex_computation machines fmt node machine =
99
  fprintf fmt "; CounterExample computation for node %s@.@." node;
100
    (* We print the types of the cex node "memory tree" TODO: add the output *)
101
  let cex_input =
102
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
103
  in
104
  let cex_input_dummy =
105
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
106
  in
107
  let cex_output =
108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
109
  in
110
  let cex_output_dummy =
111
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
112
  in
113
  let cex_memory_next =
114
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
115
  in
116
  let cex_memory_current =
117
    cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
118
  in
119
120
    (* Special case when the cex node is stateless *)
121
  let reset_name, step_name =
122
    if is_stateless machine then
123
      pp_machine_stateless_name, pp_machine_stateless_name
124
    else
125
      pp_machine_reset_name, pp_machine_step_name
126
  in
127
128
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
129
    (Utils.fprintf_list ~sep:" " pp_type)
130
    (List.map (fun v -> v.var_type) cex_memory_next);
131
132
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
133
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
134
  fprintf fmt "(rule INIT_STATE_CEX)@.";
135
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
136
  fprintf fmt "INIT_STATE_CEX@ ";
137
  fprintf fmt "(@[<v 0>%a %a@])@ "
138
    reset_name node
139
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
140
  fprintf fmt "(@[<v 0>%a %a@])"
141
    step_name node
142
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
143
  
144
  fprintf fmt "@]@ )@ ";
145
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
146
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ;
147
148
  fprintf fmt "; Inductive def@.";
149
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
150
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
151
  fprintf fmt "(declare-var cexcpt Int)@.";
152
  fprintf fmt
153
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
154
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current
155
    step_name node
156
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
157
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
158
159
let get_cex machines fmt node machine =
160
    let cex_input =
161
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
162
    in
163
    let cex_output =
164
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
165
    in
166
  let cex_memory_next =
167
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
168
  in
169
  fprintf fmt "; Property def@.";
170
  fprintf fmt "(declare-rel CEXTRACE ())@.";
171
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
172
    (pp_conj (pp_horn_var machine)) cex_output
173
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
174
    ;
175
  fprintf fmt "(query CEXTRACE)@."
176
177
(* Local Variables: *)
178
(* compile-command:"make -C ../.." *)
179
(* End: *)