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: 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).

  • 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)