thomascothran/pavlov/pavlov-model-checking

Pavlov model checking

Pavlov model checking explores all reachable event traces for a set of bthreads, reporting deadlocks, livelocks, safety violations, hot-state liveness violations, and impossible events. It is designed for model-first development: specify the behavior and properties, run the checker, then iterate on implementation.

Terminology

Safety properties

Safety properties say "something bad never happens." In Pavlov, safety checks are defined as safety bthreads and passed under :safety-bthreads. They monitor the trace and emit an event with :invariant-violated true when the rule is broken.

Hot-state liveness

Hot-state liveness says that once the model enters certain states, progress is required. In Pavlov, liveness is expressed directly on bids with :hot true.

• A hot-state violation happens when execution terminates while hot, deadlocks while hot, or can remain hot forever.
• check/check reports at most one hot-state witness under :liveness-violation.

Possibility checks

Use :possible when you want to prove that an event is reachable on at least one path.

Deadlocks

A deadlock means no events are possible and no terminal event occurred. Deadlocks matter when you expect the model to make progress or terminate. If you are modeling an open system, you can add environment bthreads or disable :check-deadlock? while refining the model.

Livelocks

A livelock means the model cycles forever without reaching a terminal event. Livelocks matter when progress should eventually happen; if cycles are intentional, consider :check-livelock? false or add a terminal event to represent completion.

Choose your path

• Building or updating a model? See ./references/designing-models.md
• Need API details or config options? Use docstrings.
• Need concrete model-checking examples? Start with the tech.thomascothran.pavlov.model.check/check docstring, then use the tests for edge cases.
• Need help designing models and properties? Use the modeling reference.
• Need to understand results? Use the interpretation reference.

Model-first workflow

See ./references/workflow.md

Default scenario branching

• Use a single check/check call per bthread group to cover all scenarios.
• Create one initiating bthread whose first bid requests a set of starting events to form the top-level branch.
• Model each positive scenario as its own bthread and assert its completion event with :possible.

For the detailed workflow, read the Best practices section in the tech.thomascothran.pavlov.model.check docstring.

Where to look

• Docstrings: clojure.repl/doc on tech.thomascothran.pavlov.model.check/check.
• Tests (edge cases and regression coverage): resource tech/thomascothran/pavlov/model/check_test.clj.
• Repo path: modules/pavlov-devtools/test/tech/thomascothran/pavlov/model/check_test.clj.
• Direct hot-state liveness coverage: resource tech/thomascothran/pavlov/model/check/liveness_test.clj.
• Modeling guidance: resource skills/pavlov-model-checking/references/designing-models.md.
• Result interpretation: resource skills/pavlov-model-checking/references/interpret-results.md.
• REPL setup: resource skills/pavlov-model-checking/references/model-checker-repl.md.