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