App State Simulator (sysi) is a C header for writing simulations of systems and checking them exhaustively. The model is ordinary C, the check is a compiled program, and the header walks the state graph. It is for system designs in general. Distributed systems are the usual subject, and the same header applies to any finite-state design that can be written this way.
TLA+ is a similar interesting idea. sysi is an alternative based on similar ideas: name the system state, allow a transition only when its guard passes, state the invariants, and check those invariants on every state the transitions can reach.
The header is sysi.h. A specification is one .c file that includes it, describes the system, and is compiled with no C runtime and no libraries beyond kernel32.
A system is a state. The specification names every variable that matters and gives the initial value of that state. Two states are the same when their bytes are equal, so every byte, including any padding in the state struct, is initialized deterministically.
Change is a set of guarded transitions, called actions. Each action has a finite list of choices, such as which client and which key. The action looks at the current state and the choice. It returns false when that choice is not enabled. When the choice is enabled, the framework has already copied the current state, and the action edits that copy into the successor. The guard is what makes an illegal step absent from the graph rather than present and then rejected.
Invariants are predicates on a single state. Each one returns true when the state is acceptable. They are the properties the design claims: exclusion rules, valid codes, conservation of a resource, and anything else that must hold everywhere the system can go.
After the graph is closed, a liveness property looks at the edges. It can require that some state stays reachable from every reached state, that every execution eventually arrives there, that a state with no enabled action is forbidden or allowed only under a stated circumstance, or that every state can get back to the start. The dictionary requires that both clients can become idle again from any reached state. Clients may keep starting new work, so the check asks for a path back to idle, and it accepts a run that never takes that path.
Given that description, the framework walks the graph. It starts at the initial state and applies every choice of every action. A successor whose bytes have been seen before is not stored again. The walk is breadth-first, so the first time a state is reached, the path to it is a shortest path. Each level of that walk is expanded by one thread per logical processor. The threads meet, and the new states are recorded in state order, before the next level starts, so that first path stays a shortest path. Every reached state is checked against every invariant. If they all hold in every reached state, the specification is verified for this finite model. If one fails, the checker prints the invariant's name, the shortest sequence of actions from the initial state, and the state after each step, then returns a nonzero exit code.
SYSI_STATE defines the state struct. SYSI_ACTION defines a transition and records its trace name, choice count, and choice text beside the function. SYSI_INVARIANT defines a predicate and records its printed name beside the function. SYSI_LIVENESS defines a closed-graph predicate and records its printed name, its kind, and its goal sample beside the function. The specification lists actions, invariants, and liveness properties in the order they are tried. The module and those lists are registered on the SysiSpec. sysi_run is the walk. The included dictionary specification is the concrete shape of that registration.
Actions and invariants in the example:
StartRead,StartWrite, andStartCountbegin one operation each.Finishends whichever operation that client is in.- Two clients may read the same key at the same time.
- A write excludes every other access to its key. Writes of different keys may overlap.
Countreads the whole dictionary, so it runs only while every client is idle, and no other operation runs during a count.- A write flips whether its key is present, which keeps the set of states finite.
OperationCodesAreValidkeeps every stored code inside the range the actions use.DictionaryAccessIsSerializablerestates the exclusion rules on the state itself.ClientsCanBecomeIdlerequires a path from every reached state back to both clients idle.
config.bat holds the path to Visual Studio's x64 tools in VCVARS64. A value already set in the environment is left alone, so one run can point somewhere else without editing the file. The default is Visual Studio 2022 Community.
From this directory:
build.batThat compiles example_spec.c into out\example_spec.exe. The program is one translation unit, linked without the C runtime. kernel32.dll is the only system library it calls. The same build compiles test.c into out\test.exe and runs it. test.c checks the walk, the invariants, and the liveness properties.
build.bat runbuilds the same way and then runs the checker. The executable on its own is out\example_spec.exe. A passing run prints how many states and transitions were explored and returns exit code 0. A failing invariant returns 1. A limit, an incomplete specification, or an allocation failure returns 2. A failing liveness property returns 3.
The checker commits each table once, up to a fixed ceiling. It leaves those ranges in place when it exits. The system reclaims them with the process.
out is created by the build and is listed in .gitignore. Object files stay there.
The checker is a non-interactive console program. It has no keyboard shortcuts and no mouse controls. The build script and the process exit code are the interface.
The code is released under the Unlicense. That is the standard public-domain dedication for software with no limits on use: copying, modification, and distribution are unrestricted for any purpose. There is no warranty, no guarantee, and no liability.