Zielonka's algorithm

See Partial solving for how the same computation below is run during exploration — before the graph is fully known — to decide vertices on the fly, rather than only after the recursion here has a complete graph to work with.

Priority direction: max-parity vs min-parity

merc's Priority is a max-parity encoding: the outermost fixpoint block gets the largest priority, Player::from_priority(p) == Even iff p is even, and the explicit solve_zielonka picks the highest priority present. mCRL2's symbolic solver is min-parity: the outermost block gets rank 0, and get_min_rank picks the smallest, with alpha = m % 2.

The recursive algorithm

For a parity game , Zielonka's algorithm peels off, in each recursive call, the attractor of the highest priority present, recurses on what remains, and then decides — depending on whether the opponent won anything at all in the remainder — whether one more attractor and one more recursive call are needed to correctly attribute that remainder:

The two marked lines are the only places the recursion ever asks "who controls reaching this set" — everywhere else it only removes vertices and recurses. That is also why on-the-fly partial solving (next page) needs to touch nothing but those two computations: substituting the safe attractor for there is enough to keep the whole recursion sound against a graph that is still being explored.

Strategy representation

A strategy is an LDD over the doubled, interleaved state vector [from₀, to₀, from₁, to₁, …] — the same layout the edge relations use. apply_strategy projects the strategy onto 2*read_idx/2*write_idx+1 and intersects it with each group's relation, which is why the layout is not free to choose: any other layout would need a translation step in the innermost loop of the only consumer. merge builds this interleaved cartesian product.