Texas Hold'em Model

This post demonstrates how Petri nets handle complex multi-player state machines. Texas Hold'em poker requires turn-taking, role-based permissions, betting conditions, and a complete audit trail. Rather than coding these rules imperatively, we encode them structurally in a Petri net.

Try the interactive demo at pilot.pflow.xyz/texas-holdem.

The Challenge

Poker has intricate state:

• Phases: preflop → flop → turn → river → showdown
• Turn order: Players act in sequence, skipping folded players
• Actions: fold, check, call, raise—each with preconditions
• Roles: Only the dealer can deal cards, only active players can bet

Traditional implementations scatter this logic across conditionals. A Petri net makes it explicit and verifiable.

State Machine: Betting Rounds

The core flow is a sequential state machine. Each betting round is a place, and phase transitions move the game forward:

Places represent game phases:

• waiting — Before hand starts
• preflop — Hole cards dealt, first betting round
• flop — Three community cards revealed
• turn_round — Fourth card revealed
• river — Fifth card revealed
• showdown — Final comparison
• complete — Hand finished

Transitions like deal_flop require the previous phase and betting_done to be marked—ensuring all players have acted before advancing.

Turn Control with Tokens

Each player has a turn place (p0_turn, p1_turn, etc.). When it's Player 0's turn, only p0_turn holds a token. Player actions consume their turn token and produce the next player's:

p0_check:
  inputs:  [p0_turn, p0_active]
  outputs: [p1_turn]

This enforces strict turn order without explicit checks—the structure makes illegal moves impossible.

Role-Based Access Control

Not all transitions are available to all players. The model uses roles to restrict who can fire which transitions:

When using go-pflow, the API enforces these roles—a player can't fire another player's transitions.

Guards: Betting Conditions

Some actions require additional conditions beyond token availability. Guards are boolean expressions that must evaluate true:

p0_raise:
  guard: "bets[0] >= current_bet && chips[0] >= raise_amount"

This ensures:

• Player has matched the current bet
• Player has enough chips to raise

Guards add business logic without complicating the Petri net structure. The net handles what can happen; guards handle when.

Event Sourcing: Audit Trail

Every transition firing creates an immutable event:

[
  {"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"}
]

This provides:

• Replay: Recreate any game state from events
• Audit: Verify all moves were legal
• Undo: Roll back to previous states

The Petri net's discrete transitions map perfectly to event sourcing—each firing is one event.

ODE for Strategic Analysis

While the game runs discretely, ODE simulation provides strategic insights. By converting the Petri net to continuous dynamics, we can evaluate position strength:

The simulation treats possible outcomes as competing flows. Higher ODE values for win_p0 indicate stronger positions. This is similar to the tic-tac-toe ODE analysis, scaled up for poker's larger state space.

Model Structure

The full model has:

Places (17):
  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,       — Active markers
  p3_active, p4_active
  betting_done                           — Sync signal

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, ...                  — Skip folded players

View in pflow editor →

Key Concepts Demonstrated

Why Petri Nets for Games?

Traditional game code mixes state, rules, and UI. A Petri net separates concerns:

• Structure = What's possible (places, transitions, arcs)
• State = What's current (token marking)
• Rules = What's allowed (guards, roles)
• History = What happened (events)

This separation makes games:

• Verifiable: Prove invariants (e.g., exactly one player acts at a time)
• Replayable: Deterministic event sequence
• Analyzable: ODE simulation for strategy
• Evolvable: Add rules without rewriting logic

Conclusion

Texas Hold'em demonstrates that Petri nets scale beyond simple workflows. Complex multi-player games with turn order, role permissions, and conditional logic fit naturally into the place-transition-arc paradigm.

The model doesn't contain poker strategy—it contains poker structure. Strategy emerges from analysis (ODE simulation) rather than being hardcoded. This separation of mechanism from policy is the core Petri net insight.

For foundational concepts: Tic-Tac-Toe Model

For the theory behind ODE analysis: Declarative Differential Models