Skip to content

Commit 25ae26e

Browse files
wimmerswimmers
committed
Print origin states in invariant debugger
1 parent 290b711 commit 25ae26e

File tree

4 files changed

+102
-35
lines changed

4 files changed

+102
-35
lines changed

‎ML/Certificate.ML

Lines changed: 42 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8042,10 +8042,21 @@ fun check_invariant_fail_impl A_ (B1_, B2_, B3_) copyi lei succsi =
80428042
(fn () => (if x_q then NONE else SOME xp))))
80438043
NONE)
80448044
()) ())
8045-
(fn x_o =>
8046-
(fn () =>
8047-
(case x_o of NONE => NONE
8048-
| SOME x_p => SOME (Inr (xb, (a1, (x_p, x_m)))))))))
8045+
(fn aa =>
8046+
(case aa of NONE => (fn () => NONE)
8047+
| SOME x_p =>
8048+
(fn f_ => fn () => f_
8049+
((hms_lookup
8050+
(ht_lookup (B1_, B2_, B3_) (heap_list A_))
8051+
(heap_map copyi) xb bi)
8052+
()) ())
8053+
(fn x_q =>
8054+
(fn () =>
8055+
(case x_q
8056+
of NONE => SOME (Inl (Inr (xb, (a1, x_m))))
8057+
| SOME x_r =>
8058+
SOME (Inr
8059+
(xb, (x_r, (a1, (x_p, x_m))))))))))))
80498060
else (fn () => (SOME (Inl (Inl (xb, (a1, a2)))))))))
80508061
end
80518062
()) ())
@@ -12873,7 +12884,7 @@ then SOME p else NONE))
1287312884
end)
1287412885
end)
1287512886
end
12876-
| SOME (Inr (l, (la, (ma, xs)))) =>
12887+
| SOME (Inr (l, (asa, (la, (ma, xs))))) =>
1287712888
(fn f_ => fn () => f_ ((show_statea l) ()) ())
1287812889
(fn s1 =>
1287912890
(fn f_ => fn () => f_ ((show_statea la) ()) ())
@@ -12884,9 +12895,6 @@ then SOME p else NONE))
1288412895
val _ =
1288512896
writeln ("\nA successor of the zones for:\n " ^
1288612897
s1);
12887-
val _ = writeln ("is not subsumed:\n " ^ s2);
12888-
val _ = writeln (implode s3 ^ "\n");
12889-
val _ = writeln "These are the candidate dbms:";
1289012898
in
1289112899
(fn f_ => fn () => f_
1289212900
((fold_map
@@ -12898,13 +12906,33 @@ then SOME p else NONE))
1289812906
in
1289912907
(fn () => ())
1290012908
end))
12901-
xs)
12909+
asa)
1290212910
()) ())
12903-
(fn _ => let
12904-
val _ = writeln "";
12905-
in
12906-
(fn () => ())
12907-
end)
12911+
(fn _ =>
12912+
let
12913+
val _ =
12914+
writeln ("\nis not subsumed:\n " ^ s2 ^ "\n");
12915+
val _ = writeln (implode s3 ^ "\n");
12916+
val _ =
12917+
writeln "These are the candidate dbms:";
12918+
in
12919+
(fn f_ => fn () => f_
12920+
((fold_map
12921+
(fn mb =>
12922+
(fn f_ => fn () => f_ ((show_dbm mb) ()) ())
12923+
(fn s => let
12924+
val _ = writeln ("\n" ^ implode s);
12925+
in
12926+
(fn () => ())
12927+
end))
12928+
xs)
12929+
()) ())
12930+
(fn _ => let
12931+
val _ = writeln "";
12932+
in
12933+
(fn () => ())
12934+
end)
12935+
end)
1290812936
end))))))
1290912937
end);
1291012938

‎ML/Certificate.sml

