Prerequisite: the Tic-Tac-Toe Model introduces turn tokens and the place/transition vocabulary this post assumes.
Texas Hold'em is the largest of our tutorial nets: five seats, four streets, 18 places and 32 transitions, declared in one JSON file — services/texas-holdem.json, now kept in sim.pflow.xyz's source — from which a code generator produced an event-sourced Go service (examples/texasholdem). The browser demo and the generated example have since been retired; this post reads them as they stood on 2026-10-12. Poker needs phases, a strict turn order, actions with preconditions and a record of what happened; we put the first three into the net's structure wherever the structure can carry them, and this post says where it can't.
The phases are a chain of places — waiting, preflop, flop, turn_round, river, showdown, complete — and the transitions start_hand, deal_flop, deal_turn, deal_river, go_showdown, determine_winner and end_hand move a single token along it:
Each deal transition consumes the current phase token and a betting_done token, so the dealer cannot advance the street until the betting has gone round. What "gone round" means here is narrower than real poker: betting_done is produced by seat 4's action, so each street is exactly one orbit of the table, p0 through p4, and a raise does not reopen the action to the seats that already acted. Re-raise loops are not in this net.
Each seat has a turn place, p0_turn through p4_turn, and an active place, p0_active through p4_active. An action consumes the seat's turn token and produces the next seat's. From the model file, a check hands the active token back while a fold keeps it:
p0_check:
inputs: [p0_turn, p0_active]
outputs: [p0_active, p1_turn]
p0_fold:
inputs: [p0_turn, p0_active]
outputs: [p1_turn]
A seat that has folded has no active token, so fold, check, call and raise are all dead for it and only pN_skip — which needs nothing but the turn token — can pass the turn along. The turn order is enforced by the structure, and it is a conservation law rather than a hope: reading the arcs, every transition preserves
waiting + p0_turn + p1_turn + p2_turn + p3_turn + p4_turn + betting_done + showdown + complete = 1
so at most one seat can hold the turn at any marking. We checked that by hand against the 32 transitions in the JSON; it has not been run through an invariant solver for this post. The phase chain carries a second one of the same shape, waiting + preflop + flop + turn_round + river + showdown + complete = 1.
The model's access block restricts the dealer-side transitions to a dealer role, and declares admin as inheriting from dealer:
| Role | Transitions |
|---|---|
dealer |
start_hand, deal_flop, deal_turn, deal_river, go_showdown, determine_winner, end_hand |
admin |
inherits dealer (also listed on start_hand) |
There are no per-seat roles. Nothing in the model binds p0_raise to the person sitting in seat 0 — any caller can fire any seat's action while that seat holds the turn token. Enforcement is also thinner than the declaration: the code generator could emit a permission middleware from the access block, but the generated example, in the checkout we read for this revision, passes an empty rule list (examples/texasholdem/service.go, accessRules := []*AccessControl{}), and its router does not call the permission check. The roles are a declaration in this model, not a demonstrated guarantee.
Guards are boolean expressions over data that must hold before a transition fires. This net declares none — the generated README's transition table shows - in the Guard column for all 32. The kind of guard a raise would need looks like this (a sketch, not from the model):
p0_raise:
guard: "bets[0] >= current_bet && chips[0] >= raise_amount"
In the demo, chip stacks, bets, blinds and the pot live in the browser's JavaScript state (frontends/texas-holdem/main.js), not in the net. The division the post originally claimed — the net handles what can happen, guards handle when — is the right shape, but in this model only the first half exists.
Every transition in the model names an event type (p0_raise → p0_raised, deal_flop → flop_dealt), and the generated service stores those events in an event store and rebuilds the marking from them. A log looks roughly like this (a sketch: the amount and cards fields are from the model's event schema, the times are made up):
[
{"action": "start_hand", "time": "10:00:00"},
{"action": "p0_raise", "amount": 50, "time": "10:00:15"},
{"action": "p1_call", "time": "10:00:23"},
{"action": "p2_fold", "time": "10:00:31"},
{"action": "deal_flop", "cards": "Ah Ks 7d", "time": "10:00:35"}
]
Because each firing is one event, replaying the log through the net reconstructs the hand, and a firing that was not enabled cannot appear in a log the service accepted — the generated aggregate.go refuses any transition that cannot fire from the current marking before it writes an event. The earlier version of this post also promised undo; the generated code does not implement rollback (its GraphQL resolver still carries TODO: Implement proper version replay), so we have dropped the claim.
The demo's "strategic analysis" is not an ODE over the 18-place game net. For each decision, the frontend builds a separate eight-place net (buildHandStrengthPetriNet in main.js) whose initial marking and rates are set from card heuristics — made-hand rank, a preflop-quality score, and draw odds by the rule of 2 and 4 — solves it with the pflow.xyz Tsit5 solver, and reads off a hand_strength value. That value is then blended with the final values of three of the small net's input places by fixed weights (0.5 preflop quality, 0.3 current hand, 0.15 hand_strength, 0.05 improvement), and each action's expected value comes from hand-written formulas: fold is 0, a call is strength × (pot + call) − call, halved when strength is below the pot odds, and a raise is scaled up above a 0.6 strength threshold. The ODE is one aggregation step inside a heuristic, and the heuristic — not the net topology — decides the ranking.
That is the opposite of tic-tac-toe, where the ODE runs on the game net itself and the move values reduce to integers read off its structure. The poker version of that idea came later, in ZK Hold'em, where hand-strength values are read off a net's drain counts instead of hand-tuned weights. The drain counts are themselves hand-picked in ranking order, so the ranking is an input there, not a result.
Places (18):
waiting, preflop, flop, turn_round, — Phase places
river, showdown, complete
p0_turn, p1_turn, p2_turn, — Turn tokens
p3_turn, p4_turn
p0_active, p1_active, p2_active, — In-hand markers (initial 1)
p3_active, p4_active
betting_done — End-of-orbit sync
Transitions (32):
start_hand, deal_flop, deal_turn, — Phase transitions
deal_river, go_showdown, determine_winner,
end_hand
p0_fold, p0_check, p0_call, p0_raise, — Player 0 actions
p1_fold, p1_check, p1_call, p1_raise, — Player 1 actions
... (5 players × 4 actions)
p0_skip, p1_skip, ... — Pass the turn (needs only pN_turn)
One defect is visible in the arcs. end_hand puts a fresh token into every pN_active without consuming the old one, so a seat that played a hand to the end starts the next hand with two active tokens. A single fold then leaves it with one, and on the next street that seat can check, call or raise again. The active places are not 1-bounded across hands; end_hand needs to consume what is left, or the fold needs to drain the place. We have not patched the model — this is a report from reading it.
What the net does hold is poker's skeleton: the street order, the one-seat-at-a-time turn (provably, by the invariant above), the fact that a folded seat can only pass, and a log in which every entry is a firing. The arithmetic — chips, bet sizing, side pots, who wins — sits outside it, in guards the model does not yet declare and in frontend code. Whether that arithmetic can move into the net without the net ballooning is the open question here. The ZK poker build at stackedup.gg takes a different cut, splitting heads-up play across four cooperating nets.
This topic is covered in depth in Chapter 10: Complex State Machines of Petri Nets as a Universal Abstraction.
For readers of the January version, after checking the post against services/texas-holdem.json, the generated example and the demo frontend on 2026-10-12 (read, not re-run):
p0_check returns p0_active; the old snippet dropped that output. Added p0_fold and the turn-token invariant, checked by hand.player0 role and admin does not own end_hand/determine_winner; the dealer role owns all seven phase transitions. The claim that "a player can't fire another player's transitions" was wrong, and the generated example does not wire the role check.win_p0 description, which matched no code; the section now describes the frontend's hand-strength heuristic. Removed "the ODE earns its keep here" and "strategy emerges from analysis rather than being hardcoded", both contradicted by main.js.pN_active is refilled by end_hand, reported above.Related: Tic-Tac-Toe Model · ZK Hold'em · Building ZK Poker · Introducing sim.pflow.xyz · Declarative Differential Models