The engine accepts Petri nets in XML format and verifies a reachability query and aims to provide a fast untimed engine for TAPAAL.
GNU General Public License v3.0
7
stars
17
forks
source link
Loop instead of deadlock - trace issue #133
Closed
srba closed 1 year ago
Run the following verification:
verifypn-osx64 --k-bound 5 --trace --search-strategy BestFS --reduction 1 --ltl-algorithm --xml-queries 1 model.xml query.xml
and it returns the following trace:
The loop-tag is redundant (as there is no loop, just deadlock). loop-LTL-problem.zip