Merge pull request #70 from jcrozum/optimize-preprocessing-ssf

Optimize preprocessing ssf

nfvsmotifs/SuccessionDiagram.py

@@ -13,6 +13,7 @@
 from nfvsmotifs.petri_net_translation import network_to_petrinet
 from nfvsmotifs.space_utils import percolate_space
 from nfvsmotifs.terminal_restriction_space import get_terminal_restriction_space
+from nfvsmotifs.pyeda_utils import aeon_to_pyeda
 from nfvsmotifs.trappist_core import compute_fixed_point_reduced_STG, trappist
 
 # Enables helpful "progress" messages.
@@ -306,21 +307,55 @@ def expand_attractors(self, node_id: int) -> list[dict[str, int]]:
             # This node is a fixed-point.
             self.attractors[node_id] = [node_space]
             return [node_space]
-
-        # Fix everything in the NFVS to zero, as long as
-        # it isn't already fixed by our `node_space`.
-        #
-        # 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.
+
+        child_spaces = [
+            self.node_space(child) for child in self.G.successors(node_id)  # type: ignore
+        ]
+
+        # Initially, the retained set only contains the fixed values from the 
+        # current node space (this elimiantes unnecessary Petri net transitions
+        # for values which we already proved are constant).
+        # 
+        # In the following code, we then extend the retained set based on the model's NFVS
+        # and the current child spaces. 
         retained_set = node_space.copy()
+
+
+        # First, if there are any child spaces present, we extend the retained set with the 
+        # values from the one that has the least amount of fixed variables shared with the NFVS.
+        if len(child_spaces) > 0:
+            # Find the child space that has the fewest nodes in common with the NFVS:
+            least_common_child_space = child_spaces[0]
+            least_common_nodes = len(set(least_common_child_space) & set(self.nfvs))
+            for child_space in child_spaces:
+                common_nodes = len(set(child_space) & set(self.nfvs))
+                if common_nodes < least_common_nodes:
+                    least_common_nodes = common_nodes
+                    least_common_child_space = child_space
+
+            for x in least_common_child_space:
+                if (x not in retained_set) and (x in self.nfvs):
+                    retained_set[x] = least_common_child_space[x]
+
+        # Then, set the remaining NFVS variables based on the majority output value in the update 
+        # function of the relevant variable.
         for x in self.nfvs:
-            if x not in retained_set:
+            if x in retained_set:
+                continue
+
+            aeon_fx = self.network.get_update_function(x)
+            pyeda_fx = aeon_to_pyeda(aeon_fx)
+            input_count = len(list(pyeda_fx.support))
+
+            half_count = pow(2, input_count - 1)
+            sat_count = pyeda_fx.satisfy_count()
+
+            if sat_count > half_count:
+                retained_set[x] = 1
+            else:
                 retained_set[x] = 0
 
-        child_spaces = [
-            self.node_space(child) for child in self.G.successors(node_id)  # type: ignore
-        ]
+
 
         if len(retained_set) == self.network.num_vars() and len(child_spaces) == 0:
             # There is only a single attractor remaining here,
@@ -384,6 +419,7 @@ def expand_attractors(self, node_id: int) -> list[dict[str, int]]:
                 candidate_seeds,
                 terminal_restriction_space,
                 max_iterations=1000,
+                is_in_an_mts=len(child_spaces) == 0,
             )
 
         if len(attractors) > 0:

nfvsmotifs/motif_avoidant.py

@@ -63,6 +63,7 @@ def detect_motif_avoidant_attractors(
         terminal_restriction_space,
         max_iterations,
         ensure_subspace=ensure_subspace,
+        is_in_an_mts=is_in_an_mts
     )
 
     if len(candidates) == 0:
