attractors

completeness(primes: dict, update: str, max_output: int = 1000) → bool

The ASP and CTL model checking based algorithm for deciding whether the minimal trap spaces of a network are complete. The algorithm is discussed in Klarner2015(a). It splits the problem of deciding completeness into smaller subproblems by searching for so-called autonomous sets in the interaction graph of the network. If the minimal trap spaces of the corresponding restricted networks are complete then each of them defines a network reduction that is in turn subjected to a search for autonomous sets. The efficiency of the algorithm depends on the existence of small autonomous sets in the interaction graph, i.e., the existence of “hierarchies” rather than a single connected component.

Note

Completeness depends on the update strategy, i.e., the minimal trap spaces may be complete in the synchronous STG but not complete in the asynchronous STG or vice versa.

Note

The algorithm returns a counterexample, i.e., a state from which there is no path to one of the minimal trap spaces, if the minimal trap spaces are not complete.

Note

Each line that corresponds to a line of the pseudo code of Figure 3 in Klarner2015(a) is marked by a comment.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

returns:

  • answer: whether subspaces is complete in the STG defined by primes and update,

example:

>>> completeness(primes, "asynchronous")
False
completeness_naive(primes, update, trap_spaces)

The naive approach to deciding whether Trapspaces is complete, i.e., whether there is no attractor outside of Trapspaces. The approach is described and discussed in Klarner2015(a). It is decided by a single CTL query of the EF_oneof_subspaces. The state explosion problem limits this function to networks with around 40 variables. For networks with more variables (or a faster answer) use completeness_iterative.

Note

Completeness depends on the update strategy, i.e., a set of subspaces may be complete in the synchronous STG but not complete in the asynchronous STG or vice versa.

Note

A typical use case is to decide whether the minimal trap spaces of a network are complete.

Note

The subspaces of Trapspaces are in in fact not required to be a trap sets, i.e., it may contain arbitrary subspaces. If there are arbitrary subspaces then the semantics of the query is such that it checks whether each attractor intersects one of the subspaces.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • trap_spaces: list of subspaces in string or dict representation

returns:

  • answer: whether subspaces is complete in the STG defined by primes and update,

example:

>>> min_trap_spaces = trap_spaces(primes, "min")
>>> answer, counterexample = completeness_naive(primes, "asynchronous", min_trap_spaces)
>>> answer
True
completeness_naive_with_counterexample(primes: dict, update: str, trap_spaces: List[Union[dict, str]])

The naive approach to deciding whether Trapspaces is complete, i.e., whether there is no attractor outside of Trapspaces. The approach is described and discussed in Klarner2015(a). It is decided by a single CTL query of the EF_oneof_subspaces. The state explosion problem limits this function to networks with around 40 variables. For networks with more variables (or a faster answer) use completeness_iterative.

Note

Completeness depends on the update strategy, i.e., a set of subspaces may be complete in the synchronous STG but not complete in the asynchronous STG or vice versa.

Note

A typical use case is to decide whether the minimal trap spaces of a network are complete.

Note

The subspaces of Trapspaces are in in fact not required to be a trap sets, i.e., it may contain arbitrary subspaces. If there are arbitrary subspaces then the semantics of the query is such that it checks whether each attractor intersects one of the subspaces.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • Trapspaces: list of subspaces in string or dict representation

returns:

  • answer: whether subspaces is complete in the STG defined by primes and update,

  • counter_example: a state from which none of the subspaces is reachable (if answer is False)

example:

>>> mintspaces = trap_spaces(primes, "min")
>>> answer, counterexample = completeness_naive(primes, "asynchronous", mintspaces)
>>> answer
True
completeness_with_counterexample(primes: dict, update: str, max_output: int = 1000) -> (<class 'bool'>, typing.List[dict])

Performs the same steps as completeness but also returns a counterexample which is None if it does not exist. A counterexample of a completeness test is a state that can not reach one of the minimal trap spaces of primes.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

returns:

  • answer: whether subspaces is complete in the STG defined by primes and update,

  • counterexample: a state that can not reach one of the minimal trap spaces of primes or None if no counterexample exists

example:

