Formal Card-Game Systems
r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Formal Card-Game Systems

Learn how a card-game rule becomes an explicit state, a permitted transition and a property that can be checked. Follow a worked mechanism into its exact TLA+ definitions, then read the evidence at the scope it actually supports.

The reference describes one particular asymmetric two-participant system. SideA and SideB have different resources, permissions and objectives. Meet the reference profile introduces those roles without assuming earlier game knowledge.

Start with one state change

A participant has five tokens and wants to spend two. Which conditions make that legal? What changes together? How do we know that a zero payment occurred when the balance stayed the same?

Start with Reading a model. It introduces pre-state and post-state notation, unchanged fields and the first invariant before the payment chapter uses them.

Three separate teaching models explain payment, object lifetime and priority in small states. The larger reference profile then develops setup, turns, operations, traversal, inspection, abilities, registry lifecycle and checkpoint composition. The teaching models have their own narrower source and evidence; they do not replace those full-profile contracts.

Choose a route

Route

What you can do

Learn

Build the concepts in order, using concrete neutral examples. No earlier TLA+ knowledge is assumed.

Reference

Look up a contract, module or qualified definition and follow its dependencies.

Evidence

Inspect the configured properties, bounds, assumptions and outcomes behind a result.

Experienced readers can enter through the full payment interface, registry contract, subject evidence, or module reference. The generated definitions are lookup material; the learning path explains why their distinctions matter.

Keep the question and its evidence together

A nonnegative-balance invariant asks a different question from eventual completion. A prepared calculation asks a different question from exploring reachable states. An instructional specialization asks a narrower question than a general payment interpreter.

Each evidence page identifies its own input and result class. The release context shown above identifies the candidate or admitted artifact you are reading. Use the evidence guide before transferring a result to another model, configuration or implementation.

Source and examples remain readable without JavaScript. Where a trace has been admitted, its complete state sequence accompanies any interactive controls. A successful check need not emit a trace, and a page without one should say so.

Looking for an earlier preview bookmark?

These static links lead to the current explanations. Each result retains its own evidence scope.