The enforcement operator <A>phi is defined on page 63 and again on page 138. The definition is as follows:
⟨A⟩φ := A ∧ <>φ ∨ B ∧ []φ = (A=><>φ|[]φ)
It holds on the states where player A can enforce that the next transition will reach a state where φ holds: Each state is either controlled by player A or player B, and if a state is controlled by player A, then it is sufficient to have a successor state where φ holds, since player A can choose that one. If the state is controlled by player B, we have to demand that []φ holds so that player B can only choose φ-states.
For computing the attractor attrA(p) := µx.(p ∨ <A>x) we relabel the state transition system such that the states controlled by player A and B are labeled with variables "a" and "b", respectively, and state s7 (the one with highest rank) is labeled with variable p.
The computation of the attractor is then the computation of mu x. (p | a & <> x | b & [] x) which is done as follows:
〖p〗= {s7}
〖a〗= {s3;s4;s5;s6}
〖b〗= {s0;s1;s2;s7}
step 0 : x = {}
〖x〗= {}
〖<> x〗 = {}
〖a & <> x〗 = {}
〖p | a & <> x〗 = {s7}
〖x〗= {}
〖[] x〗 = {}
〖b & [] x〗 = {}
〖p | a & <> x | b & [] x〗 = {s7}
step 1 : x = {s7}
〖x〗= {s7}
〖<> x〗 = {s5;s6}
〖a & <> x〗 = {s5;s6}
〖p | a & <> x〗 = {s5;s6;s7}
〖x〗= {s7}
〖[] x〗 = {s5}
〖b & [] x〗 = {}
〖p | a & <> x | b & [] x〗 = {s5;s6;s7}
step 2 : x = {s5;s6;s7}
〖x〗= {s5;s6;s7}
〖<> x〗 = {s1;s2;s5;s6;s7}
〖a & <> x〗 = {s5;s6}
〖p | a & <> x〗 = {s5;s6;s7}
〖x〗= {s5;s6;s7}
〖[] x〗 = {s5}
〖b & [] x〗 = {}
〖p | a & <> x | b & [] x〗 = {s5;s6;s7}
〖x〗= {s5;s6;s7}
fixpoint reached!
〖mu x. (p | a & <> x | b & [] x)〗 = {s5;s6;s7}
The computation starts with p-states and adds the existential A-predecessors and the universal B-predecessors until a fixpoint is reached.
