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:

  • petri_net (PetriNet) – petri net

  • initial_marking (Marking) – initial marking

  • final_marking (Marking) – final marking

Return type:

bool

import pm4py

net, im, fm = pm4py.read_pnml('model.pnml')
is_sound = pm4py.check_soundness(net, im, fm)