Awesome

petri-tlaplus 🕸️

TLA+ module for Petri Nets. Petri Nets are a simple and natural abstraction for modeling stepwise processes, concurrency, and stateful distributed systems.

Instantiate the PetriNet module to model a specific graph and assert temporal properties about all its possible executions!

Try it

Install the TLA+ tools. I install them with Nix by running nix-shell -p tlaplus.

# Model check Petri Nets.
tlc -deadlock Example1_Simple
tlc -deadlock Example3_Parallel

# Generate LaTeX PDF docs. See the `docs/` dir
tlatex -shade -latexCommand "pdflatex" -latexOutputExt "pdf" -metadir "docs" PetriNet

# Visualize the state graph using graphviz (*.dot files).
tlc -deadlock Example6_Bound -dump dot Example6_Bound

# Check all specification via make targets
make tlc       # model check all modules
make tlatex    # pretty-print all modules to `docs/`
make clean     # delete all generated files

See PetriNet.tla for the core module. See the Example_*.tla/Example_*.cfg files for usage and an introduction to some Petri net concepts.

Petri Net Specification

Excerpts of the constant and variable definitions and the core "Fire" action. See docs/PetriNet.pdf and docs/ dir for the full LaTeX pretty-printed specification and more examples.

Note that the "Workflow net" specifications are incomplete due to a limitation of the TLA+ model checker.