Hi Brian,
I don't understand what you are doing in this or your previous post.
You write
This passes checks with ISpec as temporal invariant
I don't know what you mean by a temporal invariant. 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).
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
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.
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