Skip to content

Internals

These pages are for someone who will change how the library works inside, not just call it. They explain how a policy string becomes a state machine, how that machine becomes a small game the progress check solves, and what the optional router and compare helpers actually compute. This overview tells you which work happens once when a module is built and which happens on every decision, which failures raise an exception and which make every decision abstain, and what must not be "improved" without reading the mathematics first.

It assumes you know the public picture: Architecture and One decision, step by step. If those pages still feel like a list of names, start at Anatomy of a decision. The file layout is on Package structure.

Two phases: build once, decide many times

The public contract is one call: Module.decide(Event, EvidenceSnapshot) returns a frozen DecisionRecord. Everything behind it splits into two phases.

Once, when the module is built. A policy string (or an explicit Statechart) becomes a graph the solvers can read. Star height is checked. A Thompson NFA is built and turned into a deterministic automaton by subset construction, whose states are named s0, s1, ... in a statechart; the automaton's dead state (reached when the policy has no continuation) is left out of the chart. The progress check compiles the chart into a game (adding a self-loop only to final states, those with no way out) and runs Zielonka's parity algorithm and Karp's mean-cycle algorithm on it. The two answers are cached as _game_ok and _mean_ok. If the graph is too large or the recursion too deep, both are set to false: the module still exists and still steps, but every decision abstains.

On every event. The chart moves to the next state, or stays put for an event the state does not handle (unknown, or known but out of order). Six check reports are built from the cached flags and the evidence. Any failure gives abstain with the proposed action recorded. The solvers are not re-run.

The router and compare helpers sit beside this path. decide never calls them.

flowchart LR
    T[policy text] --> P[Lark parse]
    P --> E[Expr tree]
    B[Python builders] --> E
    E --> H["star height ≤ 3"]
    H --> N[Thompson NFA]
    N --> D[subset DFA]
    D --> S["statechart s0, s1, ..."]
    X[hand-built Statechart] --> S
    S --> G["game + final-state loops"]
    G --> Z[Zielonka]
    G --> K[Karp]
    Z --> M[Module]
    K --> M
    S --> M
    M --> DEC["decide: step + 6 checks"]
    R[dispatch / compare] -.->|"optional, called by you"| DEC

The internals pages

