A stronger blocker invariant?

[lukecheeseman]

We have

\* A cown is acquired by one of its blockers.
Blocker == \A c \in Cowns: blocker[c] \in Cowns => \E k \in Blockers(c): AcquiredBy(c, k)

RECURSIVE Blockers(_)
Blockers(c) == IF blocker[c] = Null THEN {} ELSE {blocker[c]} \union Blockers(blocker[c])

AcquiredBy(a, b) == (a < b) /\ (a \in UNION Range(queue[b]))

However I think we can have a stronger invariant:

BlockerIsNextRequiredToRun ==
  \A c1, c2 \in Cowns: blocker[c1] = c2 <=>
    \E c3 \in Cowns: c1 < c3 /\ \E m \in Range(queue[c3]): c1 \in m   \* c1 is acquired by c3
      /\ ~(running[c3] /\ m = Head(queue[c3])) /\ c2 = Min({c4 \in m: c4 > c1})

This says a cowns' (c1) has a blocker if it appears in the message (m) of some higher address cown (c3) (acquired by) and that cown (c3) is not running that message (m) and the blocker is the next cown (c2) after the cown (c1) in the message (m).

I think this invariant is strong and implies the first invariant

[sophiaIC]

I think that BlockerIsNextRequiredToRun does not imply Blocker.

If we wanted BlockerIsNextRequiredToRun to imply Blocker, then we would need to also add on the res that c3\in Blockers(c1).