Commit 19ff80fa authored by Ocan Sankur's avatar Ocan Sankur

counterexample parsing bug fixed

parent d3c9d422
......@@ -1321,7 +1321,10 @@ constraints (x,y,_) with x>y"
(* Parse clock pred assignment of the form
p_x_y_*_k and return the corresponding clock_constraint *)
let constraint_of_asgn pr =
(*
let re = regexp "p_\\([0-9]*\\)_\\([0-9]*\\)_\\(s\\|w\\)_\\([0-9]*\\) = \\(TRUE\\|FALSE\\)" in
*)
let re = regexp "p_\\([0-9]*\\)_\\([0-9]*\\)_\\(s\\|w\\)_\\(m\\)?\\([0-9]*\\) = \\(TRUE\\|FALSE\\)" in
if not (string_match re pr 0) then None
else
let x = matched_group 1 pr |> int_of_string in
......@@ -1330,8 +1333,9 @@ constraints (x,y,_) with x>y"
"w" -> DBM_WEAK
| _ -> DBM_STRICT
in
let b = matched_group 4 pr |> int_of_string in
let inv = match matched_group 5 pr with "TRUE" -> true | _ -> false in
let sign = (try ignore(matched_group 4 pr); -1 with Not_found -> 1) in
let b = matched_group 5 pr |> int_of_string |> ( *) sign in
let inv = match matched_group 6 pr with "TRUE" -> true | _ -> false in
if inv then
Some (x,y,(b,ineq))
else Some (negate_constraint (x,y,(b,ineq)))
......@@ -1459,6 +1463,7 @@ constraints (x,y,_) with x>y"
(* Find a negative cycle in a, and add its predicates *)
let dim = Array.length a in
(* debug printing *)
printf "\n";
for i = 0 to dim -1 do
for j = 0 to dim - 1 do
......@@ -1562,8 +1567,8 @@ constraints (x,y,_) with x>y"
printf "Refine-separate for a b:\n";
printf "a is\n%s\n" (Dbm.to_string a);
printf "b is\n%s\n" (Dbm.to_string b);
printf "Found following interpolant: ";
*)
(* printf "Found following interpolant: ";*)
let interp = interpolant a b in
Log.debug (sprintf "refine_separate: Got interpolant of size %d:\n" (List.length interp));
List.iter
......@@ -1583,6 +1588,7 @@ constraints (x,y,_) with x>y"
);
acc
) (List.hd interp) (List.tl interp)
|> ignore
(*
let a' = CPAbs.over_approximate_udbm abs a in
let b' = CPAbs.over_approximate_udbm abs b in
......@@ -1941,10 +1947,13 @@ constraints (x,y,_) with x>y"
(match path.(i0) with
(Sym_Up(_,false),_) ->
Log.fatal "Encountered Sym_Up(_,false) during refinement with empty predecessor";
failwith "bug in refinement algorithm"
failwith "this must be a bug in refinement algorithm"
| (Sym_Up(_,true),_) ->
Log.debug "Irregular refinement: Up";
let ai0 = Dbm.copy aposts.(i0) in
(*
printf "Initial ai0:\n%s\n" (Dbm.to_string ai0);
*)
Dbm.up ai0;
let ai0_1 = Dbm.copy aposts.(i0+1) in
Dbm.down ai0_1;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment