Merge branch '391-performance-improvement-woflan' into 'integration'

Performance improvement WOFLAN

Closes #391

See merge request process-intelligence-solutions/pm4py!1407

Author: fit-daniel-schuster

pm4py/algo/analysis/woflan/algorithm.py

@@ -3,6 +3,7 @@
 from pm4py.objects.petri_net.utils import petri_utils
 import copy
 import numpy as np
+from collections import deque
 
 # Importing for place invariants related stuff (s-components, uniform and
 # weighted place invariants)
@@ -573,11 +574,12 @@ def step_7(woflan_object, return_asap_when_unsound=False):
             woflan_object.get_net(),
         )
     )
-    if len(check_for_improper_conditions(woflan_object.get_mcg())) == 0:
+    improper = check_for_improper_conditions(woflan_object.get_mcg())
+    if len(improper) == 0:
         woflan_object.diagnostic_messages.append("No improper coditions.")
         if woflan_object.print_diagnostics:
             print("No improper conditions.")
-        if woflan_object.get_left:
+        if woflan_object.get_left():
             return step_8(
                 woflan_object,
                 return_asap_when_unsound=return_asap_when_unsound,
@@ -588,16 +590,9 @@ def step_7(woflan_object, return_asap_when_unsound=False):
                 return_asap_when_unsound=return_asap_when_unsound,
             )
     else:
-        woflan_object.diagnostic_messages.append(
-            "Improper WPD. The following are the improper conditions: {}.".format(
-                check_for_improper_conditions(
-                    woflan_object.get_mcg())))
+        woflan_object.diagnostic_messages.append("Improper WPD. The following are the improper conditions: {}.".format(improper))
         if woflan_object.print_diagnostics:
-            print(
-                "Improper WPD. The following are the improper conditions: {}.".format(
-                    check_for_improper_conditions(woflan_object.get_mcg())
-                )
-            )
+            print("Improper WPD. The following are the improper conditions: {}.".format(improper))
         if return_asap_when_unsound:
             return False
         return step_9(
@@ -606,14 +601,9 @@ def step_7(woflan_object, return_asap_when_unsound=False):
 
 
 def step_8(woflan_object, return_asap_when_unsound=False):
-    if check_for_substates(woflan_object.get_mcg()):
-        return step_10(
-            woflan_object, return_asap_when_unsound=return_asap_when_unsound
-        )
-    else:
-        return step_10(
-            woflan_object, return_asap_when_unsound=return_asap_when_unsound
-        )
+    return step_10(
+        woflan_object, return_asap_when_unsound=return_asap_when_unsound
+    )
 
 
 def step_9(woflan_object, return_asap_when_unsound=False):
@@ -792,39 +782,34 @@ def compute_non_live_sequences(woflan_object):
         if all(np.equal(woflan_object.get_r_g().nodes[node]["marking"], f_m)):
             sucessfull_terminate_state = node
             break
-    # red nodes are those from which the final marking is not reachable
-    red_nodes = []
-    for node in woflan_object.get_r_g().nodes:
-        if not nx_utils.has_path(
-            woflan_object.get_r_g(), node, sucessfull_terminate_state
-        ):
-            red_nodes.append(node)
-    # Compute directed spanning tree
-    spanning_tree = nx_utils.Edmonds(woflan_object.get_r_g()).find_optimum()
-    queue = set()
-    paths = {}
-    # root node
-    queue.add(0)
-    paths[0] = []
-    processed_nodes = set()
+    if sucessfull_terminate_state is None:
+        return []
+    reversed_graph = woflan_object.get_r_g().reverse(copy=False)
+    can_reach_final = nx_utils.descendants(
+        reversed_graph, sucessfull_terminate_state
+    )
+    can_reach_final.add(sucessfull_terminate_state)
+    red_nodes = set(woflan_object.get_r_g().nodes) - can_reach_final
+
+    queue = deque()
+    queue.append((0, []))
+    shortest_path_len = {0: 0}
     red_paths = []
-    while len(queue) > 0:
-        v = queue.pop()
-        for node in spanning_tree.neighbors(v):
-            if node not in paths and node not in processed_nodes:
-                paths[node] = paths[v].copy()
-                # we can use directly 0 here, since we are working on a
-                # spanning tree and there should be no more edges to a node
-                paths[node].append(
-                    woflan_object.get_r_g().get_edge_data(v, node)[0][
-                        "transition"
-                    ]
-                )
-                if node not in red_nodes:
-                    queue.add(node)
-                else:
-                    red_paths.append(paths[node])
-        processed_nodes.add(v)
+    while queue:
+        node, path = queue.popleft()
+        if node in red_nodes:
+            red_paths.append(path)
+            continue
+        for successor in woflan_object.get_r_g().successors(node):
+            edge_data = woflan_object.get_r_g().get_edge_data(node, successor)
+            if not edge_data:
+                continue
+            transition = next(iter(edge_data.values()))["transition"]
+            next_path = path + [transition]
+            if successor in shortest_path_len and len(next_path) >= shortest_path_len[successor]:
+                continue
+            shortest_path_len[successor] = len(next_path)
+            queue.append((successor, next_path))
     return red_paths
 
 
@@ -848,70 +833,53 @@ def check_for_markings_larger_than_final_marking(graph, f_m):
             woflan_object.get_net(), woflan_object.get_initial_marking()
         )
     )