>>> answer, counterexample = completeness_with_counterexample(primes, "asynchronous")
>>> answer
False
>>> state2str(counterexample)
10010111101010100001100001011011111111
compute_attractors(primes: dict, update: str, fname_json: Optional[str] = None, check_completeness: bool = True, check_faithfulness: bool = True, check_univocality: bool = True, max_output: int = 1000) → dict

computes all attractors of primes including information about completeness, univocality, faithfulness

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • fname_json: json file name to save result

  • check_completeness: enable completeness check

  • check_faithfulness: enable faithfulness check

  • check_univocality: enable univocality check

returns:

  • attractors: attractor data

example::
>>> attractors = compute_attractors(primes, update, "attractors.json")
compute_attractors_tarjan(stg: DiGraph)

Uses networkx.strongly_connected_components , i.e., Tarjan’s algorithm with Nuutila’s modifications, to compute the SCCs of stg and networkx.has_path to decide whether a SCC is reachable from another. Returns the attractors as lists of states.

arguments:

  • stg: state transition graph

returns:

  • steady_states: the steady states

  • cyclic_attractors: the cyclic attractors

example:

>>> bnet = ["x, !x&y | z",
...         "y, !x | !z",
...         "z, x&!y"]
>>> bnet = "\n".join(bnet)
>>> primes = bnet2primes(bnet)
>>> stg = primes2stg(primes, "asynchronous")
>>> steady_states, cyclic_attractors = compute_attractors_tarjan(stg)
>>> steady_states
["101","000"]
>>> cyclic_attractors
[{"111", "110"}, {"001", "011"}]
create_attractor_report(primes: dict, fname_txt: Optional[str] = None) → str

Creates an attractor report for the network defined by primes.

arguments:

  • primes: prime implicants

  • fname_txt: the name of the report file or None

returns:

  • txt: attractor report as text

example::
>>> create_attractor_report(primes, "report.txt")
faithfulness(primes: dict, update: str, trap_space: Union[dict, str]) → bool

The model checking approach for deciding whether trap_space is faithful, i.e., whether all free variables oscillate in all of the attractors contained in it, in the state transition graph defined by primes and update. The approach is described and discussed in Klarner2015(a). It is decided by a single CTL query of the pattern EF_all_unsteady and the random-walk-approach of the function random_walk.

Note

In the (very unlikely) case that the random walk does not end in an attractor state an exception will be raised.

Note

Faithfulness depends on the update strategy, i.e., a trapspace may be faithful in the synchronous STG but not faithful in the asynchronous STG or vice versa.

Note

A typical use case is to decide whether a minimal trap space is faithful.

Note

trap_space is in fact not required to be a trap set, i.e., it may be an arbitrary subspace. If it is an arbitrary subspace then the involved variables are artificially fixed to be constant.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • trap_space: a subspace

returns:

  • answer: whether trap_space is faithful in the STG defined by primes and update

example:

>>> mintspaces = compute_trap_spaces(primes, "min")
>>> x = mintspaces[0]
>>> faithfulness(primes, x)
True
faithfulness_with_counterexample(primes: dict, update: str, trap_space: dict) -> (<class 'bool'>, typing.List[dict])

Performs the same steps as faithfulness but also returns a counterexample which is None if it does not exist. A counterexample of a faithful test is a state that belongs to an attractor which has more fixed variables than there are in trap_space.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • trap_space: a subspace

returns:

  • answer: whether trap_space is faithful in the STG defined by primes and update

  • counter_example: a state that belongs to an attractor that does not oscillate in all free variables or None if no counterexample exists

example:

>>> mintspaces = compute_trap_spaces(primes, "min")
>>> x = mintspaces[0]
>>> faithfulness(primes, x)
True
find_attractor_state_by_randomwalk_and_ctl(primes: dict, update: str, initial_state: Union[dict, str] = {}, length: int = 0, attempts: int = 10) → dict

Attempts to find a state inside an attractor by the “long random walk” method, see Klarner2015(b) Sec. 3.2 for a formal definition. The method generates a random walk of length states, starting from a state defined by initial_state. If initial_state is a subspace then random_state will be used to draw a random state from inside it. The function then uses CTL model checking, i.e., check_primes, to decide whether the last state of the random walk is inside an attractor. If so it is returned, otherwise the process is repeated. If no attractor state has been found after Attempts many trials an exception is raised.

