I don't understand what you are doing in this or your previous post.
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).
ISpec == Inv /\ [Next]_<<x, pc>>
whose form suggests that you are taking Inv to be the initial predicate.
But your definition
Inv == /\ Init
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)
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