Aeon 1.0

.gitignore

@@ -153,4 +153,7 @@ dmypy.json
 mole-*
 
 # Ignore benchmark runs.
-_run_*
+_run_*
+
+# Some weird temporary Z3 files.
+.z3-trace

balm/SuccessionDiagram.py

@@ -6,7 +6,7 @@
     from typing import Iterator
 
 import networkx as nx  # type: ignore
-from biodivine_aeon import BooleanNetwork
+from biodivine_aeon import AsynchronousGraph, BooleanNetwork
 
 from balm._sd_algorithms.compute_attractor_seeds import compute_attractor_seeds
 from balm._sd_algorithms.expand_attractor_seeds import expand_attractor_seeds
@@ -15,7 +15,7 @@
 from balm._sd_algorithms.expand_minimal_spaces import expand_minimal_spaces
 from balm._sd_algorithms.expand_source_SCCs import expand_source_SCCs
 from balm._sd_algorithms.expand_to_target import expand_to_target
-from balm.interaction_graph_utils import feedback_vertex_set
+from balm.interaction_graph_utils import cleanup_network, feedback_vertex_set
 from balm.petri_net_translation import network_to_petrinet
 from balm.space_utils import percolate_space, space_unique_key
 from balm.trappist_core import trappist
@@ -96,6 +96,7 @@ class SuccessionDiagram:
 
     __slots__ = (
         "network",
+        "symbolic",
         "petri_net",
         "nfvs",
         "dag",
@@ -104,7 +105,8 @@ class SuccessionDiagram:
 
     def __init__(self, network: BooleanNetwork):
         # Original Boolean network.
-        self.network = network
+        self.network = cleanup_network(network)
+        self.symbolic = AsynchronousGraph(self.network)
         # A Petri net representation of the original Boolean network.
         self.petri_net = network_to_petrinet(network)
         # Negative feedback vertex set.
@@ -133,7 +135,11 @@ def __getstate__(self) -> dict[str, str | nx.DiGraph | list[str] | dict[int, int
     def __setstate__(
         self, state: dict[str, str | nx.DiGraph | list[str] | dict[int, int]]
     ):
-        self.network = BooleanNetwork.from_aeon(str(state["network rules"]))
+        # In theory, the network should be cleaned-up at this point, but just in case...
+        self.network = cleanup_network(
+            BooleanNetwork.from_aeon(str(state["network rules"]))
+        )
+        self.symbolic = AsynchronousGraph(self.network)
         self.petri_net = cast(nx.DiGraph, state["petri net"])
         self.nfvs = cast(list[str], state["nfvs"])
         self.dag = cast(nx.DiGraph, state["G"])  # type: ignore
@@ -269,20 +275,16 @@ def find_node(self, node_space: BooleanSpace) -> int | None:
         if no such node exists in this succession diagram.
         """
         try:
-            key = space_unique_key(node_space, self.network)
+            key = space_unique_key(node_space, self.network) # throws IndexError
             if key in self.node_indices:
-                i = self.node_indices[key]
-                # This assertion could be violated if a user gives a node space
-                # that is not based on the same network as this succession
-                # diagram.
-                assert node_space == self.node_space(i)
-                return i
+                return self.node_indices[key]                
             else:
                 return None
-        except RuntimeError:
-            # If the user gives us a space that uses variables not used by this
-            # network, we should get an error that we can catch and report that
-            # no such space exists here.
+        except IndexError:
+            # If `space_unique_key` finds a variable that does not exist in this 
+            # `SuccessionDiagram`, it throws an `IndexError`. This can happen 
+            # for example if we are comparing two succession diagrams based on 
+            # completely different networks.
             return None
 
     def is_subgraph(self, other: SuccessionDiagram) -> bool:
@@ -586,7 +588,7 @@ def _expand_one_node(self, node_id: int):
         if DEBUG:
             print(f"[{node_id}] Expanding: {len(self.node_space(node_id))} fixed vars.")
 
-        if len(current_space) == self.network.num_vars():
+        if len(current_space) == self.network.variable_count():
             # This node is a fixed-point. Trappist would just
             # return this fixed-point again. No need to continue.
             if DEBUG:
@@ -632,9 +634,7 @@ def _ensure_node(self, parent_id: int | None, stable_motif: BooleanSpace) -> int
         considered to be zero (i.e. the node is the root).
         """
 
-        fixed_vars = percolate_space(
-            self.network, stable_motif, strict_percolation=False
-        )
+        fixed_vars = percolate_space(self.symbolic, stable_motif)
 
         key = space_unique_key(fixed_vars, self.network)
 

balm/_sd_algorithms/compute_attractor_seeds.py

@@ -2,7 +2,7 @@
 
 from typing import TYPE_CHECKING
 
-from balm.state_utils import state_list_to_bdd
+from balm.symbolic_utils import state_list_to_bdd
 
 if TYPE_CHECKING:
     from balm.SuccessionDiagram import SuccessionDiagram
@@ -32,7 +32,7 @@ def compute_attractor_seeds(
 
     node_space = sd.node_space(node_id)
 
-    if len(node_space) == sd.network.num_vars():
+    if len(node_space) == sd.network.variable_count():
         # This node is a fixed-point.
         return [node_space]
 
@@ -48,14 +48,16 @@ def compute_attractor_seeds(
     # We add the whole node space to the retain set because we know
     # 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)
+    retained_set = make_retained_set(sd.symbolic, sd.nfvs, node_space, child_spaces)
 
-    if len(retained_set) == sd.network.num_vars() and len(child_spaces) == 0:
+    if len(retained_set) == sd.network.variable_count() and len(child_spaces) == 0:
         # There is only a single attractor remaining here,
         # and its "seed" is the retained set.
         return [retained_set]
 
-    terminal_restriction_space = ~state_list_to_bdd(child_spaces)
+    terminal_restriction_space = state_list_to_bdd(
+        sd.symbolic.symbolic_context(), child_spaces
+    ).l_not()
 
     candidate_seeds = compute_fixed_point_reduced_STG(
         sd.petri_net,
@@ -73,7 +75,7 @@ def compute_attractor_seeds(
         return candidate_seeds
     else:
         attractors = detect_motif_avoidant_attractors(
-            sd.network,
+            sd.symbolic,
             sd.petri_net,
             candidate_seeds,
             terminal_restriction_space,

balm/_sd_algorithms/expand_attractor_seeds.py

@@ -70,7 +70,7 @@ def expand_attractor_seeds(sd: SuccessionDiagram, size_limit: int | None = None)
             # are not covered by the already expanded children.
 
             successor_space = sd.node_space(successors[-1])
-            retained_set = make_retained_set(sd.network, sd.nfvs, successor_space)
+            retained_set = make_retained_set(sd.symbolic, sd.nfvs, successor_space)
 
             avoid_or_none = [
                 intersect(successor_space, child) for child in expanded_motifs