Project

General

Profile

Download (7.54 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 Utils
18
open Format
19
open Lustre_types
20
open Machine_code_types
21
open Horn_backend_common
22
open Horn_backend_printers
23

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

    
48
  fprintf fmt "(declare-rel MAIN (%a))@."
49
    (pp_print_list pp_type)
50
    (List.map (fun v -> v.var_type) main_memory_next);
51

    
52
  (* Init case *)
53
  let _ =
54
    (* Special case when the main node is stateless *)
55
    if Machine_code_common.is_stateless machine then (
56
      let step_name = pp_machine_stateless_name in
57
      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
58
      fprintf fmt "(declare-rel INIT_STATE ())@.";
59
      fprintf fmt "(rule INIT_STATE)@.";
60
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
61
      fprintf fmt "INIT_STATE@ ";
62
      fprintf fmt "(@[<v 0>%a %a@])" step_name node
63
        (pp_print_list (pp_horn_var machine))
64
        (step_vars_m_x machines machine);
65
      fprintf fmt "@]@ )@ ";
66
      fprintf fmt "(MAIN %a)@]@.))@.@."
67
        (pp_print_list (pp_horn_var machine))
68
        main_memory_next)
69
    else
70
      let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in
71
      fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
72
      fprintf fmt "(declare-rel INIT_STATE ())@.";
73
      fprintf fmt "(rule INIT_STATE)@.";
74
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
75
      fprintf fmt "INIT_STATE@ ";
76
      fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
77
        (pp_print_list (pp_horn_var machine))
78
        (reset_vars machines machine);
79
      fprintf fmt "(@[<v 0>%a %a@])" step_name node
80
        (pp_print_list (pp_horn_var machine))
81
        (step_vars_m_x machines machine);
82

    
83
      fprintf fmt "@]@ )@ ";
84
      fprintf fmt "(MAIN %a)@]@.))@.@."
85
        (pp_print_list (pp_horn_var machine))
86
        main_memory_next
87
  in
88

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

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

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

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

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

    
160
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
161
    (pp_print_list pp_type)
162
    (List.map (fun v -> v.var_type) cex_memory_next);
163

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

    
176
  fprintf fmt "@]@ )@ ";
177
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
178
    (pp_print_list (pp_horn_var machine))
179
    cex_memory_next;
180

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

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

    
219
(* Local Variables: *)
220
(* compile-command:"make -C ../.." *)
221
(* End: *)
(3-3/10)