[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Model Checking the Bakery Algorithm
Hi everyone,
I have taken the TLA+ spec of the bakery algorithm from [1] and I am trying to run the model checker on it, with no success. I have deleted the comment containing the PlusCal code along with those parts related to the proof system. The spec is currently in attachment file. This is the exception that TLC throws when I run it with N = 4 or 3:
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: TLC encountered a non-enumerable quantifier bound
Nat.
line 65, col 31 to line 65, col 33 of module Bakery
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 64, column 13 to line 71, column 56 in Bakery
1. Line 64, column 16 to line 64, column 30 in Bakery
2. Line 65, column 16 to line 70, column 53 in Bakery
3. Line 65, column 19 to line 67, column 53 in Bakery
4. Line 65, column 22 to line 66, column 54 in Bakery
Why is this happening? I have indicated Spec as the temporal formula in Model Overview page.
Amirhossein
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0sdLdP1ocXp40hsscNt-KDLYwN8419YgZ9KBWphrhy3Cw%40mail.gmail.com.
------------ MODULE Bakery ----------------------------
EXTENDS Naturals
(***************************************************************************)
(* We first declare N to be the number of processes, and we assume that N *)
(* is a natural number. *)
(***************************************************************************)
CONSTANT N
ASSUME N \in Nat
(***************************************************************************)
(* We define Procs to be the set {1, 2, ... , N} of processes. *)
(***************************************************************************)
Procs == 1..N
(***************************************************************************)
(* \prec is defined to be the lexicographical less-than relation on pairs *)
(* of numbers. *)
(***************************************************************************)
a \prec b == \/ a[1] < b[1]
\/ (a[1] = b[1]) /\ (a[2] < b[2])
VARIABLES num, flag, pc, unchecked, max, nxt
vars == << num, flag, pc, unchecked, max, nxt >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ num = [i \in Procs |-> 0]
/\ flag = [i \in Procs |-> FALSE]
(* Process p *)
/\ unchecked = [self \in Procs |-> {}]
/\ max = [self \in Procs |-> 0]
/\ nxt = [self \in Procs |-> 1]
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ pc' = [pc EXCEPT ![self] = "e1"]
/\ UNCHANGED << num, flag, unchecked, max, nxt >>
e1(self) == /\ pc[self] = "e1"
/\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]]
/\ pc' = [pc EXCEPT ![self] = "e1"]
/\ UNCHANGED <<unchecked, max>>
\/ /\ flag' = [flag EXCEPT ![self] = TRUE]
/\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}]
/\ max' = [max EXCEPT ![self] = 0]
/\ pc' = [pc EXCEPT ![self] = "e2"]
/\ UNCHANGED << num, nxt >>
e2(self) == /\ pc[self] = "e2"
/\ IF unchecked[self] # {}
THEN /\ \E i \in unchecked[self]:
/\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}]
/\ IF num[i] > max[self]
THEN /\ max' = [max EXCEPT ![self] = num[i]]
ELSE /\ TRUE
/\ max' = max
/\ pc' = [pc EXCEPT ![self] = "e2"]
ELSE /\ pc' = [pc EXCEPT ![self] = "e3"]
/\ UNCHANGED << unchecked, max >>
/\ UNCHANGED << num, flag, nxt >>
e3(self) == /\ pc[self] = "e3"
/\ \/ /\ \E k \in Nat:
num' = [num EXCEPT ![self] = k]
/\ pc' = [pc EXCEPT ![self] = "e3"]
\/ /\ \E i \in {j \in Nat : j > max[self]}:
num' = [num EXCEPT ![self] = i]
/\ pc' = [pc EXCEPT ![self] = "e4"]
/\ UNCHANGED << flag, unchecked, max, nxt >>
e4(self) == /\ pc[self] = "e4"
/\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]]
/\ pc' = [pc EXCEPT ![self] = "e4"]
/\ UNCHANGED unchecked
\/ /\ flag' = [flag EXCEPT ![self] = FALSE]
/\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}]
/\ pc' = [pc EXCEPT ![self] = "w1"]
/\ UNCHANGED << num, max, nxt >>
w1(self) == /\ pc[self] = "w1"
/\ IF unchecked[self] # {}
THEN /\ \E i \in unchecked[self]:
nxt' = [nxt EXCEPT ![self] = i]
/\ ~ flag[nxt'[self]]
/\ pc' = [pc EXCEPT ![self] = "w2"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ nxt' = nxt
/\ UNCHANGED << num, flag, unchecked, max >>
w2(self) == /\ pc[self] = "w2"
/\ \/ num[nxt[self]] = 0
\/ <<num[self], self>> \prec <<num[nxt[self]], nxt[self]>>
/\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}]
/\ pc' = [pc EXCEPT ![self] = "w1"]
/\ UNCHANGED << num, flag, max, nxt >>
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ UNCHANGED << num, flag, unchecked, max, nxt >>
exit(self) == /\ pc[self] = "exit"
/\ \/ /\ \E k \in Nat:
num' = [num EXCEPT ![self] = k]
/\ pc' = [pc EXCEPT ![self] = "exit"]
\/ /\ num' = [num EXCEPT ![self] = 0]
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ UNCHANGED << flag, unchecked, max, nxt >>
p(self) == ncs(self) \/ e1(self) \/ e2(self) \/ e3(self) \/ e4(self)
\/ w1(self) \/ w2(self) \/ cs(self) \/ exit(self)
Next == (\E self \in Procs: p(self))
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ p(self))
\* END TRANSLATION (this ends the translation of the PlusCal code)
(***************************************************************************)
(* MutualExclusion asserts that two distinct processes are in their *)
(* critical sections. *)
(***************************************************************************)
MutualExclusion == \A i,j \in Procs : (i # j) => ~ /\ pc[i] = "cs"
/\ pc[j] = "cs"
-----------------------------------------------------------------------------
(***************************************************************************)
(* The Inductive Invariant *)
(* *)
(* TypeOK is the type-correctness invariant. *)
(***************************************************************************)
TypeOK == /\ num \in [Procs -> Nat]
/\ flag \in [Procs -> BOOLEAN]
/\ unchecked \in [Procs -> SUBSET Procs]
/\ max \in [Procs -> Nat]
/\ nxt \in [Procs -> Procs]
/\ pc \in [Procs -> {"ncs", "e1", "e2", "e3",
"e4", "w1", "w2", "cs", "exit"}]
(***************************************************************************)
(* Before(i, j) is a condition that implies that num[i] > 0 and, if j is *)
(* trying to enter its critical section and i does not change num[i], then *)
(* j either has or will choose a value of num[j] for which *)
(* *)
(* <<num[i],i>> \prec <<num[j],j>> *)
(* *)
(* is true. *)
(***************************************************************************)
Before(i,j) == /\ num[i] > 0
/\ \/ pc[j] \in {"ncs", "e1", "exit"}
\/ /\ pc[j] = "e2"
/\ \/ i \in unchecked[j]
\/ max[j] >= num[i]
\/ /\ pc[j] = "e3"
/\ max[j] >= num[i]
\/ /\ pc[j] \in {"e4", "w1", "w2"}
/\ <<num[i],i>> \prec <<num[j],j>>
/\ (pc[j] \in {"w1", "w2"}) => (i \in unchecked[j])
(***************************************************************************)
(* Inv is the complete inductive invariant. *)
(***************************************************************************)
Inv == /\ TypeOK
/\ \A i \in Procs :
\* /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0)
/\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0)
/\ (pc[i] \in {"e2", "e3"}) => flag[i]
/\ (pc[i] = "w2") => (nxt[i] # i)
/\ pc[i] \in {(*"e2",*) "w1", "w2"} => i \notin unchecked[i]
/\ (pc[i] \in {"w1", "w2"}) =>
\A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j)
/\ /\ (pc[i] = "w2")
/\ \/ (pc[nxt[i]] = "e2") /\ (i \notin unchecked[nxt[i]])
\/ pc[nxt[i]] = "e3"
=> max[nxt[i]] >= num[i]
/\ (pc[i] = "cs") => \A j \in Procs \ {i} : Before(i, j)
-----------------------------------------------------------------------------
=============================================================================
\* Modification History
\* Last modified Mon Mar 02 19:53:36 IRST 2020 by AmirHossein
\* Last modified Tue Aug 27 12:23:10 PDT 2019 by loki
\* Last modified Fri May 25 11:18:47 CEST 2018 by merz
\* Last modified Sat May 19 16:40:23 CEST 2018 by merz
\* Last modified Thu May 17 07:02:45 PDT 2018 by lamport
\* Created Thu Nov 21 15:54:32 PST 2013 by lamport