Skip to content

fix broken proofs in examples #244

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
muenchnerkindl merged 1 commit into from
Dec 8, 2025
Merged

fix broken proofs in examples #244

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 31 additions & 43 deletions examples/AtomicBakery.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ EXTENDS Naturals, TLAPS
(* is a natural number. *)
(***************************************************************************)
CONSTANT N
ASSUME N \in Nat
ASSUME NAssumption == N \in Nat

(***************************************************************************)
(* We define P to be the set {1, 2, ... , N} of processes. *)
Expand Down Expand Up @@ -67,7 +67,7 @@ p4: flag[self] := FALSE;
unread := P \ {self} ;
p5: while (unread # {}) {
with (i \in unread) { nxt := i ; };
await ~ flag[nxt];
await (flag[nxt] = FALSE);
p6: await \/ num[nxt] = 0
\/ LL(self, nxt) ;
unread := unread \ {nxt};
Expand All @@ -79,7 +79,7 @@ p7: num[self] := 0;
**** this ends the comment containg the pluscal code **********)

\* BEGIN TRANSLATION (this begins the translation of the PlusCal code)
VARIABLES num, flag, pc
VARIABLES pc, num, flag

(* define statement *)
LL(j, i) == \/ num[j] < num[i]
Expand All @@ -88,7 +88,7 @@ LL(j, i) == \/ num[j] < num[i]

VARIABLES unread, max, nxt

vars == << num, flag, pc, unread, max, nxt >>
vars == << pc, num, flag, unread, max, nxt >>

ProcSet == (P)

