Games and solvers¶

The progress check ("can the workflow keep going?") is computed once, when a module is built, by turning the policy's state machine into a small game and solving it with two standard algorithms. This page is for contributors who will change that code. It says first, in plain words, what the check proves and what it does not; then it shows how compile_game builds the game, why only final states get a self-loop, how Zielonka's parity algorithm and Karp's mean-cycle algorithm work on it with small worked examples, and what happens when the solvers hit a size limit.

The theory, with the published statements and their status, is on Workflows that keep going. Reader-facing guidance is on Can the workflow keep going?. Words like priority and final state are in the glossary.

What the check proves, and what it does not¶

Each state of a chart carries three things the policy author can set:

a priority, a whole number. Even means "fine to keep coming back here forever"; odd means "must not end up circling here forever". The default for a hand-built chart is 0. Text policies get 2 on states that propose an action and on final states, and 1 elsewhere (dfa_to_statechart, see Grammar compile).
a payoff, a reward (or cost, if negative) collected on arriving at the state. The default is 0.
an owner: the service (the default) or the environment (environment=True), meaning someone else picks the next event there.

The check passes when, starting from the initial state, the service has a strategy (choosing the next event in its own states, against any choice of the environment in its states) that makes the highest priority seen infinitely often even (the parity part, parity_win), and the best long-run average payoff over a reachable cycle is at least 0 (the mean-payoff part, nonnegative_mean).

Verified with Statechart directly (compile_game, then even_wins and nonnegative_mean):

Chart	`parity_win`	`nonnegative_mean`	Check
`a` (priority 0) `--e-->` `p` (priority 1, action `page`, no way out)	False	True	fail: every run ends in `p`, which is odd
`a` (priority 1) `--e-->` `b` (priority 0)	True	True	pass: every run ends in `b`
`a` (priority 1) `<--e-->` `b` (priority 1)	False	True	fail: the only cycle is odd
`a` (payoff −1) `--e-->` `b` (payoff −1)	True	False	fail: the only cycle costs
`a --e--> p` (priority 1, loops on `e`) `--fix-->` `done` (priority 0)	True	True	pass: the service can send `fix`
the same, with `p` marked `environment=True`	False	True	fail: the environment can send `e` forever

So the check catches a workflow that can loop forever in states marked odd, and, for text policies, a policy that can loop without proposing anything. What it assumes:

The service sends the right events in its own states. The fifth row passes because fix exists; nothing makes the service send it. Mark states the service does not control as environment=True.
The payoff part is one-player. Karp maximises over all routes, ignoring owners, so nonnegative_mean is a best case.
Priorities on hand-built charts are the author's. A chart left at priority 0 everywhere passes the parity part whatever its shape.

The record reports trust="lean" when the check passes, which refers to the solver's correctness, not to any guarantee about your workflow.

The game graph¶

compile_game(chart, limits) in statechart/game.py returns a frozen GameGraph:

Field	Meaning
`names`	state names in `chart.states()` order
`start`	index of `chart.initial`
`edges[v]`	tuples `(successor, event, weight)`
`priority`	`chart.priority_of(name)` for each state
`owner`	`1` (environment) for states with `environment=True`, else `0` (controller)

The weight of an edge for a chart transition t is t.payoff + chart.payoff_of(t.target): the transition's own payoff plus the payoff of the state it arrives in. Text policies set both to 0, so Karp sees an all-zero graph unless you build the chart by hand.

If the chart has more states than Limits.max_game_vertices (200), compile_game raises GameTooLarge; see When the solvers refuse.

Final states loop on themselves¶

After copying the chart's transitions, compile_game adds one edge to every state that has no outgoing transition (a final state):

(self, "_final", chart.payoff_of(name))

Parity and mean-payoff games are about infinite plays, so every vertex needs a successor. A final state is where the workflow ends; looping there at the state's own priority and payoff says "the run stays finished". No other state gets a self-loop, so the controller cannot "stay put" in a state just to win: it has to move along the arrows the policy draws. That matches decide, where an event a state does not handle leaves the entity where it is but is not progress either.

Example: `two_path_module`¶

The shape most examples use (examples/common.py):

intake --routine-->    auto   (action, payoff 1.0)  --hold--> hold (abstain)
intake --escalation--> review (action, payoff 0.5)  --hold--> hold

All four states have priority 0, and hold is final, so it gets the only self-loop:

intake: (auto, "routine", 1.0), (review, "escalation", 0.5)
auto:   (hold, "hold", 0.0)
review: (hold, "hold", 0.0)
hold:   (hold, "_final", 0.0)

