# Global Model Checking explain box(x) and implication output

there must be error in box (x) output? Also explain how implication is computed here.

Where exactly do you see an error here?

And the implication is done like one would except, so if you have two state sets A and B and you want to compute States(A -> B) then the result is:

B U (S \ A)   with S being the complete state set S := {s0, ..., s7}

So state si is part of States(A -> B) if either si is part of set B or si is not part of set A. Or you can put it like that:

If a state si is part of set A then it must be also part of set B. If this condition holds true, then si is also element of States(A -> B) otherwise it isn't.

by (3.4k points)
Thanks for the response.

How could universal predecessors of x be all states in step 0?
This is because you calculate the greatest fixpoint via a "nu" operator instead of a "mu" operator (which calculates the least fixpoint). Thus you need to start with the whole state set.
I think you mis-understood my question. I know that x will be initialised with all the states due to nu operator.

My question is how States([]x) = {s0;...;s7}?

How universal predecessor of x could be all the states, Please elaborate that part.
The reason for that is simply that x contains all states, thus all transitions do of course point to some state in {s0,...,s7} i.e. there is no state that has a transition that does not point into that set (as there are no other states outside this set). Also see page 56 in chapter 4 in that regard: pre_{universal}(S) = S