Project

General

Profile

Revision 2f7c9195 src/tools/zustre/zustre_analyze.ml

View differences:

src/tools/zustre/zustre_analyze.ml
14 14
let check machines node =
15 15

  
16 16
  let machine = get_machine machines node in
17

  
17
  let node_id = machine.mname.node_id in
18 18
  (* Declaring collecting semantics *)
19 19
  
20 20
  let main_output =
21
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
21
    rename_machine_list node_id machine.mstep.step_outputs
22 22
  in
23 23
  let main_output_dummy =
24
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
24
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
25 25
  in
26 26
  let main_input = 
27
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
27
    rename_machine_list node_id machine.mstep.step_inputs
28 28
  in  
29 29
  let main_input_dummy = 
30
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
30
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
31 31
  in  
32 32
  let main_memory_next =
33 33
    main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
......
41 41
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42 42
     Faut-il declarer les "rel" dans la hashtbl ?
43 43
  *)
44
  let decl_main = decl_rel "MAIN" main_memory_next in
44
  let decl_main =
45
    decl_rel
46
      ("MAIN" ^ "_" ^ node_id)
47
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
45 48

  
46 49
  
47 50
  
......
64 67
    Z3.Expr.mk_app
65 68
      !ctx
66 69
      decl_main
67
      (List.map horn_var_to_expr main_memory_next)
70
      ((Z3.Arithmetic.Integer.mk_numeral_i !ctx 0)::(List.map horn_var_to_expr main_memory_next))
68 71
  in
69 72
  (* Special case when the main node is stateless *)
70 73
  let _ =
......
142 145
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
143 146
  (*   step_name node *)
144 147
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
145
  
148

  
149
  let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in
150
  let k_var = decl_var k in
146 151
  
147 152
  let horn_head = 
148 153
    Z3.Expr.mk_app
149 154
      !ctx
150 155
      decl_main
151
      (List.map horn_var_to_expr main_memory_next)
156
      ((Z3.Arithmetic.mk_add
157
	  !ctx
158
	  [Z3.Expr.mk_const_f !ctx k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
159
       )::(List.map horn_var_to_expr main_memory_next))
152 160
  in
153 161
  let horn_body =
154 162
    Z3.Boolean.mk_and !ctx
155 163
      [
156
	Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_current);
164
	Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::(List.map horn_var_to_expr main_memory_current));
157 165
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
158 166
      ]
159 167
  in
160 168
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
161 169
  let vars = (step_vars_c_m_x machines machine) @ main_output_dummy @ main_input_dummy  in
162 170
  let _ =
163
    add_rule ~dont_touch:[decl_main] vars  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
171
    add_rule ~dont_touch:[decl_main] (k::vars)  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
164 172
      
165 173
  in
166 174

  
......
174 182
  let not_prop =
175 183
    Z3.Boolean.mk_not !ctx prop
176 184
  in
177
  add_rule (*~dont_touch:[decl_main;decl_err]*) main_memory_next (Z3.Boolean.mk_implies !ctx
185
  add_rule (*~dont_touch:[decl_main;decl_err]*) (k::main_memory_next) (Z3.Boolean.mk_implies !ctx
178 186
	      (
179 187
		Z3.Boolean.mk_and !ctx
180 188
		  [not_prop;
181
		   Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_next);
189
		   Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::List.map horn_var_to_expr main_memory_next);
182 190
		  ]
183 191
	      )
184 192
	      (Z3.Expr.mk_app !ctx decl_err []))
......
201 209

  
202 210
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
203 211
  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
  )
212
  | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
213
  
215 214
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
216 215
       let expr_opt = Z3.Fixedpoint.get_answer !fp in
217 216
       match expr_opt with

Also available in: Unified diff