Project

General

Profile

Download (7.69 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

    
18
open Format
19
open Lustre_types
20
open Machine_code_types
21

    
22
open Horn_backend_common
23
open Horn_backend_printers
24

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

    
43
  fprintf fmt "(declare-rel MAIN (%a))@."
44
    (Utils.fprintf_list ~sep:" " pp_type)
45
    (List.map (fun v -> v.var_type) main_memory_next);
46

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

    
87
  let step_name = 
88
    if Machine_code_common.is_stateless machine then 
89
      pp_machine_stateless_name
90
    else
91
      pp_machine_step_name
92
  in
93
  
94
  fprintf fmt "; Inductive def@.";
95
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
96
  fprintf fmt
97
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
98
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current
99
    step_name node
100
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
101
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
102

    
103

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

    
119

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

    
142
    (* Special case when the cex node is stateless *)
143
  let reset_name, step_name =
144
    if Machine_code_common.is_stateless machine then
145
      pp_machine_stateless_name, pp_machine_stateless_name
146
    else
147
      pp_machine_reset_name, pp_machine_step_name
148
  in
149

    
150
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
151
    (Utils.fprintf_list ~sep:" " pp_type)
152
    (List.map (fun v -> v.var_type) cex_memory_next);
153

    
154
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
155
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
156
  fprintf fmt "(rule INIT_STATE_CEX)@.";
157
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
158
  fprintf fmt "INIT_STATE_CEX@ ";
159
  fprintf fmt "(@[<v 0>%a %a@])@ "
160
    reset_name node
161
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
162
  fprintf fmt "(@[<v 0>%a %a@])"
163
    step_name node
164
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
165
  
166
  fprintf fmt "@]@ )@ ";
167
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
168
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ;
169

    
170
  fprintf fmt "; Inductive def@.";
171
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
172
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
173
  fprintf fmt "(declare-var cexcpt Int)@.";
174
  fprintf fmt
175
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
176
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current
177
    step_name node
178
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
179
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
180

    
181
let get_cex machines fmt machine =
182
    let cex_input =
183
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
184
    in
185
    let cex_output =
186
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
187
    in
188
  let cex_memory_next =
189
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
190
  in
191
  fprintf fmt "; Property def@.";
192
  fprintf fmt "(declare-rel CEXTRACE ())@.";
193
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
194
    (pp_conj (pp_horn_var machine)) cex_output
195
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
196
    ;
197
  fprintf fmt "(query CEXTRACE)@."
198

    
199
(* Local Variables: *)
200
(* compile-command:"make -C ../.." *)
201
(* End: *)
(2-2/5)