Statechart

A statechart is the policy drawn as a flowchart: named states, arrows labelled with events, and an optional proposed action on each state. You build one directly with Statechart when you need payoffs, priorities or environment-owned states (environment=True) that the text policy cannot express; otherwise Module.from_expr builds it for you. The game modules here run once, when a Module is built, to compute the "can the workflow keep going?" check.

Public here: Statechart (top level). Transition, GameGraph, compile_game, even_wins and max_mean_payoff are importable from the submodules but mainly matter to contributors. What the game check does and does not catch: Can the workflow keep going?; solver internals: Games and solvers.

machine

Statecharts compiled from explicit states or from a DFA.

A statechart is the encapsulated control object: named states, the transitions between them, and what each state proposes. Charts are flat (no nested or parallel states), so the compiled game stays a single graph.

Statechart dataclass

Statechart(
    name: str,
    initial: str = "start",
    _states: dict[str, Verdict | None] = dict[
        str, Verdict | None
    ](),
    _actions: dict[str, str | None] = dict[
        str, str | None
    ](),
    _transitions: list[Transition] = list[Transition](),
    _parent: dict[str, str | None] = dict[
        str, str | None
    ](),
    _payoff: dict[str, float] = dict[str, float](),
    _priority: dict[str, int] = dict[str, int](),
    _environment: dict[str, bool] = dict[str, bool](),
)

Mutable builder; freeze with validate() before use.

state

state(
    name: str,
    *,
    initial: bool = False,
    verdict: Verdict | None = None,
    action: str | None = None,
    parent: str | None = None,
    payoff: float = 0.0,
    priority: int = 0,
    environment: bool = False,
) -> Statechart

Add a state.

Parameters:

Name	Type	Description	Default
name	str	State name, unique in this chart.	required
initial	bool	Make this the start state.	False
verdict	Verdict | None	What the state means when reached (None: act if an action is proposed).	None
action	str | None	The action this state proposes.	None
parent	str | None	Recorded for nesting-aware callers; charts stay flat.	None
payoff	float	Mean-payoff weight earned on entering the state.	0.0
priority	int	Parity priority for the progress check. Even means looping through this state forever is fine for the service; odd means it is not.	0
environment	bool	The environment, not the service, picks the next event here (for example, waiting on a customer). The progress check then assumes the worst choice.	False

Source code in src/grounded_decision/statechart/machine.py

def state(
    self,
    name: str,
    *,
    initial: bool = False,
    verdict: Verdict | None = None,
    action: str | None = None,
    parent: str | None = None,
    payoff: float = 0.0,
    priority: int = 0,
    environment: bool = False,
) -> Statechart:
    """Add a state.

    Args:
        name: State name, unique in this chart.
        initial: Make this the start state.
        verdict: What the state means when reached (``None``: act if
            an action is proposed).
        action: The action this state proposes.
        parent: Recorded for nesting-aware callers; charts stay flat.
        payoff: Mean-payoff weight earned on entering the state.
        priority: Parity priority for the progress check. Even means
            looping through this state forever is fine for the service;
            odd means it is not.
        environment: The environment, not the service, picks the next
            event here (for example, waiting on a customer). The
            progress check then assumes the worst choice.
    """

    self._states[name] = verdict
    self._actions[name] = action
    self._parent[name] = parent
    self._payoff[name] = payoff
    self._priority[name] = priority
    self._environment[name] = environment
    if initial:
        self.initial = name
    return self

is_environment

is_environment(name: str) -> bool

Whether the environment picks the next event in this state.

Source code in src/grounded_decision/statechart/machine.py

def is_environment(self, name: str) -> bool:
    """Whether the environment picks the next event in this state."""

    return self._environment.get(name, False)

dfa_to_statechart

dfa_to_statechart(name: str, dfa: DFA) -> Statechart

Build a statechart from a compiled policy.

State s{i} is DFA state i. The DFA's reject sink (the state reached when the policy has no continuation for an event) is left out: an event the policy does not allow in the current state is "not handled", exactly like an event the policy never names. The entity stays where it is and nothing is proposed.

