I appreciate your for taking the time to read so carefully; this is very
helpful to me. Responses inline below.
On Monday, February 24, 2014 1:36:45 PM UTC-8, Leslie Lamport wrote:
Hi Brian,
I don't understand what you are doing in this or your previous post.
I am trying to make a version of the spec that is more subjectively
understandable to me but equivalent to the one in the hyperbook. This is
admittedly a subjective, stylistic activity.
You write
This passes checks with ISpec as temporal invariant
I don't know what you mean by a temporal invariant.
I should have said "Temporal formula." My "Model Overview" has "ISpec"
typed in to the "Temporal formula" box under "What is the behavior
spec?"
I presume that
"passes checks" means that you have successfully checked something
with the model checker, but I don't know what. In other words, I
don't know what model you have checked. To describe the model, you
need to say what you entered in the various Toolbox fields that
specify the model--that is, "What is the behavior spec?", "What to
check?", and any other things that you told the model checker to use
(I don't think there should be any).
Under "What to check?" I chose "Deadlock," not the same as my
user-defined "DeadlockFreedom."
If I had an "Initial predicate and next-state relation" chosen under
"what is the behavior spec?" then I think "Deadlock" under "What to
check?" means that the next-state relation is satisfied by every step in
every behavior. However, I have "Temporal formula" chosen instead of
"Initial predicate and next-state relation," so I don't know what
"Deadlock" under "What to check?" does under this circumstance.
You define
ISpec == Inv /\ [][Next]_<<x, pc>>
whose form suggests that you are taking Inv to be the initial predicate.
But your definition
Inv == /\ Init
/\ TypeOK
/\ MutualExclusion
/\ Fairness
/\ Coordination
/\ DeadlockFreedom
is rather bizarre. First of all, I presume that Init is defined by
the PlusCal translation. In that case, I believe that Init implies
TypeOK /\ MutualExclusion /\ Coordination. (You should make sure you
understand why it does--or find a counterexample if it doesn't.)
Therefore, Inv is equivalent to (since P => Q is equivalent to P /\ Q = P)
/\ Init
/\ Fairness
/\ DeadlockFreedom
The "Init" generated by the PlusCal translation is the following:
ProcSet == ({0,1})
Init == (* Global variables *)
/\ x = [i \in {0,1} |-> FALSE]
/\ pc = [self \in ProcSet |-> "ncs"]
which does imply TypeOK, MutualExclusion, and Coordination (I checked).
which is the conjunction of a state predicate and two temporal
formulas. Moreover, if the algorithm is deadlock free (I haven't
looked closely to see if it is), then the formula
S == Init /\ [][Next]_<<x, pc>> /\ Fairness
should imply DeadlockFreedom, so ISpec should be equivalent to S.
Abandoning Inv, I changed ISpec to equal Init /\ [][Next]_<<x, pc>> /\
Fairness and checked it in the model checker by choosing "Temporal
Formula" under "What is the behavior spec?" and typing in "ISpec." This
passes. With this chosen, I cannot choose "Initial predicate and
next-state relation."
Here is the MC.tla file
---- MODULE MC ----
EXTENDS OneBitTwoProcesses, TLC
\* SPECIFICATION definition @modelBehaviorSpec:0
spec_139335347329970000 ==
ISpec
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_139335347330971000 ==
A!ISpec
----
=============================================================================
\* Modification History
\* Created Tue Feb 25 10:37:53 PST 2014 by bbeckman
I then tried an experiment that heightens my confusion. I would have
expected that the above is equivalent to putting "Init" and "Next" into
the Init and Next slots of "Initial predicate and next-state relation"
of "What is the behavior spec?" and ALSO putting "Fairness" in the
properties box of "What to check?" However, doing so generates an error,
namely that
<Initial predicate> State (num = 1)
x (0 :> FALSE @@ 1 :> FALSE)
pc (0 :> "ncs" @@ 1 :> "ncs")
<Stuttering> State (num = 2)
Fairness asserts that \A i \in {0,1} : WF_vars(Proc(i)), where
Proc(i) == ncs(i) \/ e1(i) \/ e2(i) \/ cs(i) \/ e3(i) \/ e4(i) \/ f(i).
I think WF_vars(P) means that there is no suffix of any behavior in
which P is enabled for every step but there is no P step. For Proc(i) to
be enabled means that there exists a possible assignment of values to
variables that makes Proc(i) true. But I don't see how a stuttering
state can be reached since "ncs(i)" will push pc to e1:
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "e1"]
/\ x' = x
At the bottom of this post is my entire spec as it stands now.
Here is the failing MC.tla file
---- MODULE MC ----
EXTENDS OneBitTwoProcesses, TLC
\* INIT definition @modelBehaviorInit:0
init_139335367677776000 ==
Init
----
\* NEXT definition @modelBehaviorNext:0
next_139335367678777000 ==
Next
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_139335367679878000 ==
A!ISpec
----
\* PROPERTY definition @modelCorrectnessProperties:1
prop_139335367680979000 ==
Fairness
----
=============================================================================
\* Modification History
\* Created Tue Feb 25 10:41:16 PST 2014 by bbeckman
I believe you are confused, but I don't know what the source of your
confusion is. I suspect that you are writing formulas that don't mean
what you want them to mean. You should make sure that you understand
the meaning of each formula you write---that is, what it asserts about
a behavior. You would then see that Init, TypeOK, MutualExclusion,
and Coordination make assertions about the first state of the
behavior, while Fairness and DeadlockFreedom make assertions about the
entire behavior.
Leslie
I am definitely confused between assertions about the first state of a
behavior versus assertions about the entire behavior. Suppose, under
"What is the behavior spec?" I choose a "Temporal formula" instead of
"Initial predicate and next-state relation." Section 6.7.2 of the
hyperbook states that a formula without temporal operators is a temporal
formula true of an entire behavior if it's true of its first state. I
gather this means that, when looking at a temporal formula that is a
conjunction, TLC picks out the conjuncts that are formulas with no
primes and no temporal operators (the state predicates), and only
ensures them on the first state of any behavior.
Here is my entire spec, including translation, as it stands now.
------------------------- MODULE OneBitTwoProcesses -------------------------
EXTENDS Integers
(******************************************************************
--algorithm OneBit
{ variable x = [i \in {0,1} |-> FALSE] ;
fair process (Proc \in {0,1})
{ ncs: while (TRUE)
\* This is the model for my non-critical processing.
{ skip ;
\* Ok, I'm done with that and I want in to the
\* critical section!
e1: x[self] := TRUE ;
e2: if (~x[1-self])
\* If the other guy isn't in, I'm in!
{ cs: skip (* Model for my critical code! *) }
else
\* Oops, the other guy is in. What do I do?
{ if (self = 0)
\* If I'm process 0, I'll keep trying.
{ goto e2 }
\* But, if I'm process 1, I'll be the nice guy;
\* I'll stop trying and spin while process 0 is in.
else
{ e3: x[1] := FALSE ;
e4: while ( x[0] )
{ skip (* spin *) } ;
goto e1
} } ;
\* Ok, I'm done. I don't need the critical section now.
f: x[self] := FALSE
}
} }
******************************************************************)
\* BEGIN TRANSLATION
VARIABLES x, pc
vars == << x, pc >>
ProcSet == ({0,1})
Init == (* Global variables *)
/\ x = [i \in {0,1} |-> FALSE]
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "e1"]
/\ x' = x
e1(self) == /\ pc[self] = "e1"
/\ x' = [x EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "e2"]
e2(self) == /\ pc[self] = "e2"
/\ IF ~x[1-self]
THEN /\ pc' = [pc EXCEPT ![self] = "cs"]
ELSE /\ IF self = 0
THEN /\ pc' = [pc EXCEPT ![self] = "e2"]
ELSE /\ pc' = [pc EXCEPT ![self] = "e3"]
/\ x' = x
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "f"]
/\ x' = x
e3(self) == /\ pc[self] = "e3"
/\ x' = [x EXCEPT ![1] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "e4"]
e4(self) == /\ pc[self] = "e4"
/\ IF x[0]
THEN /\ TRUE
/\ pc' = [pc EXCEPT ![self] = "e4"]
ELSE /\ pc' = [pc EXCEPT ![self] = "e1"]
/\ x' = x
f(self) == /\ pc[self] = "f"
/\ x' = [x EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "ncs"]
Proc(self) == ncs(self) \/ e1(self) \/ e2(self) \/ cs(self) \/ e3(self)
\/ e4(self) \/ f(self)
Next == (\E self \in {0,1}: Proc(self))
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in {0,1} : WF_vars(Proc(self))
\* END TRANSLATION
PC0Labels == {"ncs", "f", "e1", "e2", "cs"}
ExtraLabels == {"e3", "e4"}
PC1Labels == PC0Labels \cup ExtraLabels
TypeOK == /\ pc \in [{0} -> PC0Labels] \cup [{1} -> PC1Labels]
/\ x \in [{0, 1} -> BOOLEAN]
InCS(i) == pc[i] = "cs"
MutualExclusion == ~(InCS(0) /\ InCS(1))
Fairness == \A i \in {0,1} : WF_vars(Proc(i))
Coordination == \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]
Trying(i) == pc[i] \in {"e1", "e2"}
DeadlockFreedom == (Trying(0) \/ Trying(1)) ~> (InCS(0) \/ InCS(1))
ISpec == Init /\ [][Next]_<<x, pc>> /\ Fairness
A == INSTANCE OneBitProtocol
WITH pc <- [i \in {0, 1} |->
IF pc[i] \in {"ncs", "f", "e3", "e4"} THEN "r" ELSE pc[i]]
=============================================================================
\* Modification History
\* Last modified Tue Feb 25 08:39:44 PST 2014 by bbeckman
\* Created Thu Feb 20 13:10:58 PST 2014 by bbeckman