Merge pull request #74 from jcrozum/control-with-lazy-diagram

reconciling #71 and #73 for #69

conftest.py

@@ -1,17 +1,27 @@
+# type: ignore
 import os
-from biodivine_aeon import BooleanNetwork # type: ignore
-# The purpose of this file is to detect tests with `network_file` as input and 
-# then supply these tests with networks from `bbm-bnet-inputs-true` up to a certain
-# network size. This network size can be configured using `--networksize` and 
-# its default value is 20.
+
+from biodivine_aeon import BooleanNetwork
+
+# The purpose of this file is to detect tests with `network_file` as input and
+# then supply these tests with networks from `bbm-bnet-inputs-true` up to a
+# certain network size. This network size can be configured using
+# `--networksize` and its default value is 20.
 
 # We intentionally test on the `-inputs-true` models as opposed to `-inputs-identity`,
 # as having fixed inputs ensures there are not too many trap spaces, fixed points, etc.
 
+
 def pytest_addoption(parser):
-    parser.addoption("--networksize", action="store", default="20", help="Only check networks up to this size.")
+    parser.addoption(
+        "--networksize",
+        action="store",
+        default="20",
+        help="Only check networks up to this size.",
+    )
+
 
-def pytest_generate_tests(metafunc):    
+def pytest_generate_tests(metafunc):
     if "network_file" in metafunc.fixturenames:
         size = int(metafunc.config.getoption("networksize"))
         models = []
@@ -24,4 +34,4 @@ def pytest_generate_tests(metafunc):
             if bn.num_vars() > size:
                 continue
             models.append(path)
-        metafunc.parametrize("network_file", models)
+        metafunc.parametrize("network_file", models)

nfvsmotifs/_sd_algorithms/__init__.py

@@ -1,11 +1,12 @@
 """
-This is an internal module which contains the implementations of the more involved 
-algorithms related to `SuccessionDiagram` construction and manipulation. The idea
-is that any implementation that requires some helper methods or data structures
-should be present here instead of `SuccessionDiagram.py` to avoid mixing of code
-used by different algorithms and bloating the core succession diagram implementation.
+This is an internal module which contains the implementations of the more
+involved algorithms related to `SuccessionDiagram` construction and
+manipulation. The idea is that any implementation that requires some helper
+methods or data structures should be present here instead of
+`SuccessionDiagram.py` to avoid mixing of code used by different algorithms and
+bloating the core succession diagram implementation.
 
-The algorithms within this module here should only use the public API of
-the `SuccessionDiagram` to avoid violating its invariants. The actual algorithms 
-are then "re-exported" as a public methods of the `SuccessionDiagram` class.
-"""
+The algorithms within this module here should only use the public API of the
+`SuccessionDiagram` to avoid violating its invariants. The actual algorithms are
+then "re-exported" as a public methods of the `SuccessionDiagram` class.
+"""

nfvsmotifs/_sd_algorithms/compute_attractor_seeds.py

@@ -5,21 +5,27 @@
 if TYPE_CHECKING:
     from nfvsmotifs.SuccessionDiagram import SuccessionDiagram
 
-from nfvsmotifs.motif_avoidant import detect_motif_avoidant_attractors, make_retained_set
-from nfvsmotifs.terminal_restriction_space import get_terminal_restriction_space
-from nfvsmotifs.trappist_core import compute_fixed_point_reduced_STG, trappist
 import nfvsmotifs
+import nfvsmotifs.SuccessionDiagram
+from nfvsmotifs.motif_avoidant import (
+    detect_motif_avoidant_attractors,
+    make_retained_set,
+)
+from nfvsmotifs.terminal_restriction_space import get_terminal_restriction_space
+from nfvsmotifs.trappist_core import compute_fixed_point_reduced_STG
+
 
 def compute_attractor_seeds(
     sd: SuccessionDiagram,
     node_id: int,
 ) -> list[dict[str, int]]:
     """
-    Compute the list of vertices such that each attractor within the subspace of the given `node_id` is covered by
-    exactly one vertex.
+    Compute the list of vertices such that each attractor within the subspace of
+    the given `node_id` is covered by exactly one vertex.
 
