Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (7.03 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 LustreSpec
20
open Corelang
21
open Machine_code
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
  (* Special case when the main node is stateless *)
45
  let reset_name, step_name =
46
    if is_stateless machine then
47
      pp_machine_stateless_name, pp_machine_stateless_name
48
    else
49
      pp_machine_reset_name, pp_machine_step_name
50
  in
51

    
52
  fprintf fmt "(declare-rel MAIN (%a))@."
53
    (Utils.fprintf_list ~sep:" " pp_type)
54
    (List.map (fun v -> v.var_type) main_memory_next);
55

    
56
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
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@])@ "
62
    reset_name node
63
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
64
  fprintf fmt "(@[<v 0>%a %a@])"
65
    step_name node
66
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
67
    
68
  fprintf fmt "@]@ )@ ";
69
  fprintf fmt "(MAIN %a)@]@.))@.@."
70
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
71

    
72
  fprintf fmt "; Inductive def@.";
73
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
74
  fprintf fmt
75
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
76
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current
77
    step_name node
78
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
79
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
80

    
81

    
82
let check_prop machines fmt node machine =
83
  let main_output =
84
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
85
  in
86
  let main_memory_next =
87
    (rename_next_list (full_memory_vars machines machine)) @ main_output
88
  in
89
  fprintf fmt "; Property def@.";
90
  fprintf fmt "(declare-rel ERR ())@.";
91
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
92
    (pp_conj (pp_horn_var machine)) main_output
93
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
94
    ;
95
   if !Options.horn_query then fprintf fmt "(query ERR)@."
96

    
97

    
98
let cex_computation machines fmt node machine =
99
  fprintf fmt "; CounterExample computation for node %s@.@." node;
100
    (* We print the types of the cex node "memory tree" TODO: add the output *)
101
  let cex_input =
102
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
103
  in
104
  let cex_input_dummy =
105
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
106
  in
107
  let cex_output =
108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
109
  in
110
  let cex_output_dummy =
111
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
112
  in
113
  let cex_memory_next =
114
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
115
  in
116
  let cex_memory_current =
117
    cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
118
  in
119

    
120
    (* Special case when the cex node is stateless *)
121
  let reset_name, step_name =
122
    if is_stateless machine then
123
      pp_machine_stateless_name, pp_machine_stateless_name
124
    else
125
      pp_machine_reset_name, pp_machine_step_name
126
  in
127

    
128
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
129
    (Utils.fprintf_list ~sep:" " pp_type)
130
    (List.map (fun v -> v.var_type) cex_memory_next);
131

    
132
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
133
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
134
  fprintf fmt "(rule INIT_STATE_CEX)@.";
135
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
136
  fprintf fmt "INIT_STATE_CEX@ ";
137
  fprintf fmt "(@[<v 0>%a %a@])@ "
138
    reset_name node
139
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
140
  fprintf fmt "(@[<v 0>%a %a@])"
141
    step_name node
142
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
143
  
144
  fprintf fmt "@]@ )@ ";
145
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
146
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ;
147

    
148
  fprintf fmt "; Inductive def@.";
149
  (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
150
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_output_dummy;
151
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
152
  fprintf fmt "(declare-var cexcpt Int)@.";
153
  fprintf fmt
154
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
155
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current
156
    step_name node
157
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
158
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
159

    
160
let get_cex machines fmt node machine =
161
    let cex_input =
162
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
163
    in
164
    let cex_output =
165
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
166
    in
167
  let cex_memory_next =
168
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
169
  in
170
  fprintf fmt "; Property def@.";
171
  fprintf fmt "(declare-rel CEXTRACE ())@.";
172
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
173
    (pp_conj (pp_horn_var machine)) cex_output
174
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
175
    ;
176
  fprintf fmt "(query CEXTRACE)@."
177

    
178
(* Local Variables: *)
179
(* compile-command:"make -C ../.." *)
180
(* End: *)