Priorities for the progress check: states that propose an action and states with no way out (final states) get 2 (even); every other state gets 1 (odd). The game is won by the largest priority seen infinitely often, so the policy passes the progress check only if, from the start, it can keep reaching states that propose an action or reach a final state. A policy that can loop forever without proposing anything fails.

Source code in src/grounded_decision/statechart/machine.py

def dfa_to_statechart(name: str, dfa: DFA) -> Statechart:
    """Build a statechart from a compiled policy.

    State ``s{i}`` is DFA state ``i``. The DFA's reject sink (the state
    reached when the policy has no continuation for an event) is left out:
    an event the policy does not allow in the current state is "not
    handled", exactly like an event the policy never names. The entity
    stays where it is and nothing is proposed.

    Priorities for the progress check: states that propose an action and
    states with no way out (final states) get 2 (even); every other state
    gets 1 (odd). The game is won by the largest priority seen infinitely
    often, so the policy passes the progress check only if, from the
    start, it can keep reaching states that propose an action or reach a
    final state. A policy that can loop forever without proposing
    anything fails.
    """

    chart = Statechart(name)
    kept = [i for i in range(dfa.states) if i != dfa.dead]
    successors: dict[int, list[tuple[str, int]]] = {
        i: [
            (letter, dfa.trans[i][j])
            for j, letter in enumerate(dfa.alphabet)
            if dfa.trans[i][j] != dfa.dead
        ]
        for i in kept
    }
    for i in kept:
        action = dfa.actions[i]
        verdict = (
            Verdict.ACT if action else (Verdict.ABSTAIN if dfa.accepting[i] else None)
        )
        final = not successors[i]
        chart.state(
            f"s{i}",
            initial=(i == dfa.start),
            verdict=verdict,
            action=action,
            priority=_PROGRESS if (action or final) else _NO_PROGRESS,
        )
    for i in kept:
        for letter, target in successors[i]:
            chart.on(f"s{i}", letter, f"s{target}")
    return chart.validate()

game

Compile a statechart to a graph game.

Vertices are states. Edges are transitions. Parity is the state's priority (even = the controller can loop forever; odd = the environment wins the loop). Payoff is the state's mean-payoff contribution.

Only states with no outgoing transitions (final states) get a self-loop, so a play never gets stuck. Other states get no idle loop: waiting in a state forever counts only if that state's own transitions allow it.

parity

Zielonka's algorithm for parity games on modest graphs.

A parity game is played by two players moving a token along the edges of a graph. Every vertex has a priority (a small integer). The controller (player Even) wins an infinite play if the largest priority that appears infinitely often is even; the environment (player Odd) wins otherwise. Each vertex is owned by one player, who chooses the next edge there.

The controller wins from a vertex if it has a strategy that wins every play starting there, whatever the environment does. When the controller owns every vertex (the default in charts compiled by :func:grounded_decision.statechart.game.compile_game; states marked environment=True belong to the environment), that is the same as: some path from the vertex reaches a cycle whose largest priority is even.

The solver is the classical recursive algorithm (Zielonka 1998). It returns both players' winning regions, which partition the vertices.

CONTROLLER module-attribute

CONTROLLER = 0

Player index of the controller (Even); matches GameGraph.owner 0.

ENVIRONMENT module-attribute

ENVIRONMENT = 1

Player index of the environment (Odd); matches GameGraph.owner 1.

even_wins

even_wins(
    game: GameGraph, limits: Limits = DEFAULT_LIMITS
) -> tuple[bool, ...]

For each vertex, whether the controller (Even) wins from it.

Source code in src/grounded_decision/statechart/parity.py

def even_wins(game: GameGraph, limits: Limits = DEFAULT_LIMITS) -> tuple[bool, ...]:
    """For each vertex, whether the controller (Even) wins from it."""

    if game.n > limits.max_game_vertices:
        raise ParityUnsolved("game exceeds vertex limit")
    successors = [
        sorted({successor for successor, _event, _payoff in game.edges[vertex]})
        for vertex in range(game.n)
    ]
    controller_region, _environment_region = _solve(
        set(range(game.n)), game, successors, depth=0, limits=limits
    )
    return tuple(vertex in controller_region for vertex in range(game.n))

attractor

