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]#

Checks if a given Petri net is a sound Workflow net (WF-net).

A Petri net is a WF-net if and only if:

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 if and only if:

It contains no live-locks.
It contains no deadlocks.
It is always possible to reach the final marking from any reachable marking.

For a formal definition of a sound WF-net, refer to: http://www.padsweb.rwth-aachen.de/wvdaalst/publications/p628.pdf

The returned tuple consists of:

A boolean indicating whether the Petri net is a sound WF-net.
A dictionary containing diagnostics collected while running WOFLAN, associating diagnostic names with their corresponding details.

Parameters:

petri_net (PetriNet) – The Petri net to check.
initial_marking (Marking) – The initial marking of the Petri net.
final_marking (Marking) – The final marking of the Petri net.
print_diagnostics (bool) – If True, additional diagnostics will be printed during the execution of WOFLAN.

Returns:

A tuple containing a boolean indicating soundness and a dictionary of diagnostics.

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)