pm4py.analysis.check_soundness#
- pm4py.analysis.check_soundness(petri_net: PetriNet, initial_marking: Marking, final_marking: Marking) bool [source]#
Check if a given Petri net is a sound WF-net. A Petri net is a WF-net iff:
it has a unique source place
it has a unique end place
every element in the WF-net is on a path from the source to the sink place
- A WF-net is sound iff:
it contains no live-locks
it contains no deadlocks
we are able to always reach the final marking
For a formal definition of sound WF-net, consider: http://www.padsweb.rwth-aachen.de/wvdaalst/publications/p628.pdf
- Parameters:
- Return type:
bool
import pm4py net, im, fm = pm4py.read_pnml('model.pnml') is_sound = pm4py.check_soundness(net, im, fm)