[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Bikeshedding fun with problem 7.7



That is very clear. Thanks again!

On Tuesday, February 25, 2014 1:46:37 PM UTC-8, Leslie Lamport wrote:
Hi Brian,
 
   My "Model Overview" has "ISpec" typed in to the "Temporal formula"
   box under "What is the behavior
spec?"
 
The "behavior spec" is the Spec that TLC is checking.  TLC requires
the spec to have the form

   Init /\ [][Next]_v /\ Liveness

If Liveness = TRUE, you can also enter this spec by selecting "Initial
predicate and next-state relation" and entering the Init and Next fields.
If Liveness # TRUE, you have to enter it in "Temporal formula".  For your
original spec ISpec, the formulas Init, Next, and Liveness were:

   Init: /\ Init
         /\ TypeOK
         /\ MutualExclusion
         /\ Coordination
   Next:  Next

   Liveness: /\ Fairness
             /\ DeadlockFreedom
 
The "What to check" section tells TLC to check that the "Behavior spec"
satisfies certain properties.  Telling it to check that Inv is an invariant
is equivalent to telling it to check the (temporal) "Property" []Inv.
When you wrote the "Behavior spec" Init /\ [][Next]_<<pc, x>>  and specified
the temporal property Fairness, you were telling TLC to check that (every
behavior of) the spec Init /\ [][Next]_<<pc, x>>  satisfies the property
Fairness.  It doesn't, because the behavior that takes nothing but stuttering
steps satisfies the spec but not Fairness.
 
Please let me know what I can do to make sure that others aren't confused
in the same way you were.
 
Thanks,
 
Leslie