Formally introduce skip nodes with optimized attractor detection.

biobalm/_sd_algorithms/expand_minimal_spaces.py

@@ -5,12 +5,17 @@
 if TYPE_CHECKING:
     from biobalm.succession_diagram import SuccessionDiagram
 
+import copy
 from biobalm.space_utils import is_subspace
 from biobalm.trappist_core import trappist
+from biobalm.types import BooleanSpace
 
 
 def expand_minimal_spaces(
-    sd: SuccessionDiagram, node_id: int | None, size_limit: int | None = None
+    sd: SuccessionDiagram,
+    node_id: int | None,
+    size_limit: int | None = None,
+    skip_remaining: bool = False,
 ) -> bool:
     """
     See `SuccessionDiagram.expand_minimal_spaces` for documentation.
@@ -22,7 +27,9 @@ def expand_minimal_spaces(
     pn = sd.node_percolated_petri_net(node_id, compute=True)
     node_space = sd.node_data(node_id)["space"]
 
-    minimal_traps = trappist(network=pn, problem="min", ensure_subspace=node_space)
+    all_minimal_traps = trappist(network=pn, problem="min", ensure_subspace=node_space)
+    # We don't need to duplicate the actual trap spaces, just the list.
+    minimal_traps = copy.copy(all_minimal_traps)
 
     if sd.config["debug"]:
         print(
@@ -33,6 +40,27 @@ def expand_minimal_spaces(
 
     stack: list[tuple[int, list[int] | None]] = [(node_id, None)]
 
+    def make_skip_node(
+        sd: SuccessionDiagram, node_id: int, all_minimal_traps: list[BooleanSpace]
+    ):
+        node = sd.node_data(node_id)
+        if node["expanded"]:
+            return
+
+        skip_edges = 0
+        for m_trap in all_minimal_traps:
+            if is_subspace(m_trap, sd.node_data(node_id)["space"]):
+                m_id = sd._ensure_node(node_id, m_trap)  # type: ignore
+                m_data = sd.node_data(m_id)
+                m_data["expanded"] = True
+                skip_edges += 1
+
+        node["expanded"] = True
+        node["skipped"] = True
+
+        if sd.config["debug"]:
+            print(f"[{node_id}] Node skipped with {skip_edges} edges.")
+
     while len(stack) > 0:
         (node, successors) = stack.pop()
         if successors is None:
@@ -51,10 +79,13 @@ def expand_minimal_spaces(
         # do not cover any new minimal trap space.
         while len(successors) > 0:
             if successors[-1] in seen:
+                # Everything in seen is expanded, so no need to skip it.
                 successors.pop()
                 continue
             if len([s for s in minimal_traps if is_subspace(s, node_space)]) == 0:
-                successors.pop()
+                skipped = successors.pop()
+                if skip_remaining:
+                    make_skip_node(sd, skipped, all_minimal_traps)
                 continue
             break
 
@@ -64,6 +95,8 @@ def expand_minimal_spaces(
         if len(successors) == 0:
             if sd.node_is_minimal(node):
                 minimal_traps.remove(sd.node_data(node)["space"])
+                if sd.config["debug"]:
+                    print(f"Remaining minimal traps: {len(minimal_traps)}.")
             continue
 
         # At this point, we know that `s` is not visited and it contains
@@ -77,5 +110,8 @@ def expand_minimal_spaces(
         # Push the successor onto the stack.
         stack.append((s, None))
 
+        if sd.config["debug"]:
+            print(f"[{s}] Expanding...")
+
     assert len(minimal_traps) == 0
     return True

biobalm/_sd_algorithms/expand_source_blocks.py

@@ -15,6 +15,7 @@ def expand_source_blocks(
     check_maa: bool = True,
     size_limit: int | None = None,
     optimize_source_nodes: bool = True,
+    check_maa_exact: bool = False,
 ) -> bool:
     """
     Base correctness assumptions:
@@ -203,9 +204,14 @@ def expand_source_blocks(
                     # just get stuck on this node and the "partial" results wouldn't be usable.
                     is_clean = False
                     try:
-                        block_sd_candidates = block_sd.node_attractor_candidates(
-                            block_sd.root(), compute=True
-                        )
+                        if check_maa_exact:
+                            block_sd_candidates = block_sd.node_attractor_seeds(
+                                block_sd.root(), compute=True, symbolic_fallback=True
+                            )
+                        else:
+                            block_sd_candidates = block_sd.node_attractor_candidates(
+                                block_sd.root(), compute=True
+                            )
                         is_clean = len(block_sd_candidates) == 0
                     except RuntimeError:
                         is_clean = False

biobalm/_sd_attractors/attractor_candidates.py

@@ -19,6 +19,7 @@
 from biodivine_aeon import Bdd, AsynchronousGraph, BddVariable
 from biobalm.trappist_core import compute_fixed_point_reduced_STG
 from biobalm.symbolic_utils import state_list_to_bdd, valuation_to_state, state_to_bdd
+from biobalm.space_utils import intersect, is_subspace
 
 try:
     pint_available = True
@@ -122,6 +123,37 @@ def compute_attractor_candidates(
             sd.edge_stable_motif(node_id, s, reduced=True) for s in children
         ]
 
+    if node_data["skipped"]:
+        # For skip nodes, it does not holds that the successors are the maximal subspaces.
+        # This means that a skip node can intersect with some other SD node and that intersection
+        # is not a subset of one of its children. In such case, we can use this intersection
+        # to further simplify the attractor detection process.
+        total_skip_nodes_applied = 0
+        for n in sd.node_ids():
+            n_data = sd.node_data(n)
+            if is_subspace(node_space, n_data["space"]):
+                # This means that (in a fully expanded SD), `node` would be a (transitive)
+                # successor of `n`, which means that a result for `n` is "attractors in n
+                # that are not in node". Hence, we can't use it to reason about `node`.
+                # This is not a problem if the intersection of the two nodes is non-triviall,
+                # because that means they have common successors (and those should be
+                # solved separately), but the nodes themselves do not depend on each other.
+                continue
+            if n_data["attractor_candidates"] == [] or n_data["attractor_seeds"] == []:
+                # This will create a lot of duplicates, but it seems to be better than
+                # not doing it at all.
+                common_subspace = intersect(node_space, n_data["space"])
+                if common_subspace is not None:
+                    reduced_subspace: BooleanSpace = {
+                        k: v for k, v in common_subspace.items() if k not in node_space
+                    }
+                    child_motifs_reduced.append(reduced_subspace)
+                    total_skip_nodes_applied += 1
+        if sd.config["debug"]:
+            print(
+                f"[{node_id}] Extended child motifs with {total_skip_nodes_applied} skip-node intersections."
+            )
+
     # Indicates that this space is either minimal, or has no computed successors.
     # In either case, the space must contain at least one attractor.
     node_is_pseudo_minimal = len(child_motifs_reduced) == 0

biobalm/_sd_attractors/attractor_symbolic.py

@@ -14,6 +14,7 @@
     Reachability,
 )
 from biobalm.symbolic_utils import state_list_to_bdd
+from biobalm.space_utils import is_subspace, intersect
 from biobalm.types import BooleanSpace
 import biodivine_aeon
 import copy
@@ -48,16 +49,37 @@ def symbolic_attractor_fallback(
             s_space = sd.node_data(s)["space"]
             candidates = candidates.minus(sd.symbolic.mk_subspace(s_space))
 
-    fixed_variables = list(node_space.keys())
-    free_variables = [
-        v for v in sd.network.variable_names() if v not in fixed_variables
-    ]
+    if node_data["skipped"]:
+        # This is the same method that we applied to candidate states computation.
+        initial_size = candidates.cardinality()
+        for n in sd.node_ids():
+            n_data = sd.node_data(n)
+            if is_subspace(node_space, n_data["space"]):
+                continue
+            if n_data["attractor_candidates"] == [] or n_data["attractor_seeds"] == []:
+                # This will create a lot of duplicates, but it seems to be better than
+                # not doing it at all.
+                common_subspace = intersect(node_space, n_data["space"])
+                if common_subspace is not None:
+                    candidates = candidates.minus(
+                        sd.symbolic.mk_subspace(common_subspace)
+                    )
+        if sd.config["debug"]:
+            print(
+                f"[{node_id}] Simplified symbolic fallback candidates with skip nodes from {initial_size} to {candidates.cardinality()}."
+            )
+
+    # These should cover all cycles in the network, so transition-guided reduction
+    # only needs to consider these variables.
+    internal_nfvs = sd.node_percolated_nfvs(node_id)
 
     if sd.config["debug"]:
         print(f"[{node_id}] > Initial attractor candidates: {candidates}")
 
     candidates = Attractors.transition_guided_reduction(
-        sd.symbolic, candidates, free_variables
+        sd.symbolic,
+        candidates,
+        internal_nfvs,
     )
 
     if not sd.node_is_minimal(node_id) and not candidates.is_empty():