Φinf is nu y. (<>y). It ensures the existence of an infinite path from here.
The template you gave contains Φinf ∧ ψ. It should be Φinf ∧ b = nu y. (<>y) ∧ b. But you moved b into the nu-operator. The correct formula should check whether the current state satisfies b, and whether there is an infinite path. Your formula checks EGb (an infinite path satisfying b on every step).
I think that's the reason why the results are different.
On the formatting of the outer bracket. Yes. You should clarify that the quantifier quantifies over the whole formula. Sometimes, the lecture notes leave out these outer brackets if they are obvious to human readers. In this case, variable x is only defined by the fixpoint. Thus, the formula up to variable x is assumed to be inside the mu-operator. However, this doesn't work for automated tools. They'd just assume that mu binds as strong as always. Thus, x would be outside the mu operator. It would be assumed to be empty.
Your can use our tools to check how nu x. b & <>x; and nu x. <>x & b; and nu x. (<>x & b) are handled differently.
