lustrec / src / backends / Horn / horn_backend_collecting_sem.ml @ 0d54d8a8
History | View | Annotate | Download (7.66 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 | 8446bf03 | ploc | open Lustre_types |
20 | 0dee2bc1 | ploc | open Corelang |
21 | 089f94be | ploc | open Machine_code_types |
22 | 0dee2bc1 | ploc | |
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 | fprintf fmt "(declare-rel MAIN (%a))@." |
||
45 | (Utils.fprintf_list ~sep:" " pp_type) |
||
46 | (List.map (fun v -> v.var_type) main_memory_next); |
||
47 | |||
48 | 07ceae4c | ploc | |
49 | (* Init case *) |
||
50 | let _ = |
||
51 | (* Special case when the main node is stateless *) |
||
52 | if is_stateless machine then ( |
||
53 | let step_name = pp_machine_stateless_name in |
||
54 | fprintf fmt "; Initial set: One Step(m,x) -- Stateless node! @."; |
||
55 | fprintf fmt "(declare-rel INIT_STATE ())@."; |
||
56 | fprintf fmt "(rule INIT_STATE)@."; |
||
57 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
58 | fprintf fmt "INIT_STATE@ "; |
||
59 | fprintf fmt "(@[<v 0>%a %a@])" |
||
60 | step_name node |
||
61 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
62 | fprintf fmt "@]@ )@ "; |
||
63 | fprintf fmt "(MAIN %a)@]@.))@.@." |
||
64 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
||
65 | ) |
||
66 | else ( |
||
67 | let reset_name, step_name = |
||
68 | pp_machine_reset_name, pp_machine_step_name |
||
69 | in |
||
70 | fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
||
71 | fprintf fmt "(declare-rel INIT_STATE ())@."; |
||
72 | fprintf fmt "(rule INIT_STATE)@."; |
||
73 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
74 | fprintf fmt "INIT_STATE@ "; |
||
75 | fprintf fmt "(@[<v 0>%a %a@])@ " |
||
76 | reset_name node |
||
77 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
||
78 | fprintf fmt "(@[<v 0>%a %a@])" |
||
79 | step_name node |
||
80 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
81 | |||
82 | fprintf fmt "@]@ )@ "; |
||
83 | fprintf fmt "(MAIN %a)@]@.))@.@." |
||
84 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
||
85 | ) |
||
86 | in |
||
87 | 0dee2bc1 | ploc | |
88 | 07ceae4c | ploc | let step_name = |
89 | if is_stateless machine then |
||
90 | pp_machine_stateless_name |
||
91 | else |
||
92 | pp_machine_step_name |
||
93 | in |
||
94 | |||
95 | 0dee2bc1 | ploc | fprintf fmt "; Inductive def@."; |
96 | (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
||
97 | fprintf fmt |
||
98 | "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
||
99 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current |
||
100 | step_name node |
||
101 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
||
102 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next |
||
103 | |||
104 | |||
105 | let check_prop machines fmt node machine = |
||
106 | let main_output = |
||
107 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
108 | in |
||
109 | let main_memory_next = |
||
110 | (rename_next_list (full_memory_vars machines machine)) @ main_output |
||
111 | in |
||
112 | fprintf fmt "; Property def@."; |
||
113 | fprintf fmt "(declare-rel ERR ())@."; |
||
114 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
||
115 | (pp_conj (pp_horn_var machine)) main_output |
||
116 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next |
||
117 | ; |
||
118 | d2d9d4cb | ploc | if !Options.horn_query then fprintf fmt "(query ERR)@." |
119 | 0dee2bc1 | ploc | |
120 | |||
121 | let cex_computation machines fmt node machine = |
||
122 | fprintf fmt "; CounterExample computation for node %s@.@." node; |
||
123 | (* We print the types of the cex node "memory tree" TODO: add the output *) |
||
124 | let cex_input = |
||
125 | rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
||
126 | in |
||
127 | let cex_input_dummy = |
||
128 | rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
||
129 | in |
||
130 | let cex_output = |
||
131 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
132 | in |
||
133 | let cex_output_dummy = |
||
134 | rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
||
135 | in |
||
136 | let cex_memory_next = |
||
137 | cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
||
138 | in |
||
139 | let cex_memory_current = |
||
140 | cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
||
141 | in |
||
142 | |||
143 | (* Special case when the cex node is stateless *) |
||
144 | let reset_name, step_name = |
||
145 | if is_stateless machine then |
||
146 | pp_machine_stateless_name, pp_machine_stateless_name |
||
147 | else |
||
148 | pp_machine_reset_name, pp_machine_step_name |
||
149 | in |
||
150 | |||
151 | fprintf fmt "(declare-rel CEX (Int %a))@.@." |
||
152 | (Utils.fprintf_list ~sep:" " pp_type) |
||
153 | (List.map (fun v -> v.var_type) cex_memory_next); |
||
154 | |||
155 | fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
||
156 | fprintf fmt "(declare-rel INIT_STATE_CEX ())@."; |
||
157 | fprintf fmt "(rule INIT_STATE_CEX)@."; |
||
158 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
||
159 | fprintf fmt "INIT_STATE_CEX@ "; |
||
160 | fprintf fmt "(@[<v 0>%a %a@])@ " |
||
161 | reset_name node |
||
162 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
||
163 | fprintf fmt "(@[<v 0>%a %a@])" |
||
164 | step_name node |
||
165 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
||
166 | |||
167 | fprintf fmt "@]@ )@ "; |
||
168 | fprintf fmt "(CEX 0 %a)@]@.))@.@." |
||
169 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ; |
||
170 | |||
171 | fprintf fmt "; Inductive def@."; |
||
172 | (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
||
173 | (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
||
174 | fprintf fmt "(declare-var cexcpt Int)@."; |
||
175 | fprintf fmt |
||
176 | "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
||
177 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current |
||
178 | step_name node |
||
179 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) |
||
180 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
||
181 | |||
182 | let get_cex machines fmt node machine = |
||
183 | let cex_input = |
||
184 | rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
||
185 | in |
||
186 | let cex_output = |
||
187 | rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
||
188 | in |
||
189 | let cex_memory_next = |
||
190 | cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
||
191 | in |
||
192 | fprintf fmt "; Property def@."; |
||
193 | fprintf fmt "(declare-rel CEXTRACE ())@."; |
||
194 | fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
||
195 | (pp_conj (pp_horn_var machine)) cex_output |
||
196 | (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next |
||
197 | ; |
||
198 | fprintf fmt "(query CEXTRACE)@." |
||
199 | |||
200 | (* Local Variables: *) |
||
201 | (* compile-command:"make -C ../.." *) |
||
202 | (* End: *) |