pm4py.analysis.check_soundness#

pm4py.analysis.check_soundness(petri_net: PetriNet, initial_marking: Marking, final_marking: Marking, print_diagnostics: bool = False) → Tuple[bool, Dict[str, Any]][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 In the returned object, the first element is a boolean indicating if the Petri net is a sound workflow net. The second element is a set of diagnostics collected while running WOFLAN (expressed as a dictionary associating the keys [name of the diagnostics] with the corresponding diagnostics).

Parameters:

petri_net (PetriNet) – petri net
initial_marking (Marking) – initial marking
final_marking (Marking) – final marking
print_diagnostics (bool) – boolean value that sets up additional prints during the execution of WOFLAN

Return type:

Tuple[bool, Dict[str, Any]]

import pm4py

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