Project

General

Profile

Revision 2f7c9195

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
src/tools/zustre/zustre_common.ml
116 116
  register_fdecl id.var_id fdecl;
117 117
  fdecl
118 118

  
119
let decl_rel name args =
119
let decl_rel name args_sorts =
120 120
  (*verifier ce qui est construit. On veut un declare-rel *)
121
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
121
  
122
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
122 123
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
123 124
  Z3.Fixedpoint.register_relation !fp fdecl;
124 125
  register_fdecl name fdecl;
......
772 773
	begin
773 774
	  (* Declaring single predicate *)
774 775
	  let vars = inout_vars machines m in
775
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars in
776
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
777
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
776 778
	  let horn_body, _ (* don't care for reset here *) =
777 779
	    instrs_to_expr
778 780
	      machines
......
811 813
	  (* Rule for reset *)
812 814

  
813 815
	  let vars = reset_vars machines m in
814
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars in
816
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
817
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
815 818
	  let horn_reset_body = machine_reset machines m in	    
816 819
	  let horn_reset_head = 
817 820
	    Z3.Expr.mk_app
......
828 831

  
829 832
	  (* Rule for step*)
830 833
	  let vars = step_vars machines m in
831
          let _ = decl_rel (machine_step_name m.mname.node_id) vars in
834
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
835
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
832 836
	  let horn_step_body, _ (* don't care for reset here *) =
833 837
	    instrs_to_expr
834 838
	      machines

Also available in: Unified diff