Note

The default value for length, namely length=0, will be replaced by:

length = 10*len(primes)

which proved sufficiently large in our computer experiments.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • initial_state: an initial state or subspace

  • length: length of random walk

  • attempts: number of attempts before exception is raised

returns:

  • attractor_state: a state that belongs to some attractor

  • raises Exception if no attractor state is found

example::
>>> find_attractor_state_by_randomwalk_and_ctl(primes, "asynchronous")
{"v1": 1, "v2": 1, "v3": 1}
intersection(*list_of_dicts)

each argument must be a list of subspaces (dicts):

>>> intersection([{"v1":1}], [{"v1":0}, {"v2":1, "v3":0}])
iterative_completeness_algorithm(primes: dict, update: str, compute_counterexample: bool, max_output: int = 1000) → Union[Tuple[bool, Optional[dict]], bool]

The iterative algorithm for deciding whether the minimal trap spaces are complete. The function is implemented by line-by-line following of the pseudo code algorithm given in “Approximating attractors of Boolean networks by iterative CTL model checking”, Klarner and Siebert 2015.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • compute_counterexample: whether to compute a counterexample

returns:

  • answer: whether subspaces is complete in the STG defined by primes and update,

  • counterexample: a state that can not reach one of the minimal trap spaces of primes or None if no counterexample exists

example:

>>> answer, counterexample = completeness_with_counterexample(primes, "asynchronous")
>>> answer
False
>>> state2str(counterexample)
10010111101010100001100001011011111111
read_attractors_json(fname: str) → dict

opens the attractor object

arguments:

  • fname: file name

returns:

  • attractors: json attractor data, see compute_attractors

example::
>>> attractors = read_attractors_json("attractors.json")
univocality(primes: dict, update: str, trap_space: Union[dict, str]) → bool

The model checking and random-walk-based method for deciding whether trap_space is univocal, i.e., whether there is a unique attractor contained in it, in the state transition graph defined by primes and update. The approach is described and discussed in Klarner2015(a). The function performs two steps: first it searches for a state that belongs to an attractor inside of trap_space using the random-walk-approach and the function random_walk, then it uses CTL model checking, specifically the pattern AGEF_oneof_subspaces, to decide if the attractor is unique inside trap_space.

Note

In the (very unlikely) case that the random walk does not end in an attractor state an exception will be raised.

Note

Univocality depends on the update strategy, i.e., a trapspace may be univocal in the synchronous STG but not univocal in the asynchronous STG or vice versa.

Note

A typical use case is to decide whether a minimal trap space is univocal.

Note

trap_space is in fact not required to be a trap set, i.e., it may be an arbitrary subspace. If it is an arbitrary subspace then the involved variables are artificially fixed to be constant.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • trap_space: a subspace

returns:

  • answer: whether trap_space is univocal in the STG defined by primes and update

example:

>>> mintspaces = compute_trap_spaces(primes, "min")
>>> x = mintrapspaces[0]
>>> univocality(primes, "asynchronous", x)
True
univocality_with_counterexample(primes: dict, update: str, trap_space: ~typing.Union[dict, str]) -> (<class 'bool'>, typing.List[dict])

Performs the same steps as univocality but also returns a counterexample which is None if it does not exist. A counterexample of a univocality test are two states that belong to different attractors.

arguments:

  • primes: prime implicants

  • update: the update strategy, one of “asynchronous”, “synchronous”, “mixed”

  • trap_space: a subspace

returns:

  • answer: whether trap_space is univocal in the STG defined by primes and update

  • counter_example: two states that belong to different attractors or None if no counterexample exists

example:

>>> mintspaces = compute_trap_spaces(primes, "min")
>>> trapspace = mintrapspaces[0]
>>> answer, counterex = univocality_with_counterexample(primes, trapspace, "asynchronous")
write_attractors_json(attractors: dict, fname_json: str)

saves the attractor object as a JSON file.

arguments:

  • attractors: json attractor data, see attractors_compute_json

  • fname_json: file name

example::
>>> save_attractor(attractors, "attractors.json")