Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (7.72 KB)

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 Corelang
21
open Machine_code_types
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
  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
  
49
  (* Init case *)
50
  let _ = 
51
    (* Special case when the main node is stateless *)
52
    if Machine_code_common.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

    
88
  let step_name = 
89
    if Machine_code_common.is_stateless machine then 
90
      pp_machine_stateless_name
91
    else
92
      pp_machine_step_name
93
  in
94
  
95
  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
   if !Options.horn_query then fprintf fmt "(query ERR)@."
119

    
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 Machine_code_common.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: *)