-    If the node is a stub, the result covers the whole subspace. If the node is expanded, the result only covers
-    the "immediate" subspace without the subspaces of the child nodes.
+    If the node is a stub, the result covers the whole subspace. If the node is
+    expanded, the result only covers the "immediate" subspace without the
+    subspaces of the child nodes.
     """
 
     if nfvsmotifs.SuccessionDiagram.DEBUG:
@@ -28,13 +34,14 @@ def compute_attractor_seeds(
     node_space = sd.node_space(node_id)
 
     if len(node_space) == sd.network.num_vars():
-        # This node is a fixed-point.     
+        # This node is a fixed-point.
         return [node_space]
 
-    # Compute the list of child spaces if the node is expanded. Otherwise "pretend" that there are no children.
+    # Compute the list of child spaces if the node is expanded. Otherwise
+    # "pretend" that there are no children.
     child_spaces = []
     if sd.node_is_expanded(node_id):
-        child_spaces = [ sd.node_space(s) for s in sd.node_successors(node_id) ]
+        child_spaces = [sd.node_space(s) for s in sd.node_successors(node_id)]
 
     # Fix everything in the NFVS to zero, as long as
     # it isn't already fixed by our `node_space`.
@@ -43,7 +50,7 @@ def compute_attractor_seeds(
     # the space is a trap and this will remove the corresponding unnecessary
     # Petri net transitions.
     retained_set = make_retained_set(sd.network, sd.nfvs, node_space, child_spaces)
-        
+
     if len(retained_set) == sd.network.num_vars() and len(child_spaces) == 0:
         # There is only a single attractor remaining here,
         # and its "seed" is the retained set.
@@ -62,7 +69,7 @@ def compute_attractor_seeds(
         retained_set,
         ensure_subspace=node_space,
         avoid_subspaces=child_spaces,
-    )        
+    )
 
     if nfvsmotifs.SuccessionDiagram.DEBUG:
         print(f"[{node_id}] Found {len(candidate_seeds)} seed candidates.")
@@ -78,7 +85,7 @@ def compute_attractor_seeds(
             candidate_seeds,
             terminal_restriction_space,
             max_iterations=1000,
-            is_in_an_mts=len(child_spaces)==0
+            is_in_an_mts=len(child_spaces) == 0,
         )
 
         return attractors

nfvsmotifs/_sd_algorithms/expand_attractor_seeds.py

@@ -5,24 +5,29 @@
 if TYPE_CHECKING:
     from nfvsmotifs.SuccessionDiagram import SuccessionDiagram
 
-from nfvsmotifs.trappist_core import compute_fixed_point_reduced_STG
+import nfvsmotifs
+import nfvsmotifs.SuccessionDiagram
 from nfvsmotifs.motif_avoidant import make_retained_set
 from nfvsmotifs.space_utils import intersect
-import nfvsmotifs
+from nfvsmotifs.trappist_core import compute_fixed_point_reduced_STG
+
 
 def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None):
     """
     See `SuccessionDiagram.expand_attractor_seeds` for documentation.
     """
 
-    # First, expand the succession diagram such that all minimal trap spaces are found.
-    # This reduces the amount of work performed in this algorithm, because for every attractor
-    # in a minimal trap space, we already have the closest trap space, now we just need to
-    # do the same for (potential) motif-avoidant attractors.
+    # First, expand the succession diagram such that all minimal trap spaces are
+    # found. This reduces the amount of work performed in this algorithm,
+    # because for every attractor in a minimal trap space, we already have the
+    # closest trap space, now we just need to do the same for (potential)
+    # motif-avoidant attractors.
     sd.expand_minimal_spaces(size_limit)
 
     if nfvsmotifs.SuccessionDiagram.DEBUG:
-        print("Minimal trap space expansion finished. Proceeding to attractor expansion.")
+        print(
+            "Minimal trap space expansion finished. Proceeding to attractor expansion."
+        )
 
     root = sd.root()
     seen = set([root])
@@ -37,21 +42,23 @@ def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None)
                 return False
 
             successors = sd.node_successors(node, compute=True)
-            successors = sorted(successors, reverse=True) # For determinism!
+            successors = sorted(successors, reverse=True)  # For determinism!
             # (reversed because we explore the list from the back)
-
-        node_space = sd.node_space(node)
 
         # Retrieve the stable motifs of children that are already expanded.
-        expanded_children = [ x for x in sd.node_successors(node) if sd.node_is_expanded(x) ]
-        expanded_motifs = [ sd.edge_stable_motif(node, child) for child in expanded_children ]
-
-        # Now, we skip all successors that are either already seen, or that 
+        expanded_children = [
+            x for x in sd.node_successors(node) if sd.node_is_expanded(x)
+        ]
+        expanded_motifs = [
+            sd.edge_stable_motif(node, child) for child in expanded_children
+        ]
+
+        # Now, we skip all successors that are either already seen, or that
         # do not contain any candidate states for motif-avoidant attractors.
         while len(successors) > 0:
             if successors[-1] in seen:
-                # The next node was already seen on stack. We can thus skip it and continue
-                # to the next one.
+                # The next node was already seen on stack. We can thus skip it
+                # and continue to the next one.
                 successors.pop()
                 continue
             if sd.node_is_expanded(successors[-1]):
@@ -65,8 +72,10 @@ def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None)
             successor_space = sd.node_space(successors[-1])
             retained_set = make_retained_set(sd.network, sd.nfvs, successor_space)
 
-            avoid_or_none = [ intersect(successor_space, child) for child in expanded_motifs ]
-            avoid = [ x for x in avoid_or_none if x is not None ]
+            avoid_or_none = [
+                intersect(successor_space, child) for child in expanded_motifs
+            ]
+            avoid = [x for x in avoid_or_none if x is not None]
 
             successor_seeds = compute_fixed_point_reduced_STG(
                 sd.petri_net,
@@ -77,14 +86,16 @@ def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None)
             )
 
             if len(successor_seeds) == 0:
-                # At this point, we know that this successor is not expanded and there are either
-                # no candidate states in it, or all candidate states are already covered by some
-                # other expanded successor.
+                # At this point, we know that this successor is not expanded and
+                # there are either no candidate states in it, or all candidate
+                # states are already covered by some other expanded successor.
                 successors.pop()
                 continue
 
             if nfvsmotifs.SuccessionDiagram.DEBUG:
-                print(f"[{node}] Found successor with new attractor candidate seeds. Expand node {successors[-1]}.")
+                print(
+                    f"[{node}] Found successor with new attractor candidate seeds. Expand node {successors[-1]}."
+                )
 
             break
 
@@ -100,5 +111,5 @@ def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None)
         stack.append((node, successors))
         # Push the successor onto the stack.
         stack.append((s, None))
-            
-    return True
+
+    return True

nfvsmotifs/_sd_algorithms/expand_bfs.py

@@ -5,11 +5,12 @@
 if TYPE_CHECKING:
     from nfvsmotifs.SuccessionDiagram import SuccessionDiagram
 
+
 def expand_bfs(
-    sd: SuccessionDiagram, 
-    node_id: int | None = None, 
-    bfs_level_limit: int | None = None, 
-    size_limit: int | None = None
+    sd: SuccessionDiagram,
+    node_id: int | None = None,
+    bfs_level_limit: int | None = None,
+    size_limit: int | None = None,
 ) -> bool:
     """
     See `SuccessionDiagram.expand_bfs` for documentation.