Lines changed: 42 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8075,10 +8075,21 @@ fun check_invariant_fail_impl A_ (B1_, B2_, B3_) copyi lei succsi =
80758075
(fn () => (if x_q then NONE else SOME xp))))
80768076
NONE)
80778077
()) ())
8078-
(fn x_o =>
8079-
(fn () =>
8080-
(case x_o of NONE => NONE
8081-
| SOME x_p => SOME (Inr (xb, (a1, (x_p, x_m)))))))))
8078+
(fn aa =>
8079+
(case aa of NONE => (fn () => NONE)
8080+
| SOME x_p =>
8081+
(fn f_ => fn () => f_
8082+
((hms_lookup
8083+
(ht_lookup (B1_, B2_, B3_) (heap_list A_))
8084+
(heap_map copyi) xb bi)
8085+
()) ())
8086+
(fn x_q =>
8087+
(fn () =>
8088+
(case x_q
8089+
of NONE => SOME (Inl (Inr (xb, (a1, x_m))))
8090+
| SOME x_r =>
8091+
SOME (Inr
8092+
(xb, (x_r, (a1, (x_p, x_m))))))))))))
80828093
else (fn () => (SOME (Inl (Inl (xb, (a1, a2)))))))))
80838094
end
80848095
()) ())
@@ -12906,7 +12917,7 @@ then SOME p else NONE))
1290612917
end)
1290712918
end)
1290812919
end
12909-
| SOME (Inr (l, (la, (ma, xs)))) =>
12920+
| SOME (Inr (l, (asa, (la, (ma, xs))))) =>
1291012921
(fn f_ => fn () => f_ ((show_statea l) ()) ())
1291112922
(fn s1 =>
1291212923
(fn f_ => fn () => f_ ((show_statea la) ()) ())
@@ -12917,9 +12928,6 @@ then SOME p else NONE))
1291712928
val _ =
1291812929
writeln ("\nA successor of the zones for:\n " ^
1291912930
s1);
12920-
val _ = writeln ("is not subsumed:\n " ^ s2);
12921-
val _ = writeln (implode s3 ^ "\n");
12922-
val _ = writeln "These are the candidate dbms:";
1292312931
in
1292412932
(fn f_ => fn () => f_
1292512933
((fold_map
@@ -12931,13 +12939,33 @@ then SOME p else NONE))
1293112939
in
1293212940
(fn () => ())
1293312941
end))
12934-
xs)
12942+
asa)
1293512943
()) ())
12936-
(fn _ => let
12937-
val _ = writeln "";
12938-
in
12939-
(fn () => ())
12940-
end)
12944+
(fn _ =>
12945+
let
12946+
val _ =
12947+
writeln ("\nis not subsumed:\n " ^ s2 ^ "\n");
12948+
val _ = writeln (implode s3 ^ "\n");
12949+
val _ =
12950+
writeln "These are the candidate dbms:";
12951+
in
12952+
(fn f_ => fn () => f_
12953+
((fold_map
12954+
(fn mb =>
12955+
(fn f_ => fn () => f_ ((show_dbm mb) ()) ())
12956+
(fn s => let
12957+
val _ = writeln ("\n" ^ implode s);
12958+
in
12959+
(fn () => ())
12960+
end))
12961+
xs)
12962+
()) ())
12963+
(fn _ => let
12964+
val _ = writeln "";
12965+
in
12966+
(fn () => ())
12967+
end)
12968+
end)
1294112969
end))))))
1294212970
end);
1294312971

