Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_analyze.ml @ dbab1fe5

History | View | Annotate | Download (5.84 KB)

1
(* This module takes a main node (reset and step) and a property. It assumes
2
   that the system is properly defined and check that the property is valid. 
3

    
4
   When valid, it returns a set of local invariants. Otherwise, it returns a cex
5
   expressed as a sequence of input values.
6

    
7
*)
8
open Lustre_types
9
open Machine_code_types
10
open Machine_code_common
11
open Zustre_common
12
open Zustre_data
13

    
14
let check machines node =
15

    
16
  let machine = get_machine machines node in
17

    
18
  (* Declaring collecting semantics *)
19
  
20
  let main_output =
21
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
22
  in
23
  let main_output_dummy =
24
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
25
  in
26
  let main_memory_next =
27
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
28
      main_output
29
  in
30
  let main_memory_current =
31
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
32
      main_output_dummy
33
  in
34

    
35
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
36
     Faut-il declarer les "rel" dans la hashtbl ?
37
  *)
38
  let decl_main = decl_rel "MAIN" main_memory_next in
39

    
40
  
41
  
42
  (* Init case *)
43
  let decl_init = decl_rel "INIT_STATE" [] in
44

    
45
  (* (special) rule INIT_STATE *)
46
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
47
  Z3.Fixedpoint.add_rule !fp init_expr None;
48
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
49
  (* 			 !ctx *)
50
  (* 			 decl_init *)
51
  (* 			 [] *)
52
  (* )  in *)
53

    
54
  (* Re-declaring variables *)
55
  let _ = List.map decl_var main_memory_next in
56

    
57
  let horn_head = 
58
    Z3.Expr.mk_app
59
      !ctx
60
      decl_main
61
      (List.map horn_var_to_expr main_memory_next)
62
  in
63
  (* Special case when the main node is stateless *)
64
  let _ =
65
    if Machine_code_common.is_stateless machine then
66
      begin
67
	
68
	(* Initial set: One Step(m,x)  -- Stateless node  *)	
69
     	(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)
70

    
71
	(* Note that vars here contains main_memory_next *)
72
	let vars = step_vars_m_x machines machine in
73
	(* Re-declaring variables *)
74
	let _ = List.map decl_var vars in
75
	
76
	let horn_body =
77
	  Z3.Boolean.mk_and !ctx
78
	    [
79
	      Z3.Expr.mk_app !ctx decl_init [];
80
	      Z3.Expr.mk_app !ctx
81
		(get_fdecl (machine_stateless_name node))
82
		(List.map horn_var_to_expr vars) 
83
	    ]
84
	in
85
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
86
	  
87
	  
88
      end
89
    else
90
      begin
91
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)
92

    
93
	(* Re-declaring variables *)
94
	let vars_reset = reset_vars machines machine in
95
	let vars_step = step_vars_m_x machines machine in
96
	let vars_step_all = step_vars_c_m_x machines machine in
97
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in
98

    
99
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
100
	let horn_body =
101
	  Z3.Boolean.mk_and !ctx
102
	    [
103
	      Z3.Expr.mk_app !ctx decl_init [];
104
	      Z3.Expr.mk_app !ctx
105
		(get_fdecl (machine_reset_name node))
106
		(List.map horn_var_to_expr (reset_vars machines machine));
107
	      Z3.Expr.mk_app !ctx
108
		(get_fdecl (machine_step_name node))
109
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
110
	    ]
111
	in
112

    
113
	(* Vars contains all vars: in_out, current, mid, neXt memories *)
114
	let vars = step_vars_c_m_x machines machine in
115
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
116
	  
117
	  
118
      end
119
  in
120
  
121
  let step_name = 
122
    if Machine_code_common.is_stateless machine then 
123
      machine_stateless_name
124
    else
125
      machine_step_name
126
  in
127
  
128
  (* ; Inductive def@. *)
129

    
130
  List.iter (fun x -> ignore (decl_var x)) main_output_dummy;
131
  
132
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
133

    
134
  (* fprintf fmt *)
135
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
136
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
137
  (*   step_name node *)
138
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
139
  
140
  
141
  let horn_head = 
142
    Z3.Expr.mk_app
143
      !ctx
144
      decl_main
145
      (List.map horn_var_to_expr main_memory_next)
146
  in
147
  let horn_body =
148
    Z3.Boolean.mk_and !ctx
149
      [
150
	Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_current);
151
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
152
      ]
153
  in
154
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
155
  let vars = (step_vars_c_m_x machines machine) @ main_output_dummy in
156
  let _ =
157
    add_rule ~dont_touch:[decl_main] vars  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
158
      
159
  in
160

    
161

    
162
  (* Property def *)
163
  let decl_err = decl_rel "ERR" [] in
164

    
165
  let prop =
166
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
167
  in
168
  let not_prop =
169
    Z3.Boolean.mk_not !ctx prop
170
  in
171
  add_rule (*~dont_touch:[decl_main;decl_err]*) main_memory_next (Z3.Boolean.mk_implies !ctx
172
	      (
173
		Z3.Boolean.mk_and !ctx
174
		  [not_prop;
175
		   Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_next);
176
		  ]
177
	      )
178
	      (Z3.Expr.mk_app !ctx decl_err []))
179
  ;
180
  
181
      (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." *)
182
      (*   (pp_conj (pp_horn_var machine)) main_output *)
183
      (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *)
184
      (*   ; *)
185
      (*  if !Options.horn_query then fprintf fmt "(query ERR)@." *)
186

    
187
      (* Debug instructions *)
188
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
189
  if false then
190
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
191
    (Utils.fprintf_list ~sep:"@ "
192
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
193
    rules_expr;
194
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
195

    
196
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
197

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