From fe53b80b17754ed9c7827cc7e8f0cf5f9e7ee1e4 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Fri, 6 Sep 2024 11:25:52 +0200
Subject: [PATCH 1/9] Formally introduce skip nodes with optimized attractor
 detection.

---
 .../_sd_algorithms/expand_minimal_spaces.py   |  42 +++++-
 .../_sd_algorithms/expand_source_blocks.py    |  12 +-
 .../_sd_attractors/attractor_candidates.py    |  32 +++++
 biobalm/_sd_attractors/attractor_symbolic.py  |  32 ++++-
 biobalm/succession_diagram.py                 | 132 ++++++++++++++++--
 biobalm/types.py                              |  20 +++
 6 files changed, 251 insertions(+), 19 deletions(-)

diff --git a/biobalm/_sd_algorithms/expand_minimal_spaces.py b/biobalm/_sd_algorithms/expand_minimal_spaces.py
index 0df78b7..c61e0c2 100644
--- a/biobalm/_sd_algorithms/expand_minimal_spaces.py
+++ b/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
diff --git a/biobalm/_sd_algorithms/expand_source_blocks.py b/biobalm/_sd_algorithms/expand_source_blocks.py
index 4ee440c..e0cf8a2 100644
--- a/biobalm/_sd_algorithms/expand_source_blocks.py
+++ b/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
diff --git a/biobalm/_sd_attractors/attractor_candidates.py b/biobalm/_sd_attractors/attractor_candidates.py
index 7c48297..ed70dd8 100644
--- a/biobalm/_sd_attractors/attractor_candidates.py
+++ b/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
diff --git a/biobalm/_sd_attractors/attractor_symbolic.py b/biobalm/_sd_attractors/attractor_symbolic.py
index a8d1e2c..17c634f 100644
--- a/biobalm/_sd_attractors/attractor_symbolic.py
+++ b/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, compute=True)
 
     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():
diff --git a/biobalm/succession_diagram.py b/biobalm/succession_diagram.py
index 0ee9505..966bb95 100644
--- a/biobalm/succession_diagram.py
+++ b/biobalm/succession_diagram.py
@@ -35,7 +35,12 @@
     network_to_petrinet,
     restrict_petrinet_to_subspace,
 )