‎Simple_Networks/Simple_Network_Language_Certificate_Checking.thy

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1438,12 +1438,17 @@ definition
14381438
}) xs;
14391439
Heap_Monad.return ()
14401440
}
1441-
| Some (Inr (l, l', M, xs)) \<Rightarrow> do {
1441+
| Some (Inr (l, as, l', M, xs)) \<Rightarrow> do {
14421442
s1 \<leftarrow> show_state l;
14431443
s2 \<leftarrow> show_state l';
14441444
s3 \<leftarrow> show_dbm M;
14451445
let _ = println (STR ''\<newline>A successor of the zones for:\<newline> '' + s1);
1446-
let _ = println (STR ''is not subsumed:\<newline> '' + s2);
1446+
Heap_Monad.fold_map (\<lambda>M. do {
1447+
s \<leftarrow> show_dbm M;
1448+
let _ = println (STR ''\<newline>'' + String.implode s);
1449+
Heap_Monad.return ()
1450+
}) as;
1451+
let _ = println (STR ''\<newline>is not subsumed:\<newline> '' + s2 + STR ''\<newline>'');
14471452
let _ = println (String.implode s3 + STR ''\<newline>'');
14481453
let _ = println (STR ''These are the candidate dbms:'');
14491454
Heap_Monad.fold_map (\<lambda>M. do {

‎Worklist_Algorithms/Unreachability_Certification.thy

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -922,8 +922,8 @@ definition
922922
l \<leftarrow> SPEC (\<lambda>xs. set xs = L');
923923
monadic_list_all_fail' (\<lambda>l.
924924
do {
925-
case op_map_lookup l M' of None \<Rightarrow> RETURN None | Some xs \<Rightarrow> do {
926-
let succs = PR_CONST succs l xs;
925+
case op_map_lookup l M' of None \<Rightarrow> RETURN None | Some as \<Rightarrow> do {
926+
let succs = PR_CONST succs l as;
927927
monadic_list_all_fail' (\<lambda>(l', xs). do {
928928
xs \<leftarrow> SPEC (\<lambda>xs'. set xs' = xs);
929929
if xs = [] then RETURN None
@@ -935,8 +935,14 @@ definition
935935
b2 \<leftarrow> monadic_list_all_fail (\<lambda>x'.
936936
monadic_list_ex (\<lambda>y. RETURN (PR_CONST less_eq x' y)) ys
937937
) xs;
938-
case b2 of None \<Rightarrow> RETURN None | Some M \<Rightarrow> RETURN (Some (Inr (l, l', M, ys)))
939-
}
938+
case b2 of None \<Rightarrow> RETURN None | Some M \<Rightarrow> do {
939+
case op_map_lookup l M' of
940+
None \<Rightarrow> RETURN (Some (Inl (Inr (l, l', ys)))) \<comment> \<open>never used\<close>
941+
| Some as \<Rightarrow> do {
942+
as \<leftarrow> SPEC (\<lambda>xs'. set xs' = as);
943+
RETURN (Some (Inr (l, as, l', M, ys)))}
944+
}
945+
}
940946
}
941947
else RETURN (Some (Inl (Inl (l, l', xs))))
942948
}
@@ -949,7 +955,7 @@ definition
949955
sepref_thm check_invariant_fail_impl is
950956
"uncurry check_invariant_fail"
951957
:: "(lso_assn K)\<^sup>k *\<^sub>a table_assn\<^sup>k \<rightarrow>\<^sub>a
952-
option_assn ((K \<times>\<^sub>a K \<times>\<^sub>a list_assn A +\<^sub>a K \<times>\<^sub>a K \<times>\<^sub>a list_assn A) +\<^sub>a K \<times>\<^sub>a K \<times>\<^sub>a A \<times>\<^sub>a list_assn A)"
958+
option_assn ((K \<times>\<^sub>a K \<times>\<^sub>a list_assn A +\<^sub>a K \<times>\<^sub>a K \<times>\<^sub>a list_assn A) +\<^sub>a K \<times>\<^sub>a list_assn A \<times>\<^sub>a K \<times>\<^sub>a A \<times>\<^sub>a list_assn A)"
953959
unfolding PR_CONST_def
954960
unfolding check_invariant_fail_def list_of_set_def[symmetric]
955961
unfolding monadic_list_all_fail'_alt_def monadic_list_all_fail_alt_def

0 commit comments

Comments
 (0)