Revision 2f7c9195
Added by Pierre-Loïc Garoche over 5 years ago
| 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
zustre progress. Issues with sliced predicates