Q16: cycles in the mute-sets

[sophiaIC]

I think that we should have a further invariant:
c \notin MutTrans(c)
where
MitTrans(c) = { c } \cup { c' | \exists c''\in MutTrans(c). c'\in mut[c''] }

[sophiaIC]

Otherwise, we would allow the following configuration:

        queue[c1] = {​​​​​​​​c1}​​​   sch[c1]=false   prio[c1]=-1    mute[c1]={​​​​​​​​c2}​​​​​​​​    
        queue[c2] = {​​​​​​​​​c2}​​​​​​​​   sch[c2]=false   prio[c2]=-1   mute[c2]={​​​​​​​​​c1}​​​​​​​​​   
​        queue[c3] = {​​​​​​​​ }​​​​​​​    sch[c3]=true    prio[c3]=0    mute[c3]={​​​​​​​​ }​​​​​​ 

[Theodus]

I've added an invariant that the transitive closure of MutedBy is acyclic in 97c2f57:

CylcicTransitiveClosure(R(_, _)) ==
  LET s == {<<a, b>> \in Cowns \X Cowns: R(a, b)}
  IN \E c \in Cowns: <<c, c>> \in TC(s)

MutedBy(a, b) == (a \in mute[b]) /\ (priority[a] = -1)
AcyclicTCMute == ~CylcicTransitiveClosure(MutedBy)