Project

General

Profile

Download (7.8 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
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
open Format
18
open Lustre_types
19
open Machine_code_types
20
open Horn_backend_common
21
open Horn_backend_printers
22

    
23
let collecting_semantics machines fmt node machine =
24
  fprintf fmt "; Collecting semantics for node %s@.@." node;
25
  (* We print the types of the main node "memory tree" TODO: add the output *)
26
  let main_output =
27
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
28
  in
29
  let main_output_dummy =
30
    rename_machine_list
31
      ("dummy" ^ machine.mname.node_id)
32
      machine.mstep.step_outputs
33
  in
34
  let main_memory_next =
35
    rename_next_list
36
      (* machine.mname.node_id *)
37
      (full_memory_vars machines machine)
38
    @ main_output
39
  in
40
  let main_memory_current =
41
    rename_current_list
42
      (* machine.mname.node_id *)
43
      (full_memory_vars machines machine)
44
    @ main_output_dummy
45
  in
46

    
47
  fprintf fmt "(declare-rel MAIN (%a))@."
48
    (Utils.fprintf_list ~sep:" " pp_type)
49
    (List.map (fun v -> v.var_type) main_memory_next);
50

    
51
  (* Init case *)
52
  let _ =
53
    (* Special case when the main node is stateless *)
54
    if Machine_code_common.is_stateless machine then (
55
      let step_name = pp_machine_stateless_name in
56
      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
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@])" step_name node
62
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
63
        (step_vars_m_x machines machine);
64
      fprintf fmt "@]@ )@ ";
65
      fprintf fmt "(MAIN %a)@]@.))@.@."
66
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
67
        main_memory_next)
68
    else
69
      let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name 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@])@ " reset_name node
76
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
77
        (reset_vars machines machine);
78
      fprintf fmt "(@[<v 0>%a %a@])" step_name node
79
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
80
        (step_vars_m_x machines machine);
81

    
82
      fprintf fmt "@]@ )@ ";
83
      fprintf fmt "(MAIN %a)@]@.))@.@."
84
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
85
        main_memory_next
86
  in
87

    
88
  let step_name =
89
    if Machine_code_common.is_stateless machine then pp_machine_stateless_name
90
    else pp_machine_step_name
91
  in
92

    
93
  fprintf fmt "; Inductive def@.";
94
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
95
    fmt main_output_dummy;
96
  fprintf fmt
97
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN \
98
     %a)@]@.))@.@."
99
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
100
    main_memory_current step_name node
101
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
102
    (step_vars machines machine)
103
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
104
    main_memory_next
105

    
106
let check_prop machines fmt machine =
107
  let main_output =
108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
109
  in
110
  let main_memory_next =
111
    rename_next_list (full_memory_vars machines machine) @ main_output
112
  in
113
  fprintf fmt "; Property def@.";
114
  fprintf fmt "(declare-rel ERR ())@.";
115
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
116
    (pp_conj (pp_horn_var machine))
117
    main_output
118
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
119
    main_memory_next;
120
  if !Options.horn_query then fprintf fmt "(query ERR)@."
121

    
122
let cex_computation machines fmt node machine =
123
  fprintf fmt "; CounterExample computation for node %s@.@." node;
124
  (* We print the types of the cex node "memory tree" TODO: add the output *)
125
  let cex_input =
126
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
127
  in
128
  let cex_input_dummy =
129
    rename_machine_list
130
      ("dummy" ^ machine.mname.node_id)
131
      machine.mstep.step_inputs
132
  in
133
  let cex_output =
134
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
135
  in
136
  let cex_output_dummy =
137
    rename_machine_list
138
      ("dummy" ^ machine.mname.node_id)
139
      machine.mstep.step_outputs
140
  in
141
  let cex_memory_next =
142
    cex_input
143
    @ rename_next_list (full_memory_vars machines machine)
144
    @ cex_output
145
  in
146
  let cex_memory_current =
147
    cex_input_dummy
148
    @ rename_current_list (full_memory_vars machines machine)
149
    @ cex_output_dummy
150
  in
151

    
152
  (* Special case when the cex node is stateless *)
153
  let reset_name, step_name =
154
    if Machine_code_common.is_stateless machine then
155
      pp_machine_stateless_name, pp_machine_stateless_name
156
    else pp_machine_reset_name, pp_machine_step_name
157
  in
158

    
159
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
160
    (Utils.fprintf_list ~sep:" " pp_type)
161
    (List.map (fun v -> v.var_type) cex_memory_next);
162

    
163
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
164
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
165
  fprintf fmt "(rule INIT_STATE_CEX)@.";
166
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
167
  fprintf fmt "INIT_STATE_CEX@ ";
168
  fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
169
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
170
    (reset_vars machines machine);
171
  fprintf fmt "(@[<v 0>%a %a@])" step_name node
172
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
173
    (step_vars_m_x machines machine);
174

    
175
  fprintf fmt "@]@ )@ ";
176
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
177
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
178
    cex_memory_next;
179

    
180
  fprintf fmt "; Inductive def@.";
181
  (* Declare dummy inputs. Outputs should have been declared previously with
182
     collecting sem *)
183
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
184
    fmt cex_input_dummy;
185
  fprintf fmt "(declare-var cexcpt Int)@.";
186
  fprintf fmt
187
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ \
188
     (CEX (+ 1 cexcpt) %a)@]@.))@.@."
189
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
190
    cex_memory_current step_name node
191
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
192
    (step_vars machines machine)
193
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
194
    cex_memory_next
195

    
196
let get_cex machines fmt machine =
197
  let cex_input =
198
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
199
  in
200
  let cex_output =
201
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
202
  in
203
  let cex_memory_next =
204
    cex_input
205
    @ rename_next_list (full_memory_vars machines machine)
206
    @ cex_output
207
  in
208
  fprintf fmt "; Property def@.";
209
  fprintf fmt "(declare-rel CEXTRACE ())@.";
210
  fprintf fmt
211
    "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
212
    (pp_conj (pp_horn_var machine))
213
    cex_output
214
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
215
    cex_memory_next;
216
  fprintf fmt "(query CEXTRACE)@."
217

    
218
(* Local Variables: *)
219
(* compile-command:"make -C ../.." *)
220
(* End: *)
(2-2/5)