2424from pm4py .objects .petri_net .utils import petri_utils
2525import copy
2626import numpy as np
27+ from collections import deque
2728
2829# Importing for place invariants related stuff (s-components, uniform and
2930# weighted place invariants)
@@ -594,11 +595,12 @@ def step_7(woflan_object, return_asap_when_unsound=False):
594595 woflan_object .get_net (),
595596 )
596597 )
597- if len (check_for_improper_conditions (woflan_object .get_mcg ())) == 0 :
598+ improper = check_for_improper_conditions (woflan_object .get_mcg ())
599+ if len (improper ) == 0 :
598600 woflan_object .diagnostic_messages .append ("No improper coditions." )
599601 if woflan_object .print_diagnostics :
600602 print ("No improper conditions." )
601- if woflan_object .get_left :
603+ if woflan_object .get_left () :
602604 return step_8 (
603605 woflan_object ,
604606 return_asap_when_unsound = return_asap_when_unsound ,
@@ -609,16 +611,9 @@ def step_7(woflan_object, return_asap_when_unsound=False):
609611 return_asap_when_unsound = return_asap_when_unsound ,
610612 )
611613 else :
612- woflan_object .diagnostic_messages .append (
613- "Improper WPD. The following are the improper conditions: {}." .format (
614- check_for_improper_conditions (
615- woflan_object .get_mcg ())))
614+ woflan_object .diagnostic_messages .append ("Improper WPD. The following are the improper conditions: {}." .format (improper ))
616615 if woflan_object .print_diagnostics :
617- print (
618- "Improper WPD. The following are the improper conditions: {}." .format (
619- check_for_improper_conditions (woflan_object .get_mcg ())
620- )
621- )
616+ print ("Improper WPD. The following are the improper conditions: {}." .format (improper ))
622617 if return_asap_when_unsound :
623618 return False
624619 return step_9 (
@@ -627,14 +622,9 @@ def step_7(woflan_object, return_asap_when_unsound=False):
627622
628623
629624def step_8 (woflan_object , return_asap_when_unsound = False ):
630- if check_for_substates (woflan_object .get_mcg ()):
631- return step_10 (
632- woflan_object , return_asap_when_unsound = return_asap_when_unsound
633- )
634- else :
635- return step_10 (
636- woflan_object , return_asap_when_unsound = return_asap_when_unsound
637- )
625+ return step_10 (
626+ woflan_object , return_asap_when_unsound = return_asap_when_unsound
627+ )
638628
639629
640630def step_9 (woflan_object , return_asap_when_unsound = False ):
@@ -813,39 +803,34 @@ def compute_non_live_sequences(woflan_object):
813803 if all (np .equal (woflan_object .get_r_g ().nodes [node ]["marking" ], f_m )):
814804 sucessfull_terminate_state = node
815805 break
816- # red nodes are those from which the final marking is not reachable
817- red_nodes = []
818- for node in woflan_object .get_r_g ().nodes :
819- if not nx_utils .has_path (
820- woflan_object .get_r_g (), node , sucessfull_terminate_state
821- ):
822- red_nodes .append (node )
823- # Compute directed spanning tree
824- spanning_tree = nx_utils .Edmonds (woflan_object .get_r_g ()).find_optimum ()
825- queue = set ()
826- paths = {}
827- # root node
828- queue .add (0 )
829- paths [0 ] = []
830- processed_nodes = set ()
806+ if sucessfull_terminate_state is None :
807+ return []
808+ reversed_graph = woflan_object .get_r_g ().reverse (copy = False )
809+ can_reach_final = nx_utils .descendants (
810+ reversed_graph , sucessfull_terminate_state
811+ )
812+ can_reach_final .add (sucessfull_terminate_state )
813+ red_nodes = set (woflan_object .get_r_g ().nodes ) - can_reach_final
814+
815+ queue = deque ()
816+ queue .append ((0 , []))
817+ shortest_path_len = {0 : 0 }
831818 red_paths = []
832- while len (queue ) > 0 :
833- v = queue .pop ()
834- for node in spanning_tree .neighbors (v ):
835- if node not in paths and node not in processed_nodes :
836- paths [node ] = paths [v ].copy ()
837- # we can use directly 0 here, since we are working on a
838- # spanning tree and there should be no more edges to a node
839- paths [node ].append (
840- woflan_object .get_r_g ().get_edge_data (v , node )[0 ][
841- "transition"
842- ]
843- )
844- if node not in red_nodes :
845- queue .add (node )
846- else :
847- red_paths .append (paths [node ])
848- processed_nodes .add (v )
819+ while queue :
820+ node , path = queue .popleft ()
821+ if node in red_nodes :
822+ red_paths .append (path )
823+ continue
824+ for successor in woflan_object .get_r_g ().successors (node ):
825+ edge_data = woflan_object .get_r_g ().get_edge_data (node , successor )
826+ if not edge_data :
827+ continue
828+ transition = next (iter (edge_data .values ()))["transition" ]
829+ next_path = path + [transition ]
830+ if successor in shortest_path_len and len (next_path ) >= shortest_path_len [successor ]:
831+ continue
832+ shortest_path_len [successor ] = len (next_path )
833+ queue .append ((successor , next_path ))
849834 return red_paths
850835
851836
@@ -869,70 +854,53 @@ def check_for_markings_larger_than_final_marking(graph, f_m):
869854 woflan_object .get_net (), woflan_object .get_initial_marking ()
870855 )
871856 )
857+ tree = woflan_object .get_restricted_coverability_tree ()
872858 f_m = convert_marking (
873859 woflan_object .get_net (), woflan_object .get_final_marking ()
874860 )
875- infinite_markings = []
876- for node in woflan_object .get_restricted_coverability_tree ().nodes :
877- if (
878- np .inf
879- in woflan_object .get_restricted_coverability_tree ().nodes [node ][
880- "marking"
881- ]
882- ):
883- infinite_markings .append (node )
884- larger_markings = check_for_markings_larger_than_final_marking (
885- woflan_object .get_restricted_coverability_tree (), f_m
861+ infinite_markings = {
862+ node
863+ for node , data in tree .nodes (data = True )
864+ if np .inf in data ["marking" ]
865+ }
866+ larger_markings = set (
867+ check_for_markings_larger_than_final_marking (tree , f_m )
886868 )
887- green_markings = []
888- for node in woflan_object .get_restricted_coverability_tree ().nodes :
889- add_to_green = True
890- for marking in infinite_markings :
891- if nx_utils .has_path (
892- woflan_object .get_restricted_coverability_tree (), node , marking
893- ):
894- add_to_green = False
895- for marking in larger_markings :
896- if nx_utils .has_path (
897- woflan_object .get_restricted_coverability_tree (), node , marking
898- ):
899- add_to_green = False
900- if add_to_green :
901- green_markings .append (node )
902- red_markings = []
903- for node in woflan_object .get_restricted_coverability_tree ().nodes :
904- add_to_red = True
905- for node_green in green_markings :
906- if nx_utils .has_path (
907- woflan_object .get_restricted_coverability_tree (),
908- node ,
909- node_green ,
910- ):
911- add_to_red = False
912- break
913- if add_to_red :
914- red_markings .append (node )
869+ bad_nodes = infinite_markings | larger_markings
870+
871+ postorder_nodes = list (nx_utils .topological_sort (tree ))[::- 1 ]
872+ subtree_has_bad = {}
873+ subtree_has_green = {}
874+ green_markings = set ()
875+
876+ for node in postorder_nodes :
877+ children = list (tree .successors (node ))
878+ has_bad = node in bad_nodes or any (subtree_has_bad .get (child , False ) for child in children )
879+ is_green = not has_bad
880+ if is_green :
881+ green_markings .add (node )
882+ subtree_has_bad [node ] = has_bad
883+ subtree_has_green [node ] = is_green or any (
884+ subtree_has_green .get (child , False ) for child in children
885+ )
886+
887+ red_markings = {
888+ node for node in tree .nodes if not subtree_has_green .get (node , False )
889+ }
915890 # Make the path as short as possible. If we reach a red state, we stop and
916891 # do not go further in the "red zone".
917- queue = set ()
918- queue .add (0 )
919- paths = {}
920- paths [0 ] = []
892+ queue = deque ()
893+ queue .append ((0 , []))
921894 paths_to_red = []
922- while len (queue ) > 0 :
923- v = queue .pop ()
924- successors = (
925- woflan_object .get_restricted_coverability_tree ().successors (v )
926- )
895+ while queue :
896+ v , path = queue .popleft ()
897+ if v in red_markings :
898+ paths_to_red .append (path )
899+ continue
900+ successors = tree .successors (v )
927901 for suc in successors :
928- paths [suc ] = paths [v ].copy ()
929- paths [suc ].append (
930- woflan_object .get_restricted_coverability_tree ().get_edge_data (
931- v , suc
932- )["transition" ]
933- )
934- if suc in red_markings :
935- paths_to_red .append (paths [suc ])
936- else :
937- queue .add (suc )
902+ edge_data = tree .get_edge_data (v , suc )
903+ transition = edge_data ["transition" ] if edge_data else None
904+ next_path = path + [transition ]
905+ queue .append ((suc , next_path ))
938906 return paths_to_red
0 commit comments