`HighPriorityInUnbockedQueue` -- what does the name express?
sophiaIC opened this issue · 1 comments
sophiaIC commented
Why is HighPriorityInUnbockedQueue called so? Does it hold that a cown with ptiotity 1 is “unblocked”? And what does “unblocked” mean? Does it mean that it is not in a MutedBy relation?
Theodus commented
I've replaced this invariant with two that actually use the Blockers of a cown:
\* 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)
\* All blockers of a high-priority cown are high-priority.
HighPriorityBlockersAreHighPriority ==
\A c \in HighPriority(Cowns): \A k \in Blockers(c): priority[k] = 1