The controller wins parity everywhere (every priority is even), and the only cycle is the hold loop, with mean 0.0. Both parts pass.

incident_response gives paging priority 2 (even) and payoff −0.2. Its cycles are mitigating ↔ paging (mean 0.4) and mitigating ↔ resolved (mean 1.5); the best is 1.5, so the mean-payoff part passes, and every priority is even, so the parity part passes.

Zielonka's algorithm¶

even_wins(game, limits) in statechart/parity.py returns, for each vertex, whether the controller (player 0, "Even") wins from it. controller_wins_from_start is even_wins(...)[game.start], cached on the module as _game_ok.

A run is won by Even if the highest priority it visits infinitely often is even. Each vertex is owned by one player, who picks the next edge there. The implementation is the standard recursive algorithm and supports both owners; tests/test_games.py checks it against brute force on random one- and two-player games. compile_game produces environment-owned vertices for states marked environment=True.

The attractor¶

attractor(universe, target, player=..., ...) returns the vertices from which player can force a visit to target:

attracted = target ∩ universe
repeat until nothing changes:
    for each vertex v in universe − attracted:
        moves = successors of v inside universe
        if owner[v] == player: join if ANY move is in attracted
        else:                  join if EVERY move is in attracted

The owner chooses, so one good move is enough for the owner, while the opponent can only be forced if all its moves lead in. (An opponent with no move left inside the universe is stuck and joins.)

The recursion¶

_solve(vertices) returns the two winning regions (controller, environment) of the subgame on vertices:

If vertices is empty, both regions are empty.
Let d be the highest priority in vertices and top the vertices with that priority. The favoured player is Even if d is even, Odd otherwise.
A = the favoured player's attractor of top. Solve the rest, vertices − A, recursively.
If the other player wins nothing in the rest, the favoured player wins all of vertices: it can keep returning to top.
Otherwise, B = the other player's attractor of its winning region in the rest. Solve vertices − B recursively. The favoured player wins its region there; the other player wins its region there plus all of B.

Each recursive call is on a trap (a set neither player can be forced out of), so the subgame is well defined. Recursion depth is capped by Limits.max_parity_depth (64); exceeding it raises ParityUnsolved.

Worked examples¶

All even. Two vertices, priorities 0 and 0, a → b, b final (self-loop). d = 0, favoured is Even, A is everything, the rest is empty, Odd wins nothing, so Even wins both vertices.

Odd trap. a (priority 0, Even-owned) has one edge to p (priority 1); p is final, so compile_game gives it a self-loop. d = 1, favoured is Odd. Odd's attractor of {p} includes a, because every move from a leads to p. The rest is empty, so Odd wins everything: Even loses from a, and the check fails. This is the first row of the table above.

A way out the service controls. a (priority 0) → p; p (priority 1) loops on e and has fix → done; done (priority 0) is final. All three are Even-owned. d = 1, favoured is Odd. Odd's attractor of {p} is {a, p} (a's only move leads to p). Solving the rest, {done}, Even wins it, so the other player (Even) wins something. B = Even's attractor of {done} in the whole game: p joins (Even owns it and one move, fix, leads in), then a joins. B is everything, vertices − B is empty, and Even wins all three. The check passes.

The same, environment-owned. Mark p environment=True, so Odd owns it. Even's attractor of {done} is now just {done}: Odd can keep choosing e at p. Solving vertices − B = {a, p}: d = 1, Odd's attractor of {p} is {a, p}, the rest is empty, so Odd wins a and p. The check fails from a. These are the last two rows of the table above.

Karp's algorithm¶

statechart/mean_payoff.py computes the best average weight per step over cycles reachable from the start, by Karp's algorithm. nonnegative_mean(game) is max_mean_payoff(game) >= -1e-12, cached as _mean_ok. Karp ignores owners: it is exact for one-player graphs, and for charts with environment-owned states it answers the best case. Above Limits.max_karp_vertices (200) it raises GameTooLarge.

Recurrence¶

Let \(n\) be the number of vertices and \(s\) the start. \(\mathrm{dp}[k][v]\) is the best weight of a walk of exactly \(k\) edges from \(s\) to \(v\):

\[ \mathrm{dp}[k][v] = \begin{cases} 0 & k=0,\; v=s \\ -\infty & k=0,\; v\neq s \quad (\text{for maximising}) \\ \max_u\bigl(\mathrm{dp}[k-1][u] + w(u,v)\bigr) & k\ge 1 \end{cases} \]