+    tree = woflan_object.get_restricted_coverability_tree()
     f_m = convert_marking(
         woflan_object.get_net(), woflan_object.get_final_marking()
     )
-    infinite_markings = []
-    for node in woflan_object.get_restricted_coverability_tree().nodes:
-        if (
-            np.inf
-            in woflan_object.get_restricted_coverability_tree().nodes[node][
-                "marking"
-            ]
-        ):
-            infinite_markings.append(node)
-    larger_markings = check_for_markings_larger_than_final_marking(
-        woflan_object.get_restricted_coverability_tree(), f_m
+    infinite_markings = {
+        node
+        for node, data in tree.nodes(data=True)
+        if np.inf in data["marking"]
+    }
+    larger_markings = set(
+        check_for_markings_larger_than_final_marking(tree, f_m)
     )
-    green_markings = []
-    for node in woflan_object.get_restricted_coverability_tree().nodes:
-        add_to_green = True
-        for marking in infinite_markings:
-            if nx_utils.has_path(
-                woflan_object.get_restricted_coverability_tree(), node, marking
-            ):
-                add_to_green = False
-        for marking in larger_markings:
-            if nx_utils.has_path(
-                woflan_object.get_restricted_coverability_tree(), node, marking
-            ):
-                add_to_green = False
-        if add_to_green:
-            green_markings.append(node)
-    red_markings = []
-    for node in woflan_object.get_restricted_coverability_tree().nodes:
-        add_to_red = True
-        for node_green in green_markings:
-            if nx_utils.has_path(
-                woflan_object.get_restricted_coverability_tree(),
-                node,
-                node_green,
-            ):
-                add_to_red = False
-                break
-        if add_to_red:
-            red_markings.append(node)
+    bad_nodes = infinite_markings | larger_markings
+
+    postorder_nodes = list(nx_utils.topological_sort(tree))[::-1]
+    subtree_has_bad = {}
+    subtree_has_green = {}
+    green_markings = set()
+
+    for node in postorder_nodes:
+        children = list(tree.successors(node))
+        has_bad = node in bad_nodes or any(subtree_has_bad.get(child, False) for child in children)
+        is_green = not has_bad
+        if is_green:
+            green_markings.add(node)
+        subtree_has_bad[node] = has_bad
+        subtree_has_green[node] = is_green or any(
+            subtree_has_green.get(child, False) for child in children
+        )
+
+    red_markings = {
+        node for node in tree.nodes if not subtree_has_green.get(node, False)
+    }
     # Make the path as short as possible. If we reach a red state, we stop and
     # do not go further in the "red zone".
-    queue = set()
-    queue.add(0)
-    paths = {}
-    paths[0] = []
+    queue = deque()
+    queue.append((0, []))
     paths_to_red = []
-    while len(queue) > 0:
-        v = queue.pop()
-        successors = (
-            woflan_object.get_restricted_coverability_tree().successors(v)
-        )
+    while queue:
+        v, path = queue.popleft()
+        if v in red_markings:
+            paths_to_red.append(path)
+            continue
+        successors = tree.successors(v)
         for suc in successors:
-            paths[suc] = paths[v].copy()
-            paths[suc].append(
-                woflan_object.get_restricted_coverability_tree().get_edge_data(
-                    v, suc
-                )["transition"]
-            )
-            if suc in red_markings:
-                paths_to_red.append(paths[suc])
-            else:
-                queue.add(suc)
+            edge_data = tree.get_edge_data(v, suc)
+            transition = edge_data["transition"] if edge_data else None
+            next_path = path + [transition]
+            queue.append((suc, next_path))
     return paths_to_red

pm4py/algo/analysis/woflan/graphs/minimal_coverability_graph/minimal_coverability_graph.py

@@ -55,9 +55,7 @@ def remove_subtree(tree, n):
 
     G = nx_utils.MultiDiGraph()
 
-    incidence_matrix = helper.compute_incidence_matrix(net)
-    firing_dict = helper.split_incidence_matrix(incidence_matrix, net)
-    req_dict = helper.compute_firing_requirement(net)
+    _, req_sparse, deltas, _, _ = helper.compute_firing_requirement(net)
 
     initial_mark = helper.convert_marking(net, initial_marking, original_net)
     j = 0
@@ -126,7 +124,7 @@ def remove_subtree(tree, n):
                     unprocessed_nodes.append(n)
         else:
             enabled_markings = helper.enabled_markings(
-                firing_dict, req_dict, G.nodes[n]["marking"]
+                req_sparse, deltas, G.nodes[n]["marking"]
             )
             for el in enabled_markings:
                 G.add_node(j, marking=el[0])
@@ -136,7 +134,7 @@ def remove_subtree(tree, n):
                 j += 1
             processed_nodes.add(n)
 
-    return (G, firing_dict, req_dict)
+    return (G, req_sparse, deltas)
 
 
 def apply(net, initial_marking, original_net=None):
@@ -151,12 +149,11 @@ def apply(net, initial_marking, original_net=None):
     def detect_same_labelled_nodes(G):
         same_labels = {}
         for node in G.nodes:
-            if np.array2string(G.nodes[node]["marking"]) not in same_labels:
-                same_labels[np.array2string(G.nodes[node]["marking"])] = [node]
+            marking_key = helper.marking_to_key(G.nodes[node]["marking"])
+            if marking_key not in same_labels:
+                same_labels[marking_key] = [node]
             else:
-                same_labels[np.array2string(G.nodes[node]["marking"])].append(
-                    node
-                )
+                same_labels[marking_key].append(node)
         return same_labels
 
     def merge_nodes_of_same_label(G, same_labels):
@@ -171,16 +168,20 @@ def merge_nodes_of_same_label(G, same_labels):
                     i += 1
         return G
 
-    mct, firing_dict, req_dict = minimal_coverability_tree(
+    mct, req_sparse, deltas = minimal_coverability_tree(
         net, initial_marking, original_net
     )
     mcg = merge_nodes_of_same_label(mct, detect_same_labelled_nodes(mct))
 
     to_remove_edges = []
+    enabled_cache = {}
     for edge in mcg.edges:
-        reachable_markings = helper.enabled_markings(
-            firing_dict, req_dict, mcg.nodes[edge[0]]["marking"]
-        )
+        source = edge[0]
+        if source not in enabled_cache:
+            enabled_cache[source] = helper.enabled_markings(
+                req_sparse, deltas, mcg.nodes[source]["marking"]
+            )
+        reachable_markings = enabled_cache[source]
         not_reachable = True
         for el in reachable_markings:
             if np.array_equal(el[0], mcg.nodes[edge[1]]["marking"]):

pm4py/algo/analysis/woflan/graphs/reachability_graph/reachability_graph.py

@@ -14,10 +14,7 @@ def apply(net, initial_marking, original_net=None):
     initial_marking = helper.convert_marking(
         net, initial_marking, original_net
     )
-    firing_dict = helper.split_incidence_matrix(
-        helper.compute_incidence_matrix(net), net
-    )
-    req_dict = helper.compute_firing_requirement(net)
+    _, req_sparse, deltas, _, _ = helper.compute_firing_requirement(net)
     look_up_indices = {}
     j = 0
     reachability_graph = nx_utils.MultiDiGraph()
@@ -26,25 +23,26 @@ def apply(net, initial_marking, original_net=None):
     working_set = set()
     working_set.add(j)
 
-    look_up_indices[np.array2string(initial_marking)] = j
+    look_up_indices[helper.marking_to_key(initial_marking)] = j
 
     j += 1
     while len(working_set) > 0:
         m = working_set.pop()
         possible_markings = helper.enabled_markings(
-            firing_dict, req_dict, reachability_graph.nodes[m]["marking"]
+            req_sparse, deltas, reachability_graph.nodes[m]["marking"]
         )
         for marking in possible_markings:
-            if np.array2string(marking[0]) not in look_up_indices:
-                look_up_indices[np.array2string(marking[0])] = j
+            marking_key = helper.marking_to_key(marking[0])
+            if marking_key not in look_up_indices:
+                look_up_indices[marking_key] = j
                 reachability_graph.add_node(j, marking=marking[0])
                 working_set.add(j)
                 reachability_graph.add_edge(m, j, transition=marking[1])
                 j += 1
             else:
                 reachability_graph.add_edge(
                     m,
-                    look_up_indices[np.array2string(marking[0])],
+                    look_up_indices[marking_key],
                     transition=marking[1],
                 )
     return reachability_graph