diff --git a/nfvsmotifs/SuccessionDiagram.py b/nfvsmotifs/SuccessionDiagram.py index 401893eb..a47ba9ea 100644 --- a/nfvsmotifs/SuccessionDiagram.py +++ b/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: diff --git a/nfvsmotifs/motif_avoidant.py b/nfvsmotifs/motif_avoidant.py index 7d7c5521..90dd1d8d 100644 --- a/nfvsmotifs/motif_avoidant.py +++ b/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,