Revision 57d61d67
Added by Pierre-Loïc Garoche over 6 years ago
src/tools/zustre/zustre_analyze.ml | ||
---|---|---|
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 |
|
|
44 | 45 |
let decl_main = |
45 | 46 |
decl_rel |
46 | 47 |
("MAIN" ^ "_" ^ node_id) |
... | ... | |
210 | 211 |
|
211 | 212 |
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status); |
212 | 213 |
match res_status with |
213 |
| Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err |
|
214 |
| Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err
|
|
214 | 215 |
|
215 | 216 |
| Z3.Solver.UNSATISFIABLE -> (*build_inv*) ( |
216 | 217 |
let expr_opt = Z3.Fixedpoint.get_answer !fp in |
... | ... | |
221 | 222 |
| Z3.Solver.UNKNOWN -> () |
222 | 223 |
with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () |
223 | 224 |
(* Local Variables: *) |
224 |
(* compile-command:"make -C ../.." *) |
|
225 |
(* compile-command:"make -C ../.. lustrev" *)
|
|
225 | 226 |
(* End: *) |
Also available in: Unified diff
New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation