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!
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.
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.