The best cycle mean is then

\[ \lambda = \max_v \min_{0 \le k < n} \frac{\mathrm{dp}[n][v] - \mathrm{dp}[k][v]}{n-k} \]

where entries that are \(-\infty\) are skipped. min_mean_payoff runs the same computation on the chart with every weight negated and returns minus the result, so there is only one implementation of the recurrence; both are checked against brute-force cycle enumeration on random graphs in tests/test_games.py. If nothing finite remains, the function returns 0.0, which passes nonnegative_mean; it does not happen in compiled charts, because every vertex has a successor.

The inner minimum is essential: for each end vertex it picks the weakest cycle consistent with the walk, and the outer maximum then picks the best vertex. Dropping the inner minimum gives a wrong answer.

Worked table¶

A hand-built chart with two states, start a, state payoffs 0, and transitions a --go (payoff 2)--> b, b --back (payoff 4)--> a. Both states have a way out, so compile_game adds no self-loop.

vertices 0=a, 1=b; n=2; start=0
edges:
  0: (1, "go", 2.0)
  1: (0, "back", 4.0)

\(k\)	\(\mathrm{dp}[k][a]\)	\(\mathrm{dp}[k][b]\)
0	0	−∞
1	−∞	2 (go)
2	6 (go, back)	−∞

For a: \(k=0\) gives \((6-0)/2 = 3\); \(k=1\) is skipped (−∞); the minimum is 3. For b: \(\mathrm{dp}[2][b]\) is −∞, so b is skipped. The maximum over vertices is 3: the cycle a → b → a with weights 2 and 4. Running it:

from grounded_decision import Statechart
from grounded_decision.statechart import compile_game, max_mean_payoff, min_mean_payoff

chart = (
    Statechart("k")
    .state("a", initial=True)
    .state("b")
    .on("a", "go", "b", payoff=2.0)
    .on("b", "back", "a", payoff=4.0)
)
game = compile_game(chart)
print(max_mean_payoff(game))  # 3.0
print(min_mean_payoff(game))  # 3.0 (the only cycle, so maximum and minimum agree)

Truffet's step is absent¶

A two-player tropical-elimination step for mean-payoff games (after Truffet) is not in the code: not imported, not behind a flag. The math catalog (result 104) records a finite counterexample to it. REF_TRUFFET_BAN is attached to the policy-shape and progress check reports so an auditor can see the absence. If two-player mean payoff is ever needed, it needs a different, sound solver.

When the solvers refuse¶

Module._solve_game runs:

try:
    game = compile_game(chart, limits)
    _game_ok   = controller_wins_from_start(game, limits)
    _mean_ok   = nonnegative_mean(game, limits)
    _game_note = "parity_win=... nonnegative_mean=..."
except (GameTooLarge, ParityUnsolved) as exc:
    _game_ok = _mean_ok = False
    _game_note = str(exc)

GameTooLarge means more states than max_game_vertices, or more than max_karp_vertices for the mean-payoff solver. ParityUnsolved means the recursion went deeper than max_parity_depth, or even_wins itself saw too many vertices.

The module is still built, and every later decide:

still steps the chart and returns the new state in extras["state"];
still records proposed_action;
abstains, because the progress check (game) fails. Its summary is the exception text, so reason contains it. Example: a two-state chart with Limits(max_game_vertices=1) gives reason="2 vertices exceed limit 1" and extras={"state": "b"} after go; with Limits(max_karp_vertices=1) the reason is "2 vertices exceed the mean-payoff limit 1".

A parity loss or a negative mean has the same shape, with _game_note reading parity_win=False ... or ... nonnegative_mean=False.

Cached once, not per event¶

Zielonka and Karp run once, from the initial state. decide does not re-solve as the chart moves, so a module sitting in paging still reports the result computed from watch. The check is a property of the policy, like star height, not a live sensor. Per-event work on this path is chart.step plus the four evidence checks.

Changing this code¶

Self-loops go on final states only. Adding an idle loop to every state would let the controller win by standing still, and the check would pass for almost every chart.
The grammar priorities (2 for action and final states, 1 otherwise) assume max-parity: the largest priority seen infinitely often decides. If you change the parity convention, change those numbers with it.
Changing priorities or owners changes which policies pass. Test it against every example (make snapshots).
The attractor's any/all rule follows owner. Do not hard-code it.
Keep Karp's inner minimum.
Do not add Truffet's step.
Test solver changes against brute force, as test_zielonka_matches_brute_force_on_random_games does.