Page Code After reading you can
Grammar compile grammar/parse.py, policy.lark, ast.py, height.py, dfa.py, statechart/machine.py change the policy language, draw a Thompson fragment, follow subset construction, explain why complement drops actions
Games and solvers statechart/game.py, parity.py, mean_payoff.py say exactly what the progress check proves (and what it assumes), walk Zielonka, fill a Karp table
Router and compare router/dispatch.py, ugc.py, wl.py, compare/*.py trace dispatch, say what each handler guarantees, describe the table sampler correctly

Signatures for the same modules: API reference. Trust levels and the gap between theorem and practice: Trust levels and honest limits.

What fails where

Work When On failure
Lark parse parse(source) ParseError (empty input, illegal character, unexpected token; expected tokens listed sorted)
Star height compile_expr, Module.from_expr, Module.__post_init__ StarHeightError; the module is never built
NFA / DFA size compile_expr CompileError; the module is never built
Ambiguous actions compile_expr CompileError (Policy is ambiguous: ...) when one event can lead to two different actions; the module is never built
dfa_to_statechart Module.from_expr none if the DFA is well formed
chart.validate() Module.__post_init__ ValueError on a missing initial state or dangling transition
compile_game Module.__post_init__ GameTooLarge caught: flags false, module exists, every decision abstains
Zielonka Module.__post_init__ ParityUnsolved caught: same as above
Karp Module.__post_init__ GameTooLarge above max_karp_vertices caught: flags false, every decision abstains; otherwise no exception (if no cycle is reachable the mean is 0.0)
Chart step every decide event not handled in this state: stay, proposed_action is None
Six checks every decide any fail: Verdict.ABSTAIN, proposal kept
dispatch only if you call it RouterRefuse for an unknown subgoal or a wrong envelope; a result with ok=False for undec, exptime_trap, fpras, or WL above the cap

The difference between "raises, the module never exists" and "the module exists, every decision abstains" is deliberate. A fourth nested * is a mistake in the policy: you find out at deploy time. A chart with 201 states is a request for more than Limits allows: the honest answer is "I will not act", not an unbounded computation. Because the module still exists, you can still step it and inspect extras["state"]. Keep GameTooLarge and ParityUnsolved caught in Module._solve_game; turning them into exceptions would change that contract. More: When the solvers refuse.

Limits

Every cap is a field of the frozen Limits object, passed to Module and to dispatch. Exceeding one raises at build time or makes the progress check fail; nothing falls back to a slower exact procedure, and the millisecond budgets are not timers (they are targets checked by tests/test_performance_budget.py). max_table_cells_exact and max_switch_steps are read by the table samplers in compare, which raise ValueError above them. The full table, with units and when to change each value: Defaults and limits.

A string becoming a step

Take the policy the tests use:

test(ping) ; act(ack)
  1. Lark reads policy.lark, tokenises, parses, and the transformer returns Seq((Test("ping"), Act("ack"))).
  2. Star height is 0. The alphabet is {ping}; actions are not events.
  3. Thompson construction gives four NFA states: 0 --ping--> 1 --ε--> 2 --ε--> 3, with state 3 marked ack.
  4. Subset construction: the start set is \(\{0\}\). After ping, the ε-closure of \(\{1\}\) is \(\{1,2,3\}\), marked ack. A further ping leads to the empty set, the dead state (DFA.dead is 2). Three DFA states.
  5. dfa_to_statechart leaves the dead state out and names the others s0 and s1, with one arrow s0 --ping--> s1. s0 proposes nothing and has a way out, so its priority is 1 (odd); s1 has verdict ACT, action ack and no way out, so its priority is 2 (even).
  6. compile_game adds a _final self-loop to s1, the only state with no outgoing arrow.
  7. Zielonka: from s0 the only play is s0, s1, s1, …; the largest priority seen forever is 2 (even), so the controller wins. Karp: all payoffs are 0, the best mean is 0, so nonnegative_mean holds. The progress check passes.
  8. A second ping in s1 is not handled: the entity stays in s1 and nothing is proposed.
  9. decide(Event("ping"), evidence) steps s0 → s1, proposes ack, and acts only if the neighbour-agreement, knife-edge, unusual-case and support checks also pass.

Grammar compile draws every NFA fragment and fills the subset table; Games and solvers does the same for Zielonka and Karp.

Two easily confused splits

parse.py is only a front end. It knows nothing about star height or automata. A new keyword or comment form is a change to policy.lark and the transformer, not to dfa.py. dfa.py assumes it already has an Expr; a different NFA construction, handling of missing events, or complement encoding is a change there, not in Lark.

On the game side, machine.py is the object a policy author edits; game.py, parity.py and mean_payoff.py are the solvers. compile_game adds a self-loop only to final states, so every play is infinite; there is no idle loop on other states.

Things that are absent on purpose

Read the matching theory page and the CatalogRef in certificates.py before "adding" any of these.

  • No two-player tropical mean-payoff step (Truffet). The math catalog (result 104) records a finite counterexample. Karp is the one-player solver and is exact for these charts.
  • No rewriting a policy down to star height 3. The limit is checked on the policy as written. Four nested * fail even if an equivalent shallower policy exists.
  • No semidefinite-programming Max-Cut. The handler uses the top Laplacian eigenvector plus local search, which guarantees at least half the edges are cut. α_GW ≈ 0.8786 is reported as the best ratio a polynomial algorithm can promise if the Unique Games Conjecture holds, never as a guarantee of this code.
  • No FPRAS for general tables. Two-row tables are sampled exactly from the hypergeometric (Fisher exact test) distribution, which is not uniform over tables. Wider tables use a switch chain whose mixer_status says not_paper_fpras.
  • No prophet factor \(2^{-310}\) as a product number. It is reported on the result and not used. factor_claimed=0.5 is reported only by single_item_max_of_samples (bar = the largest of one past sample per arrival), for which it is a proven guarantee in expectation; the scalar-bar rule single_item_one_sample reports None.
  • No Weisfeiler–Leman above k = 2. Level k costs roughly \(n^{k+1}\); the cap is a cost budget, and the refusal label exptime_trap means "too expensive under our budget".
  • No search for rational roots. The rational_zeros handler always refuses. In the wider literature, Hilbert's tenth problem is undecidable over the integers (a theorem) and open over the rationals; the math catalog (result 004) states the rational case as a claim. See Questions with no algorithm.

Changing a solver

  1. Read the theory page under Theory and the CatalogRef in certificates.py. Make sure you implement the checked statement, not the strongest sentence of a paper.
  2. Change the smallest module. Star height is height.py. Thompson fragments are _compile_nfa in dfa.py. Final-state self-loops are at the end of compile_game; grammar priorities are set in dfa_to_statechart. Zielonka is even_wins, _solve and attractor in parity.py. Karp is _karp. Envelope refusals are at the top of dispatch.
  3. Add a test next to the existing ones (tests/test_grammar.py, test_games.py, test_router_compare.py, test_runtime.py). For solvers, compare against brute force, as test_zielonka_matches_brute_force_on_random_games does.
  4. If you change an advertised constant (gw_alpha, k_median_threshold, the reconstruction margin, the knife-edge prefactor), update the theory page, Defaults and limits and the README in the same change, and run make snapshots.
  5. Never start a Lean process from Python; catalog references are strings.

Reading order

  1. This page.
  2. Grammar compile, including the test(ping) ; act(ack) trace.
  3. Games and solvers: what the progress check proves, final-state loops, Zielonka and Karp.
  4. Router and compare if you are touching envelopes, approximations, tables, prophet or optimal transport.

Then reread One decision, step by step with the cached flags in mind.