Kayfabe: Model-based program testing with TLC
summary
Kayfabe is a C# harness that runs TLC, extracts the full TLC state graph, computes a minimal spanning set of behaviors by reducing routing to TSP (NP‑hard) and then drives the program through each behavior checking state equality and action enablement. It supports Pressler-style trace checking and model‑based testing, uses Google OR-Tools for TSP heuristics, requires a serializer/mapping for GUIDs and hidden variables, and currently scales practically to models up to roughly 10,000 states before routing (V^2) becomes the bottleneck.
AI-written summary · about
chapters (24)
- 0:00Intro
- 0:18Motivation
- 0:58Tradeoffs between testing methods
- 1:45What is Kayfabe?
- 2:09Trace Checker: Idea
- 4:22Model-Based Testing: Kayfabe Model Player
- 7:29Model Player: Blindspots
- 8:54System Architecture
- 10:09Model Player: Steps
- 10:51Routing Algorithm: Problem Description
- 11:48Routing Algorithm: Graph Construction 2
- 12:59Routing Algorithm: Computing the Tour
- 14:13Transition Inspection Problem
- 15:19Chinese Postman Approach - Example
- 16:06TLA+ Serialization
- 16:50TSP Solver
- 17:49How to build a Kayfabe model harness
- 18:28Example: MapCollection
- 18:57Data Contracts
- 19:19Execution Context
- 19:49State Mapping Function
- 20:36Implementing Actions
- 21:15Running the Test
- 21:46Routing Algorithm Alternatives
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
30mTackling Concurrency Bugs with TLA+
01h 12mDistributed systems showdown — TLA + vs real code
23m„Complete” In-Sprint Testing Using Collaborative Models
14mModel-guided Fuzzing of Distributed Systems
43mCan you Test it
44mModel-Based Testing for the Zephyr RTOS
29mGeneration and Refinement of Testing Models