A collection of tools for exploring High-Level Petri nets !
Hue is an API and a collection of tools for checking reachability properties directly on High-Level Petri nets. It accepts models in PNML format and the same formula language used in the Model-Checking Contest (MCC).
Example of models and formulas can be found in the benchmarks folder, which
contains colored models extracted from the 2022 edition of the MCC.
An oracle for the reachability competition of MCC 2023 can be found in the source repository of the htest command, at: ./htest/oracle_reach2023.txt. We also provide an oracle for the 2022 edition, ./htest/oracle_reach2022.txt, compiled from information provided by Yann Thierry-Mieg, see here.
uwalk is a prototype stepper (a simulation tool) that performs random,
parallel exploration over a high-level net without unfolding it. It can also
test for ReachabilityCardinality (option -r) or ReachabilityFireability
(option -f) properties on the fly.
hsimplify is a command that applies elementary simplifications over reachability formulas and can also, in some cases, find tautologies.
htest is a tool that can compare verification results, for the Reachability competition, with oracles files computed on the 2022 and 2023 edition of the MCC.
horacle is an internal set of conversion utilities that were used to compile
the oracle file used by htest for the 2023 edition of the MCC.