-from biobalm.space_utils import percolate_network, percolate_space, space_unique_key
+from biobalm.space_utils import (
+    percolate_network,
+    percolate_space,
+    space_unique_key,
+    is_subspace,
+)
 from biobalm.trappist_core import trappist
 from biobalm.types import (
     BooleanSpace,
@@ -1223,6 +1228,7 @@ def expand_block(
         find_motif_avoidant_attractors: bool = True,
         size_limit: int | None = None,
         optimize_source_nodes: bool = True,
+        exact_attractor_detection: bool = False,
     ) -> bool:
         """
         Expand the succession diagram using the source block method.
@@ -1240,12 +1246,21 @@ def expand_block(
         attractor search and always produces a smaller succession diagram, but if you need to
         obtain a succession diagram where this does not happen (e.g. for testing), you can turn
         this off using `optimize_source_nodes`.
+
+        If `exact_attractor_detection` is selected, the method will use attractor seeds instead
+        of attractor candidates to check for motif-avoidant attractors. This means that the attractor
+        detection can take much longer. In particular, it will not expand the SD if it cannot detect
+        all attractors, meaning it can get "stuck". However, assuming you want to run full attractor
+        detection anyway, this might save you some time, as you won't need to re-run  the failed
+        candidate detection. (This is only relevant for models where the attractors are very
+        complex and the candidate state detection can fail with default settings)
         """
         return expand_source_blocks(
             self,
             find_motif_avoidant_attractors,
             size_limit=size_limit,
             optimize_source_nodes=optimize_source_nodes,
+            check_maa_exact=exact_attractor_detection,
         )
 
     def expand_bfs(
@@ -1301,7 +1316,10 @@ def expand_dfs(
         return expand_dfs(self, node_id, dfs_stack_limit, size_limit)
 
     def expand_minimal_spaces(
-        self, node_id: int | None = None, size_limit: int | None = None
+        self,
+        node_id: int | None = None,
+        size_limit: int | None = None,
+        skip_remaining: bool = False,
     ) -> bool:
         """
         Expands the succession diagram in a way that guarantees every minimal
@@ -1324,8 +1342,14 @@ def expand_minimal_spaces(
 
         Returns `True` if the expansion procedure terminated without exceeding
         the size limit.
+
+        If `skip_remaining` is set, any nodes that are not expanded by this procedure
+        are "skipped" with edges redirected to the corresponding minimal trap spaces
+        (see also `SuccessionDiagram.skip_remaining`). This is usually faster than
+        using `skip_remaining` directly, since the minimal trap spaces are only
+        computed once.
         """
-        return expand_minimal_spaces(self, node_id, size_limit)
+        return expand_minimal_spaces(self, node_id, size_limit, skip_remaining)
 
     def expand_attractor_seeds(self, size_limit: int | None = None) -> bool:
         """
@@ -1355,6 +1379,97 @@ def expand_to_target(
         """
         return expand_to_target(self, target, size_limit)
 
+    def skip_to_minimal(self, node_id: int) -> bool:
+        """
+        Skip the expansion of this node (see also `NodeData.skipped`) and add extra
+        edges that connect it directly to its minimal trap spaces. Returns `False`
+        if the node is already expanded.
+
+        Note that this method is relatively inefficient when applied to multiple
+        nodes repeatedly, as it has to recompute the minimal trap spaces for each node.
+        To turn multiple nodes into skip nodes, see also `skip_remaining`.
+        """
+
+        node = self.node_data(node_id)
+
+        if node["expanded"]:
+            return False
+
+        pn = self.node_percolated_petri_net(node_id, compute=True)
+        minimal_traps = trappist(
+            network=pn, problem="min", ensure_subspace=node["space"]
+        )
+
+        if len(minimal_traps) == 1 and minimal_traps[0] == node["space"]:
+            # This node is a minimal trap space
+            # and thus cannot be skipped.
+            node["expanded"] = True
+            return True
+
+        for m_trap in minimal_traps:
+            m_id = self._ensure_node(node_id, m_trap)
+            # Also expand the minimal trap space, since we know
+            # it has no successors.
+            m_data = self.node_data(m_id)
+            m_data["expanded"] = True
+
+        node["expanded"] = True
+        node["skipped"] = True
+
+        if self.config["debug"]:
+            print(f"[{node_id}] Added {len(minimal_traps)} skip edges.")
+
+        return True
+
+    def skip_remaining(self) -> int:
+        """
+        Apply `skip_to_minimal` to every node that is not expanded.
+
+        This is faster than calling the method individually if the number of
+        nodes is high since we can cache the minimal trap spaces.
+
+        Returns the number of created skip nodes.
+        """
+
+        pn = self.node_percolated_network(self.root(), compute=True)
+        minimal_traps = trappist(network=pn, problem="min")
+
+        if self.config["debug"]:
+            print(f"Skipping remaining nodes. Found {len(minimal_traps)} trap spaces.")
+
+        trap_with_id: list[tuple[int, BooleanSpace]] = []
+        for m_trap in minimal_traps:
+            m_id = self._ensure_node(None, m_trap)
+            m_data = self.node_data(m_id)
+            trap_with_id.append((m_id, m_trap))
+            # We can expand the minimal trap spaces since
+            # they don't have successors.
+            m_data["expanded"] = True
+
+        skipped_nodes = 0
+        for node_id in self.node_ids():
+            node = self.node_data(node_id)
+
+            if node["expanded"]:
+                continue
+
+            skip_edges = 0
+            for m_id, m_trap in trap_with_id:
+                if is_subspace(m_trap, node["space"]):
+                    self._ensure_edge(node_id, m_id, m_trap)
+                    skip_edges += 1
+
+            node["skipped"] = True
+            node["expanded"] = True
+            skipped_nodes += 1
+
+            if self.config["debug"]:
+                print(
+                    f"[{node_id}] Added {skipped_nodes} skip edges into minimal trap spaces."
+                )
+
+        return skipped_nodes
+
     def _update_node_depth(self, node_id: int, parent_id: int):
         """
         An internal method that updates the depth of a node based on a specific
@@ -1464,10 +1579,7 @@ def _expand_one_node(self, node_id: int):
             print(f"[{node_id}] Found sub-spaces: {len(sub_spaces)}")
 
         for sub_space in sub_spaces:
-            child_id = self._ensure_node(node_id, sub_space)
-
-            if self.config["debug"]:
-                print(f"[{node_id}] Created edge into node {child_id}.")
+            self._ensure_node(node_id, sub_space)
 
         # If everything else worked out, we can mark the node as expanded.
         node["expanded"] = True
@@ -1506,6 +1618,7 @@ def _ensure_node(self, parent_id: int | None, stable_motif: BooleanSpace) -> int
                 attractor_seeds=None,
                 attractor_sets=None,
                 parent_node=parent_id,
+                skipped=None,
             )
             self.node_indices[key] = child_id
         else:
@@ -1522,5 +1635,8 @@ def _ensure_edge(self, parent_id: int, child_id: int, stable_motif: BooleanSpace
         # TODO: It seems that there are some networks where the same child
         # can be reached through multiple stable motifs. Not sure how to
         # approach these... but this is probably good enough for now.
-        self.dag.add_edge(parent_id, child_id, motif=stable_motif)  # type: ignore
+        if not self.dag.has_edge(parent_id, child_id):  # type: ignore
+            self.dag.add_edge(parent_id, child_id, motif=stable_motif)  # type: ignore
+            if self.config["debug"]:
+                print(f"[{parent_id}] Created edge into node {child_id}.")
         self._update_node_depth(child_id, parent_id)
diff --git a/biobalm/types.py b/biobalm/types.py
index a610302..c941b7e 100644
--- a/biobalm/types.py
+++ b/biobalm/types.py
@@ -167,6 +167,26 @@ class NodeData(TypedDict):
     expanding its predecessors).
     """
 
+    skipped: bool | None
+    """
+    If `True`, indicates that the successors of this node are not the normal
+    maximal trap spaces, but rather some smaller trap spaces deeper in the
+    succession diagram. The only requirement is that all minimal trap spaces
+    that are reachable from this "skip node" are still reachable through
+    this modified set of successors (in the most basic form, the successors
+    can be the minimal trap spaces themselves).
+
+    For skip nodes, attractor detection still works, but can over-count
+    motif-avoidant attractors assuming the attractor intersects multiple
+    skip nodes. In other words, each attractor is still found, but it is
+    not necessarily true that its smallest trap space is discovered.
+    Nevertheless, if the network has no motif-avoidant attractors, the
+    result is always the same regardless of how many skip nodes are used.
+
+    A skip node is considered "expanded", since its outgoing edges are
+    computed.
+    """
+
 
 class SuccessionDiagramConfiguration(TypedDict):
     """

From 2c5a9e2ec31dc744080829857820344a2c133f19 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Fri, 6 Sep 2024 13:13:59 +0200
Subject: [PATCH 2/9] Some sort of bug in mk_dnf?

---
 biobalm/symbolic_utils.py | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/biobalm/symbolic_utils.py b/biobalm/symbolic_utils.py
index 0ae1852..e441226 100644
--- a/biobalm/symbolic_utils.py
+++ b/biobalm/symbolic_utils.py
@@ -73,7 +73,14 @@ def state_list_to_bdd(
         if isinstance(bdd_context, BddVariableSet)
         else bdd_context.bdd_variable_set()
     )
-    return bdd.mk_dnf(states)
+    # There seems to be some bug in the "mk_dnf" function that makes some
+    # input instances shockingly slow. I am switching back to the "normal"
+    # enumeration method for now.
+    result = bdd.mk_false()
+    for clause in states:
+        result = result.l_or(bdd.mk_conjunctive_clause(clause))
+    return result
+    # return bdd.mk_dnf(states)
 
 
 def function_eval(f: Bdd, state: BooleanSpace) -> Literal[0, 1] | None:

From 39268c60d334678f1f74c139b574f9535df3ad6c Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Fri, 6 Sep 2024 20:57:58 +0200
Subject: [PATCH 3/9] Reduce the amount of logging.

---
 biobalm/succession_diagram.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/biobalm/succession_diagram.py b/biobalm/succession_diagram.py
index 966bb95..e16c9b3 100644
--- a/biobalm/succession_diagram.py
+++ b/biobalm/succession_diagram.py
@@ -1637,6 +1637,6 @@ def _ensure_edge(self, parent_id: int, child_id: int, stable_motif: BooleanSpace
         # approach these... but this is probably good enough for now.
         if not self.dag.has_edge(parent_id, child_id):  # type: ignore
             self.dag.add_edge(parent_id, child_id, motif=stable_motif)  # type: ignore
-            if self.config["debug"]:
-                print(f"[{parent_id}] Created edge into node {child_id}.")
+            #if self.config["debug"]:
+            #    print(f"[{parent_id}] Created edge into node {child_id}.")
         self._update_node_depth(child_id, parent_id)

From d8d2d08a42eb5fe6632a78fe6832305c88098ba3 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 12:38:03 +0200
Subject: [PATCH 4/9] Update AEON.py

---
 pyproject.toml   | 2 +-
 requirements.txt | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/pyproject.toml b/pyproject.toml
index e89d704..0a547b9 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -6,7 +6,7 @@ readme = "README.md"
 license = { file = "LICENSE" }
 requires-python = ">=3.11"
 dependencies = [
-    'biodivine_aeon ==1.0.0a10',
+    'biodivine_aeon >=1.0.0',
     'clingo >=5.6.2',
     'networkx >=2.8.8',    
 ]
diff --git a/requirements.txt b/requirements.txt
index b104275..8a59fc5 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,4 +1,4 @@
-biodivine_aeon==1.0.0a10
+biodivine_aeon>=1.0.0
 clingo==5.6.2
 networkx==2.8.8
 pypint[pint]==1.6.2
\ No newline at end of file

From a6c4f676a2deefbb73ab4f7e92b916ef51da575c Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 12:54:08 +0200
Subject: [PATCH 5/9] Formatting.

---
 biobalm/succession_diagram.py | 2 --
 1 file changed, 2 deletions(-)

diff --git a/biobalm/succession_diagram.py b/biobalm/succession_diagram.py
index e16c9b3..2a2dd70 100644
--- a/biobalm/succession_diagram.py
+++ b/biobalm/succession_diagram.py
@@ -1637,6 +1637,4 @@ def _ensure_edge(self, parent_id: int, child_id: int, stable_motif: BooleanSpace
         # approach these... but this is probably good enough for now.
         if not self.dag.has_edge(parent_id, child_id):  # type: ignore
             self.dag.add_edge(parent_id, child_id, motif=stable_motif)  # type: ignore
-            #if self.config["debug"]:
-            #    print(f"[{parent_id}] Created edge into node {child_id}.")
         self._update_node_depth(child_id, parent_id)

From a3fc6b49bac7b394b59f090e41b9e229133bcbda Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 12:56:52 +0200
Subject: [PATCH 6/9] Fixed aeon bug.

---
 biobalm/symbolic_utils.py | 9 +--------
 pyproject.toml            | 2 +-
 2 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/biobalm/symbolic_utils.py b/biobalm/symbolic_utils.py
index e441226..0ae1852 100644
--- a/biobalm/symbolic_utils.py
+++ b/biobalm/symbolic_utils.py
@@ -73,14 +73,7 @@ def state_list_to_bdd(
         if isinstance(bdd_context, BddVariableSet)
         else bdd_context.bdd_variable_set()
     )
-    # There seems to be some bug in the "mk_dnf" function that makes some
-    # input instances shockingly slow. I am switching back to the "normal"
-    # enumeration method for now.
-    result = bdd.mk_false()
-    for clause in states:
-        result = result.l_or(bdd.mk_conjunctive_clause(clause))
-    return result
-    # return bdd.mk_dnf(states)
+    return bdd.mk_dnf(states)
 
 
 def function_eval(f: Bdd, state: BooleanSpace) -> Literal[0, 1] | None:
diff --git a/pyproject.toml b/pyproject.toml
index 0a547b9..edde318 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -6,7 +6,7 @@ readme = "README.md"
 license = { file = "LICENSE" }
 requires-python = ">=3.11"
 dependencies = [
-    'biodivine_aeon >=1.0.0',
+    'biodivine_aeon >=1.0.1',
     'clingo >=5.6.2',
     'networkx >=2.8.8',    
 ]

From ae4ff6889aeb3cbbecf5a2569a4b9112357a49fb Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 12:59:45 +0200
Subject: [PATCH 7/9] Typo.

---
 biobalm/_sd_attractors/attractor_candidates.py | 2 +-
 biobalm/succession_diagram.py                  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/biobalm/_sd_attractors/attractor_candidates.py b/biobalm/_sd_attractors/attractor_candidates.py
index ed70dd8..f49894c 100644
--- a/biobalm/_sd_attractors/attractor_candidates.py
+++ b/biobalm/_sd_attractors/attractor_candidates.py
@@ -124,7 +124,7 @@ def compute_attractor_candidates(
         ]
 
     if node_data["skipped"]:
-        # For skip nodes, it does not holds that the successors are the maximal subspaces.
+        # For skip nodes, it does not hold 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.
diff --git a/biobalm/succession_diagram.py b/biobalm/succession_diagram.py
index 2a2dd70..b67e6d9 100644
--- a/biobalm/succession_diagram.py
+++ b/biobalm/succession_diagram.py
@@ -1253,7 +1253,7 @@ def expand_block(
         all attractors, meaning it can get "stuck". However, assuming you want to run full attractor
         detection anyway, this might save you some time, as you won't need to re-run  the failed
         candidate detection. (This is only relevant for models where the attractors are very
-        complex and the candidate state detection can fail with default settings)
+        complex and the candidate state detection can fail with default settings).
         """
         return expand_source_blocks(
             self,

From 7d2f23d19d1d0473926ad804f62efcbf856ef41c Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 13:17:27 +0200
Subject: [PATCH 8/9] Add a skip node test.

---
 tests/succession_diagram_test.py | 53 ++++++++++++++++++++++++++++++--
 1 file changed, 50 insertions(+), 3 deletions(-)

diff --git a/tests/succession_diagram_test.py b/tests/succession_diagram_test.py
index 565456a..f61329d 100644
--- a/tests/succession_diagram_test.py
+++ b/tests/succession_diagram_test.py
@@ -2,6 +2,7 @@
 
 from biodivine_aeon import AsynchronousGraph, Attractors, BooleanNetwork
 
+import copy
 import biobalm
 import biobalm.succession_diagram
 from biobalm.succession_diagram import SuccessionDiagram
@@ -254,6 +255,13 @@ def test_attractor_detection(network_file: str):
     if not fully_expanded:
         return
 
+    # Partial succession diagrams
+    sd_min_partial = SuccessionDiagram(bn)
+    sd_min_partial.expand_minimal_spaces(size_limit=10, skip_remaining=True)
+    sd_block_partial = SuccessionDiagram(bn)
+    sd_block_partial.expand_block(size_limit=10)
+    sd_block_partial.skip_remaining()
+
     # Compute attractors in diagram nodes.
     # TODO: There will probably be a method that does this in one "go".
     nfvs_attractors: list[BooleanSpace] = []
@@ -265,12 +273,25 @@ def test_attractor_detection(network_file: str):
         if len(attr) > 0:
             nfvs_attractors += attr
 
+    min_partial_attractors: list[BooleanSpace] = []
+    for i in sd_min_partial.node_ids():
+        attr = sd_min_partial.node_attractor_seeds(i, compute=True)
+        if len(attr) > 0:
+            min_partial_attractors += attr
+
+    block_partial_attractors: list[BooleanSpace] = []
+    for i in sd_block_partial.node_ids():
+        attr = sd_block_partial.node_attractor_seeds(i, compute=True)
+        if len(attr) > 0:
+            block_partial_attractors += attr
+
     # Compute symbolic attractors using AEON.
-    symbolic_attractors = Attractors.attractors(stg, stg.mk_unit_colored_vertices())
+    symbolic_attractors_all = Attractors.attractors(stg, stg.mk_unit_colored_vertices())
 
     # Check that every "seed" returned by SuccessionDiagram appears in
     # some symbolic attractor, and that every symbolic attractor contains
     # at most one such "seed" state.
+    symbolic_attractors = copy.copy(symbolic_attractors_all)
     for seed in nfvs_attractors:
         symbolic_seed = stg.mk_subspace(seed)
         found = None
@@ -284,11 +305,37 @@ def test_attractor_detection(network_file: str):
 
         symbolic_attractors.pop(found)
 
-    print("Attractors:", len(nfvs_attractors))
-
     # All symbolic attractors must be covered by some seed at this point.
     assert len(symbolic_attractors) == 0
 
+    # Copy of the test above, but for the results from partially expanded diagrams.
+
+    symbolic_attractors = copy.copy(symbolic_attractors_all)
+    for seed in min_partial_attractors:
+        symbolic_seed = stg.mk_subspace(seed)
+        found = None
+
+        for i in range(len(symbolic_attractors)):
+            if symbolic_seed.is_subset(symbolic_attractors[i]):
+                found = i
+        assert found is not None
+
+        symbolic_attractors.pop(found)
+    assert len(symbolic_attractors) == 0
+
+    symbolic_attractors = copy.copy(symbolic_attractors_all)
+    for seed in block_partial_attractors:
+        symbolic_seed = stg.mk_subspace(seed)
+        found = None
+
+        for i in range(len(symbolic_attractors)):
+            if symbolic_seed.is_subset(symbolic_attractors[i]):
+                found = i
+        assert found is not None
+
+        symbolic_attractors.pop(found)
+    assert len(symbolic_attractors) == 0
+
 
 def test_attractor_expansion(network_file: str):
     # This test is similar to the "test attractor detection" function above, but

From 738c51524b0208b0128051a5461403394292c910 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 18 Sep 2024 15:07:18 +0200
Subject: [PATCH 9/9] Fix inconsistencies in trap space detection when node
 percolation happens in the root.

---
 .../_sd_algorithms/expand_minimal_spaces.py   |  2 ++
 biobalm/succession_diagram.py                 | 27 +++++++++++--------
 tests/succession_diagram_test.py              | 17 ++++++++++--
 3 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/biobalm/_sd_algorithms/expand_minimal_spaces.py b/biobalm/_sd_algorithms/expand_minimal_spaces.py
index c61e0c2..32515f7 100644
--- a/biobalm/_sd_algorithms/expand_minimal_spaces.py
+++ b/biobalm/_sd_algorithms/expand_minimal_spaces.py
@@ -28,6 +28,7 @@ def expand_minimal_spaces(
     node_space = sd.node_data(node_id)["space"]
 
     all_minimal_traps = trappist(network=pn, problem="min", ensure_subspace=node_space)
+    all_minimal_traps = [(node_space | x) for x in all_minimal_traps]
     # We don't need to duplicate the actual trap spaces, just the list.
     minimal_traps = copy.copy(all_minimal_traps)
 
@@ -53,6 +54,7 @@ def make_skip_node(
                 m_id = sd._ensure_node(node_id, m_trap)  # type: ignore
                 m_data = sd.node_data(m_id)
                 m_data["expanded"] = True
+                assert sd.node_is_minimal(m_id)
                 skip_edges += 1
 
         node["expanded"] = True
diff --git a/biobalm/succession_diagram.py b/biobalm/succession_diagram.py
index b67e6d9..d74f6e8 100644
--- a/biobalm/succession_diagram.py
+++ b/biobalm/succession_diagram.py
@@ -1319,7 +1319,7 @@ def expand_minimal_spaces(
         self,
         node_id: int | None = None,
         size_limit: int | None = None,
-        skip_remaining: bool = False,
+        skip_ignored: bool = False,
     ) -> bool:
         """
         Expands the succession diagram in a way that guarantees every minimal
@@ -1343,13 +1343,15 @@ def expand_minimal_spaces(
         Returns `True` if the expansion procedure terminated without exceeding
         the size limit.
 
-        If `skip_remaining` is set, any nodes that are not expanded by this procedure
+        If `skip_ignored` is set, any nodes that are not expanded by this procedure
         are "skipped" with edges redirected to the corresponding minimal trap spaces
         (see also `SuccessionDiagram.skip_remaining`). This is usually faster than
         using `skip_remaining` directly, since the minimal trap spaces are only
-        computed once.
+        computed once. However, note that if used with `size_limit`, nodes that
+        are not processed when `size_limit` is reached remain unprocessed
+        (i.e. it is not guaranteed that all nodes are either fully expanded or skipped).
         """
-        return expand_minimal_spaces(self, node_id, size_limit, skip_remaining)
+        return expand_minimal_spaces(self, node_id, size_limit, skip_ignored)
 
     def expand_attractor_seeds(self, size_limit: int | None = None) -> bool:
         """
@@ -1396,9 +1398,8 @@ def skip_to_minimal(self, node_id: int) -> bool:
             return False
 
         pn = self.node_percolated_petri_net(node_id, compute=True)
-        minimal_traps = trappist(
-            network=pn, problem="min", ensure_subspace=node["space"]
-        )
+        minimal_traps = trappist(network=pn, problem="min")
+        minimal_traps = [(node["space"] | x) for x in minimal_traps]
 
         if len(minimal_traps) == 1 and minimal_traps[0] == node["space"]:
             # This node is a minimal trap space
@@ -1432,7 +1433,9 @@ def skip_remaining(self) -> int:
         """
 
         pn = self.node_percolated_network(self.root(), compute=True)
+        root_space = self.node_data(self.root())["space"]
         minimal_traps = trappist(network=pn, problem="min")
+        minimal_traps = [root_space | x for x in minimal_traps]
 
         if self.config["debug"]:
             print(f"Skipping remaining nodes. Found {len(minimal_traps)} trap spaces.")
@@ -1463,10 +1466,12 @@ def skip_remaining(self) -> int:
             node["expanded"] = True
             skipped_nodes += 1
 
-            if self.config["debug"]:
-                print(
-                    f"[{node_id}] Added {skipped_nodes} skip edges into minimal trap spaces."
-                )
+            # At this point, all minimal traps must be expanded,
+            # hence we should never skip one.
+            assert not self.node_is_minimal(node_id)
+
+        if self.config["debug"]:
+            print(f"Skipped {skipped_nodes} nodes.")
 
         return skipped_nodes
 
diff --git a/tests/succession_diagram_test.py b/tests/succession_diagram_test.py
index f61329d..6d372d4 100644
--- a/tests/succession_diagram_test.py
+++ b/tests/succession_diagram_test.py
@@ -255,13 +255,26 @@ def test_attractor_detection(network_file: str):
     if not fully_expanded:
         return
 
-    # Partial succession diagrams
+    # Build partial succession diagrams.
     sd_min_partial = SuccessionDiagram(bn)
-    sd_min_partial.expand_minimal_spaces(size_limit=10, skip_remaining=True)
+    sd_min_partial.expand_minimal_spaces(size_limit=10, skip_ignored=True)
+    sd_min_partial.skip_remaining()
     sd_block_partial = SuccessionDiagram(bn)
     sd_block_partial.expand_block(size_limit=10)
     sd_block_partial.skip_remaining()
 
+    # Check that the minimal trap spaces match
+    for node in sd_min_partial.node_ids():
+        sd_id = sd.find_node(sd_min_partial.node_data(node)["space"])
+        assert sd_id is not None
+        assert sd.node_is_minimal(sd_id) == sd_min_partial.node_is_minimal(node)
+    for node in sd_block_partial.node_ids():
+        sd_id = sd.find_node(sd_block_partial.node_data(node)["space"])
+        assert sd_id is not None
+        assert sd.node_is_minimal(sd_id) == sd_block_partial.node_is_minimal(node)
+    assert len(sd.minimal_trap_spaces()) == len(sd_min_partial.minimal_trap_spaces())
+    assert len(sd.minimal_trap_spaces()) == len(sd_block_partial.minimal_trap_spaces())
+
     # Compute attractors in diagram nodes.
     # TODO: There will probably be a method that does this in one "go".
     nfvs_attractors: list[BooleanSpace] = []