About
Pnmc is a symbolic model checker for Petri nets written in C++14. It uses the libsdd library which implements Hierarchical Set Decision Diagrams. It ranked second at the Model Checking Contest in 2014 and 2015, in the State Space category.
Pre-compiled binaries for Linux 64 bits are available here.
Features
- Symbolic generation of state spaces
- Symbolic generation of state spaces of Timed Petri nets using discrete time semantics
- Verification of dead states (deadlocks)
- Verification of dead transitions
- Verification of a subset of the reachability properties of the Model Checking Contest
License
Pnmc is released under the BSD license.
News
- (2016-06-30) pnmc ranked third at the Model Checking Contest in the State Space category; 10 tools were participating.
- (2015-08-30) Version 20150830 released:
- Fixes a situation were untimed transitions would not update impacted timed transitions;
- Tina's .net format is now the default one.
- (2015-08-19) pnmc ranked second at the Model Checking Contest in the State Space category; 11 tools were participating.