Send doesn't change the priority or muted cowns

[lukecheeseman]

The current definition of Prioritizing is defined as:

Prioritizing(cs) ==
  LET unprioritized == {c \in cs: priority[c] < 1} IN
  unprioritized \union UNION {Blockers(c): c \in unprioritized}

We only check Prioritizing with a single element set which means we can rewrite this as:

Prioritizing(c) == IF priority[c] < 1 THEN {c} \union Blockers(c) ELSE {}

The guard and the assignments that appear in Send are:

IF priority[Min(receivers)] = 1 THEN
  LET prioritizing == Prioritizing(Min(receivers)) IN
  LET unmuting == LowPriority(prioritizing) IN

So prioritizing and unmuting will be empty.

This is interesting, I recall this used to work over all the receivers but then @Theodus changed it as this is not how the implementation works. I wonder if this unnecessary operation is present in the implementation.

Without these operations, Send now seems very strange to me:

Send(cown) ==
  LET senders == CurrentMessage(cown) IN
  /\ running[cown]
  /\ fuel > 0
  /\ \E receivers \in SUBSET Cowns:
    /\ Cardinality(receivers) > 0
    /\ queue' =
      (Min(receivers) :> Append(queue[Min(receivers)], receivers)) @@ queue
    /\ IF priority[Min(receivers)] = 1 THEN
      /\ LET mutors == {c \in receivers \ senders: ValidMutor(c)} IN
        IF mutors /= {} /\ mutor[cown] = Null
          /\ \A c \in senders: priority[c] = 0
          /\ \A c \in senders: c \notin receivers \* TODO: justify
        THEN
          /\ mutor' = (cown :> Min(mutors)) @@ mutor
        ELSE
          /\ UNCHANGED <<mutor>>
      ELSE
        /\ UNCHANGED <<scheduled, priority, mutor>>
  /\ fuel' = fuel - 1
  /\ UNCHANGED <<running, blocker, mute>>

Assigning a mutor (any receiver who is overloaded or muted) is dependent on whether the first receiver has a high priority?
And this is the only outcome of checking the first receiver is high?
I wonder if this is a latent bug in the spec?

[lukecheeseman]

Linking to issue #21 as this is another oddity of Send