Project

General

Profile

« Previous | Next » 

Revision 57d61d67

Added by Pierre-Loïc Garoche over 6 years ago

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

View differences:

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