attractor(
    universe: set[int],
    target: set[int],
    *,
    player: int,
    game: GameGraph,
    successors: list[list[int]],
) -> set[int]

Vertices of universe from which player can force a visit to target.

A vertex joins when its owner is player and some move leads into the set, or when its owner is the opponent and every move does (an opponent with no move left inside universe is stuck and joins too).

Source code in src/grounded_decision/statechart/parity.py

def attractor(
    universe: set[int],
    target: set[int],
    *,
    player: int,
    game: GameGraph,
    successors: list[list[int]],
) -> set[int]:
    """Vertices of ``universe`` from which ``player`` can force a visit to ``target``.

    A vertex joins when its owner is ``player`` and *some* move leads into
    the set, or when its owner is the opponent and *every* move does (an
    opponent with no move left inside ``universe`` is stuck and joins too).
    """

    attracted = set(target) & universe
    changed = True
    while changed:
        changed = False
        for vertex in universe - attracted:
            moves_inside = [
                successor for successor in successors[vertex] if successor in universe
            ]
            if game.owner[vertex] == player:
                joins = any(successor in attracted for successor in moves_inside)
            else:
                joins = all(successor in attracted for successor in moves_inside)
            if joins:
                attracted.add(vertex)
                changed = True
    return attracted

mean_payoff

One-player mean-payoff via Karp's minimum/maximum mean cycle.

Two-player tropical elimination (Truffet) is banned: Lean records a finite counterexample (family 104). For 1-player compiled statecharts Karp is exact.

max_mean_payoff

max_mean_payoff(
    game: GameGraph, limits: Limits = DEFAULT_LIMITS
) -> float

Maximum mean weight of a reachable cycle from the start (Karp).

Raises:

Type	Description
GameTooLarge	The game has more than limits.max_karp_vertices vertices (Karp's table is quadratic in that number).

Source code in src/grounded_decision/statechart/mean_payoff.py

def max_mean_payoff(game: GameGraph, limits: Limits = DEFAULT_LIMITS) -> float:
    """Maximum mean weight of a reachable cycle from the start (Karp).

    Raises:
        GameTooLarge: The game has more than ``limits.max_karp_vertices``
            vertices (Karp's table is quadratic in that number).
    """

    return _karp_maximum(game, limits=limits)

min_mean_payoff

min_mean_payoff(
    game: GameGraph, limits: Limits = DEFAULT_LIMITS
) -> float

Minimum mean weight of a reachable cycle from the start (Karp).

Computed as minus the maximum mean of the same game with every weight negated, so there is a single implementation of Karp's recurrence.

Raises:

Type	Description
GameTooLarge	The game has more than limits.max_karp_vertices vertices.

Source code in src/grounded_decision/statechart/mean_payoff.py

def min_mean_payoff(game: GameGraph, limits: Limits = DEFAULT_LIMITS) -> float:
    """Minimum mean weight of a reachable cycle from the start (Karp).

    Computed as minus the maximum mean of the same game with every weight
    negated, so there is a single implementation of Karp's recurrence.

    Raises:
        GameTooLarge: The game has more than ``limits.max_karp_vertices``
            vertices.
    """

    negated = GameGraph(
        names=game.names,
        start=game.start,
        edges=tuple(
            tuple((target, event, -weight) for target, event, weight in outgoing)
            for outgoing in game.edges
        ),
        priority=game.priority,
        owner=game.owner,
    )
    return -_karp_maximum(negated, limits=limits)

nonnegative_mean

nonnegative_mean(
    game: GameGraph, limits: Limits = DEFAULT_LIMITS
) -> bool

Zero-threshold winning set test used by the Lean 104 scope.

Raises:

Type	Description
GameTooLarge	The game has more than limits.max_karp_vertices vertices.

Source code in src/grounded_decision/statechart/mean_payoff.py

def nonnegative_mean(game: GameGraph, limits: Limits = DEFAULT_LIMITS) -> bool:
    """Zero-threshold winning set test used by the Lean 104 scope.

    Raises:
        GameTooLarge: The game has more than ``limits.max_karp_vertices``
            vertices.
    """

    return max_mean_payoff(game, limits) >= -1e-12