Expand Down Expand Up @@ -136,7 +136,7 @@ p5(self) == /\ pc[self] = "p5"
/\ IF unread[self] # {}
THEN /\ \E i \in unread[self]:
nxt' = [nxt EXCEPT ![self] = i]
/\ ~ flag[nxt'[self]]
/\ (flag[nxt'[self]] = FALSE)
/\ pc' = [pc EXCEPT ![self] = "p6"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ nxt' = nxt
Expand Down Expand Up @@ -192,6 +192,13 @@ TypeOK == /\ num \in [P -> Nat]
/\ pc \in
[P -> {"p1", "p2", "p3", "p4", "p5", "p6", "cs", "p7"}]

THEOREM Typing == Spec => []TypeOK
<1>. USE DEF ProcSet, TypeOK
<1>1. Init => TypeOK
BY DEF Init
<1>2. TypeOK /\ [Next]_vars => TypeOK'
BY DEF Next, vars, p, p1, p2, p3, p4, p5, p6, p7, cs
<1>. QED BY <1>1, <1>2, PTL DEF Spec

(***************************************************************************)
(* After(i, j) is a condition that implies that num[j] > 0 and, if i is *)
Expand Down Expand Up @@ -226,9 +233,9 @@ IInv(i) ==
/\ (pc[i] \in {"cs", "p7"}) => \A j \in P \ {i} : After(j, i)

(***************************************************************************)
(* Inv is the complete inductive invariant. *)
(* Inv is the main inductive invariant, modulo type correctness. *)
(***************************************************************************)
Inv == TypeOK /\ \A i \in P : IInv(i)
Inv == \A i \in P : IInv(i)
-----------------------------------------------------------------------------
(***************************************************************************)
(* Proof of Mutual Exclusion *)
Expand All @@ -238,54 +245,35 @@ Inv == TypeOK /\ \A i \in P : IInv(i)
(* which Inv is true leaves Inv true. Step <1>4 follows easily from *)
(* <1>1-<1>3 by simple temporal reasoning. *)
(***************************************************************************)
THEOREM Spec => []Inv
<1> USE DEFS TypeOK, Inv, IInv, ProcSet
<1>1. Init => Inv
BY DEFS Init, Inv
<1>2. Inv /\ [Next]_vars => Inv'
<2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv'
OBVIOUS
<2> USE DEFS After, LL
THEOREM Spec => []MutualExclusion
<1>. USE NAssumption DEFS ProcSet, TypeOK
<1>1. Init => Inv
BY DEF Init, Inv, IInv
<1>2. TypeOK /\ Inv /\ [Next]_vars => Inv'
<2>. SUFFICES ASSUME TypeOK, Inv, Next
PROVE Inv'
BY DEF Inv, IInv, After, LL, vars
<2>. USE DEFS Inv, IInv, After, LL, P
<2>1. ASSUME NEW self \in P, p1(self) PROVE Inv'
BY <2>1 DEF p1
<2>2. ASSUME NEW self \in P, p2(self) PROVE Inv'
<3>1. CASE unread[self] = {}
BY <2>2, <3>1 DEF p2
<3>2. CASE unread[self] # {}
BY <2>2, <3>2 DEF p2
<3>3. QED
BY <3>1, <3>2
BY <2>2 DEF p2
<2>3. ASSUME NEW self \in P, p3(self) PROVE Inv'
BY <2>3 DEF p3
<2>4. ASSUME NEW self \in P, p4(self) PROVE Inv'
BY <2>4 DEF p4
<2>5. ASSUME NEW self \in P, p5(self) PROVE Inv'
<3>1. CASE unread[self] = {}
BY <2>5, <3>1 DEF p5
<3>2. CASE unread[self] # {}
BY <2>5, <3>2, CVC4T(30) DEF p5
<3>3. QED
BY <3>1, <3>2
BY <2>5, SMTT(20) DEF p5
<2>6. ASSUME NEW self \in P, p6(self) PROVE Inv'
<3>p. P \subseteq Nat
BY N \in Nat DEF P
<3>1. CASE num[nxt[self]] = 0
BY <2>6, <3>1 DEF p6
<3>2. CASE LL(self, nxt[self])
BY <2>6, <3>2, <3>p DEF p6
<3>3. QED
BY <2>6, <3>1, <3>2 DEF p6
BY <2>6, SMTT(20) DEF p6
<2>7. ASSUME NEW self \in P, cs(self) PROVE Inv'
BY <2>7 DEF cs
BY <2>7, SMTT(20) DEF cs
<2>8. ASSUME NEW self \in P, p7(self) PROVE Inv'
BY <2>8 DEF p7
<2>9. CASE UNCHANGED vars
BY <2>9 DEF vars
<2>10. QED
BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, p
<2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF Next, p
<1>3. Inv => MutualExclusion
BY DEFS Inv, After, MutualExclusion
<1>4. QED
BY <1>1, <1>2, <1>3, PTL DEF Spec
BY DEF Inv, IInv, After, MutualExclusion
<1>. QED BY <1>1, <1>2, <1>3, Typing, PTL DEF Spec

=============================================================================

35 changes: 24 additions & 11 deletions examples/AtomicBakeryWithoutSMT.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,26 +198,31 @@ Inv == TypeOK /\ \A i \in P : IInv(i)
-----------------------------------------------------------------------------

THEOREM GTAxiom == \A n, m \in Nat : ~ (n > m /\ m > n)
OBVIOUS (*{ by (isabelle "(auto dest: nat_less_trans)") }*)
BY Isa

THEOREM GEQAxiom == \A n, m \in Nat : (n = m) \/ n > m \/ m > n
OBVIOUS (*{ by (isabelle "(auto elim: nat_less_cases)") }*)
BY Isa

THEOREM GEQTransitive == \A n, m, q \in Nat : n >= m /\ m >= q => n >= q
OBVIOUS (*{ by (isabelle "(auto dest: nat_leq_trans)") }*)
OBVIOUS (*{ by (isabelle "(auto dest: int_leq_trans)") }*)

THEOREM Transitivity2 == \A n, m, q \in Nat : n > m /\ m >= q => n > q
OBVIOUS (*{ by (isabelle "(auto dest: nat_leq_less_trans)") }*)
OBVIOUS (*{ by (isabelle "(auto dest: int_leq_less_trans)") }*)

THEOREM GEQorLT == \A n, m \in Nat : n >= m <=> ~(m > n)
OBVIOUS (*{ by (isabelle "(auto simp: nat_not_less[simplified])") }*)
BY Isa
\* OBVIOUS (*{ by (isabelle "(auto simp: nat_not_less[simplified])") }*)

THEOREM NatGEQZero == \A n \in Nat: (n > 0) <=> (n # 0)
OBVIOUS (*{ by (isabelle "(auto simp: nat_gt0_not0)") }*)
BY Isa
\* OBVIOUS (*{ by (isabelle "(auto simp: nat_gt0_not0)") }*)

THEOREM Plus1 == \A n \in Nat: n+1 \in Nat /\ n+1 # 0
BY Isa

THEOREM Plus1GT == \A n \in Nat : n+1 > n
BY Isa

THEOREM GGIrreflexive == ASSUME NEW i \in P,
NEW j \in P,
i # j,
Expand Down Expand Up @@ -390,13 +395,21 @@ THEOREM InductiveInvariant == Inv /\ Next => Inv'
(* We start by proving two auxiliary assertions *)
<2>1. max'[self] >= max[self] /\ max'[self] >= num[k]
<3>1. CASE num[k] > max[self]
BY <3>1, k \in P, SimplifyAndSolve
(* FIXME: Isabelle needs "k \in P" but doesn't find it by itself *)
<4>. /\ k \in P
/\ num[k] \in Nat
/\ max'[self] = num[k]
BY <3>1, Zenon
<4>. QED BY <3>1, Isa
<3>2. CASE ~(num[k] > max[self])
<4>. /\ max[self] \in Nat
/\ UNCHANGED max
BY <3>2, Zenon
<4>1. max[self] >= num[k]
BY <3>2, GEQorLT, Zenon
<4>2. QED
BY <3>2, <4>1, SimplifyAndSolve
<4>2. max[self] >= max[self]
BY Isa
<4>. QED
BY <3>2, <4>1, <4>2, Zenon
<3>3. QED
BY <3>1, <3>2, Zenon
<2>2. After(self,i) => After(self,i)'
Expand Down Expand Up @@ -438,7 +451,7 @@ THEOREM InductiveInvariant == Inv /\ Next => Inv'
<4>1. max[j] >= num[i]
BY <3>1, Zenon DEF After
<4>2. num'[j] > max[j]
BY SimplifyAndSolve
BY Plus1GT, Zenon
<4>3. num'[j] > num[i]
BY <4>1, <4>2, Plus1, Transitivity2, Zenon
<4>4. GG(i,j)'
Expand Down
32 changes: 25 additions & 7 deletions examples/Bakery.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ p4: unread := P \ {self} ;
or { flag[self] := FALSE } ;
p5: while (unread # {}) {
with (i \in unread) { nxt := i ; };
await ~ flag[nxt];
await (flag[nxt] = FALSE);
p6: await \/ num[nxt] = 0
\/ LL(self, nxt) ;
unread := unread \ {nxt};
Expand All @@ -127,7 +127,7 @@ p7: with (repeat \in BOOLEAN, k \in Nat) {
**** this ends the comment containg the pluscal code **********)

\* BEGIN TRANSLATION (this begins the translation of the PlusCal code)
VARIABLES num, flag, pc
VARIABLES pc, num, flag

(* define statement *)
LL(j, i) == \/ num[j] < num[i]
Expand All @@ -136,7 +136,7 @@ LL(j, i) == \/ num[j] < num[i]

VARIABLES unread, max, nxt

vars == << num, flag, pc, unread, max, nxt >>
vars == << pc, num, flag, unread, max, nxt >>

ProcSet == (P)

Expand Down Expand Up @@ -194,7 +194,7 @@ p5(self) == /\ pc[self] = "p5"
/\ IF unread[self] # {}
THEN /\ \E i \in unread[self]:
nxt' = [nxt EXCEPT ![self] = i]
/\ ~ flag[nxt'[self]]
/\ (flag[nxt'[self]] = FALSE)
/\ pc' = [pc EXCEPT ![self] = "p6"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ nxt' = nxt
Expand Down Expand Up @@ -329,7 +329,11 @@ THEOREM Spec => []MutualExclusion
<2>3. ASSUME NEW self \in P,
p3(self)
PROVE Inv'
BY <2>3, Z3T(60) DEF p3, TypeOK, IInv, After, LL
<3>1. TypeOK'
BY <2>3 DEF p3, TypeOK
<3>2. ASSUME NEW i \in P PROVE IInv(i)'
BY <2>3, SMTT(60) DEF p3, TypeOK, IInv, After, LL
<3>. QED BY <3>1, <3>2
<2>4. ASSUME NEW self \in P,
p4(self)
PROVE Inv'
Expand All @@ -341,15 +345,29 @@ THEOREM Spec => []MutualExclusion
<2>5. ASSUME NEW self \in P,
p5(self)
PROVE Inv'
BY <2>5, Z3T(60) DEF p5, TypeOK, IInv, After, LL
<3>1. TypeOK'
<4>1. /\ num' \in [P -> Nat]
/\ flag' \in [P -> BOOLEAN]
/\ unread' \in [P -> SUBSET P]
/\ max' \in [P -> Nat]
/\ nxt' \in [P -> P]
/\ pc' \in [P -> {"p1", "p2", "p3", "p4", "p5", "p6", "cs", "p7"}]
BY <2>5 DEF p5, TypeOK
<4>2. /\ \A i \in P : pc'[i] \in {"p2", "p5", "p6"} => i \notin unread'[i]
/\ \A i \in P : (pc'[i] = "p6") => nxt'[i] # i
BY <2>5 DEF p5, TypeOK
<4>. QED BY <4>1, <4>2 DEF TypeOK
<3>2. ASSUME NEW i \in P PROVE IInv(i)'
BY <2>5, SMTT(20) DEF p5, TypeOK, IInv, After, LL
<3>. QED BY <3>1, <3>2
<2>6. ASSUME NEW self \in P,
p6(self)
PROVE Inv'
BY <2>6, Z3T(60) DEF p6, TypeOK, IInv, After, LL
<2>7. ASSUME NEW self \in P,
cs(self)
PROVE Inv'
BY <2>7 DEF cs, TypeOK, IInv, After, LL
BY <2>7, SMTT(20) DEF cs, TypeOK, IInv, After, LL
<2>8. ASSUME NEW self \in P,
p7(self)
PROVE Inv'
Expand Down
10 changes: 3 additions & 7 deletions examples/BubbleSort.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,8 +205,9 @@ THEOREM Spec => [](pc = "Done" => IsSorted(A) /\ IsPermOf(A, A0))
<2> SUFFICES ASSUME Inv, Lbl_1 \/ Lbl_2 \* Next
PROVE Inv'
<3>1. Inv /\ UNCHANGED vars => Inv'
BY DEF vars, TypeOK, RealInv, IsSorted, IsSortedTo,
IsSortedFromTo, IsPermOf, Perms, **
BY Zenon
DEF vars, TypeOK, RealInv, IsSorted, IsSortedTo,
IsSortedFromTo, IsPermOf, Perms, **
<3>2. QED
BY <3>1 DEF Next
<2>1. TypeOK'
Expand All @@ -228,9 +229,4 @@ THEOREM Spec => [](pc = "Done" => IsSorted(A) /\ IsPermOf(A, A0))
(***************************************************************************)
=============================================================================
\* Modification History
\* Last modified Wed Aug 28 14:03:35 CEST 2019 by merz
\* Last modified Mon Mar 17 11:17:49 CET 2014 by doligez
\* Last modified Fri Mar 07 15:24:43 CET 2014 by shaolin
\* Last modified Tue Nov 27 13:33:10 CET 2012 by doligez
\* Last modified Fri Nov 23 09:32:08 PST 2012 by lamport
\* Created Wed Nov 21 11:50:58 PST 2012 by lamport
Loading