@@ -80,6 +81,7 @@ def _preprocess_candidates(
     terminal_restriction_space: BinaryDecisionDiagram,
     max_iterations: int,
     ensure_subspace: dict[str, int] | None = None,
+    is_in_an_mts: bool = False
 ) -> list[dict[str, int]]:
     """
     A fast but incomplete method for eliminating spurious attractor candidates.
@@ -110,60 +112,86 @@ def _preprocess_candidates(
             continue
         var_name = network.get_variable_name(varID)
         variables.append(var_name)
-        function_expression = network.get_update_function(varID)
-        function_bdd: BinaryDecisionDiagram = expr2bdd(
-            aeon_to_pyeda(function_expression)
-        )
-
+        function_expression = network.get_update_function(varID) 
+        function_bdd = expr2bdd(aeon_to_pyeda(function_expression))
         update_functions[var_name] = function_bdd
 
-    # symbolic_candidates = state_list_to_bdd(candidates)
-    symbolic_candidates = deepcopy(candidates)
-    filtered_candidates: list[dict[str, int]] = []
-    for state in candidates:
-        # state_bdd = state_to_bdd(state)
-
-        # Remove state from the symbolic set. If we can prove that is
-        # is not an attractor, we will put it back.
-        # symbolic_candidates = symbolic_candidates & ~state_bdd
-        symbolic_candidates = remove_state_from_dnf(symbolic_candidates, state)
-
-        # A copy of the state that we can overwrite.
-        simulation = state.copy()
-        is_valid_candidate = True
-        for _ in range(max_iterations):
-            # Advance all variables by one step in random order.
-            random.shuffle(variables)
-            for var in variables:
-                step = function_eval(update_functions[var], simulation)
-                assert step is not None
-                simulation[var] = step
-
-            # if function_is_true(symbolic_candidates, simulation):
-            if dnf_function_is_true(symbolic_candidates, simulation):
-                # The state can reach some other state in the candidate
-                # set. This does not mean it cannot be an attractor, but
-                # it means it is sufficient to keep considering the other
-                # candidate.
-                is_valid_candidate = False
+    # A random generator initialized with a fixed seed. Ensures simulation
+    # is randomized but deterministic.
+    generator = random.Random(1234567890)
+
+    # Use stochastic simulation to prune the set of candidate states.
+    # We use different simulation approach depending on whether this space
+    # is a minimal trap or not. In previous work, this was shown to work
+    # well, but in the future we need to better document the resoning
+    # behind these two algorithms.
+    if is_in_an_mts == False:
+        # Copy is sufficient because we won't be modifying the states within the set.
+        candidates_dnf = candidates.copy()
+        filtered_candidates = []
+        for state in candidates:                        
+            # Remove the state from the candidates. If we can prove that is
+            # is not an attractor, we will put it back.
+            candidates_dnf = remove_state_from_dnf(candidates_dnf, state)
+
+            simulation = state.copy()   # A copy of the state that we can overwrite.
+            is_valid_candidate = True
+            for _ in range(max_iterations):
+                # Advance all variables by one step in random order.
+                generator.shuffle(variables)
+                for var in variables:
+                    step = function_eval(update_functions[var], simulation)
+                    assert step is not None
+                    simulation[var] = step
+
+                if dnf_function_is_true(candidates_dnf, simulation):
+                    # The state can reach some other state in the candidate
+                    # set. This does not mean it cannot be an attractor, but
+                    # it means it is sufficient to keep considering 
+                    # the remaining candidates.
+                    is_valid_candidate = False
+                    break
+
+                if not function_is_true(terminal_restriction_space, simulation):
+                    # The state can reach some other state outside of the
+                    # terminal restriction space, which means it cannot be
+                    # a motif avoidant attractor in this subspace.
+                    is_valid_candidate = False
+                    break
+
+            if is_valid_candidate:
+                # If we cannot rule out the candidate, we have to put it back
+                # into the candidate set.
+                candidates_dnf.append(state)
+                filtered_candidates.append(state)
+
+        return filtered_candidates
+    else:
+        filtered_candidates = []
+        for i in range(max_iterations):
+            generator.shuffle(variables)                        
+            candidates_dnf = candidates.copy()
+            filtered_candidates = []
+
+            for state in candidates:
+                candidates_dnf = remove_state_from_dnf(candidates_dnf, state)
+
+                simulation = state.copy()
+                for var in variables:
+                    step = function_eval(update_functions[var], simulation)
+                    assert step is not None
+                    simulation[var] = step
+
+                if not dnf_function_is_true(candidates_dnf, simulation):
+                    candidates_dnf.append(simulation)
+                    filtered_candidates.append(simulation)
+
+            if len(filtered_candidates) <= 1:
                 break
 
-            if not function_is_true(terminal_restriction_space, simulation):
-                # The state can reach some other state outside of the
-                # terminal restriction space, which means it cannot be
-                # a motif avoidant attractor in this subspace.
-                is_valid_candidate = False
-                break
-
-        if is_valid_candidate:
-            # If we cannot rule out the candidate, we can put it back
-            # into candidate set.
-            # symbolic_candidates = symbolic_candidates | state_bdd
-            symbolic_candidates.append(state)
-            filtered_candidates.append(state)
-
-    return filtered_candidates
+            candidates = filtered_candidates
 
+        return filtered_candidates
 
 def _filter_candidates(
     petri_net: DiGraph,