Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_analyze.ml @ 3d3718ae

History | View | Annotate | Download (6.85 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_input = 
27
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
28
  in  
29
  let main_input_dummy = 
30
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
31
  in  
32
  let main_memory_next =
33
    main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
34
      main_output
35
  in
36
  let main_memory_current =
37
    main_input_dummy @ (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
38
      main_output_dummy
39
  in
40

    
41
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42
     Faut-il declarer les "rel" dans la hashtbl ?
43
  *)
44
  let decl_main = decl_rel "MAIN" main_memory_next in
45

    
46
  
47
  
48
  (* Init case *)
49
  let decl_init = decl_rel "INIT_STATE" [] in
50

    
51
  (* (special) rule INIT_STATE *)
52
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
53
  Z3.Fixedpoint.add_rule !fp init_expr None;
54
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
55
  (* 			 !ctx *)
56
  (* 			 decl_init *)
57
  (* 			 [] *)
58
  (* )  in *)
59

    
60
  (* Re-declaring variables *)
61
  let _ = List.map decl_var main_memory_next in
62

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

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

    
99
	(* Re-declaring variables *)
100
	let vars_reset = reset_vars machines machine in
101
	let vars_step = step_vars_m_x machines machine in
102
	let vars_step_all = step_vars_c_m_x machines machine in
103
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in
104

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

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

    
136
  List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy);
137
  
138
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
139

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

    
167

    
168
  (* Property def *)
169
  let decl_err = decl_rel "ERR" [] in
170

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

    
193
      (* Debug instructions *)
194
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
195
  if true then
196
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
197
    (Utils.fprintf_list ~sep:"@ "
198
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
199
    rules_expr;
200
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
201

    
202
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
203
  match res_status with
204
  | Z3.Solver.SATISFIABLE -> (
205
     (*Zustre_cex.build_cex decl_err*)
206
    let expr1_opt = Z3.Fixedpoint.get_answer !fp in
207
    let expr2_opt = Z3.Fixedpoint.get_ground_sat_answer !fp in 
208
       match expr1_opt, expr2_opt with
209
	 None, None -> Format.eprintf "Sat No feedback@."
210
       | Some e, Some e2 -> Format.eprintf "Sat Result: %s, %s@."
211
					   (Z3.Expr.to_string e)
212
					   (Z3.Expr.to_string e2)
213
       | _ -> assert false
214
  )
215
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
216
       let expr_opt = Z3.Fixedpoint.get_answer !fp in
217
       match expr_opt with
218
	 None -> Format.eprintf "Unsat No feedback@."
219
       | Some e -> Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
220
  )
221
  | Z3.Solver.UNKNOWN -> ()
222
      
223
(* Local Variables: *)
224
(* compile-command:"make -C ../.." *)
225
(* End: *)