@@ -18,12 +19,12 @@ def expand_bfs(
     if node_id is None:
         node_id = sd.root()
 
-    seen = set()
+    seen: set[int] = set()
     seen.add(node_id)
 
     level_id = 0
     current_level = [node_id]
-    next_level = []
+    next_level: list[int] = []
 
     while len(current_level) > 0:
         for node in current_level:
@@ -42,9 +43,9 @@ def expand_bfs(
                 if s not in seen:
                     seen.add(s)
                     next_level.append(s)
-        
+
         # The level is explored. Check if this exceeds the level limit.
-        if  (bfs_level_limit is not None) and (level_id >= bfs_level_limit):
+        if (bfs_level_limit is not None) and (level_id >= bfs_level_limit):
             # Level limit reached.
             return False
 

nfvsmotifs/_sd_algorithms/expand_dfs.py

@@ -5,6 +5,7 @@
 if TYPE_CHECKING:
     from nfvsmotifs.SuccessionDiagram import SuccessionDiagram
 
+
 def expand_dfs(
     sd: SuccessionDiagram,
     node_id: int | None = None,
@@ -18,7 +19,7 @@ def expand_dfs(
     if node_id is None:
         node_id = sd.root()
 
-    seen = set()
+    seen: set[int] = set()
     seen.add(node_id)
 
     stack: list[tuple[int, list[int] | None]] = [(node_id, None)]
@@ -32,9 +33,9 @@ def expand_dfs(
             if (size_limit is not None) and (len(sd) >= size_limit):
                 # Size limit reached.
                 return False
-            
+
             successors = sd.node_successors(node, compute=True)
-            successors = sorted(successors, reverse=True) # For determinism!
+            successors = sorted(successors, reverse=True)  # For determinism!
             # (reversed because we explore the list from the back)
 
         # Remove all immediate successors that are already visited.
@@ -48,7 +49,7 @@ def expand_dfs(
         if (dfs_stack_limit is not None) and (len(stack) >= dfs_stack_limit):
             # We cannot push any successor nodes because it would exceed
             # the stack limit. As such, we can just continue with the next
-            # item on the stack. however, we must remember that we skipped 
+            # item on the stack. however, we must remember that we skipped
             # some nodes and the result is thus incomplete.
             result_is_complete = False
             continue
@@ -58,6 +59,6 @@ def expand_dfs(
         # Push the node back with the remaining successors.
         stack.append((node, successors))
         # Push the successor onto the stack.
-        stack.append((s, None))        
+        stack.append((s, None))
 
-    return result_is_complete
+    return result_is_complete