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():