biodivine_aeon

AEON.py is a Python library for working with Boolean networks. It supports a wide range of features, including symbolic representation of network dynamics. More general information is available on GitHub.

To explore the library documentation, you can start with one of the core data classes: RegulatoryGraph, BooleanNetwork and AsynchronousGraph. Alternatively, to learn more about the available algorithms, you may want to look at Attractors, TrapSpaces, FixedPoints, Classification, or Control.

View Source

  1from typing import Literal, TypedDict, Mapping, Union, Optional
  2
  3# Notes on Python version updates:
  4#  - TODO: If we ever move to 3.10, we can start using `TypeAlias`.
  5#  - TODO: If we ever move to 3.10, we can start using `|` instead of `Union` (and stop using `Optional`).
  6#  - TODO: If we ever move to 3.11, we can start using `Generic` and `TypedDict` together.
  7#  - TODO: If we ever move to 3.12, we can start using `type` instead of `TypeAlias`.
  8#  - TODO: If we ever move to 3.12, we can start using special syntax for generics.
  9
 10# Counterintuitively, these two lines should actually reexport the native PyO3 module here. But it is a bit of a hack
 11# which does not work super reliably. Refer to the PyO3 guide for how this should be handled if it stops working.
 12import biodivine_aeon
 13from .biodivine_aeon import *
 14
 15# Replace module-level documentation.
 16__doc__ = biodivine_aeon.__doc__
 17
 18# The "__all__" list allows us to control what items are exported from the module. It has to be built as a single
 19# assignment, because the interpreter will cache its contents (i.e. subsequent updates are not taken into account).
 20# We include all Python-only types that we have in this file, plus all classes from the native module as long as
 21# they do not start with an underscore. We can also use this to influence the order in which items appear
 22# in documentation.
 23assert hasattr(biodivine_aeon, "__all__")
 24__all__ = [
 25              'LOG_NOTHING',
 26              'LOG_ESSENTIAL',
 27              'LOG_VERBOSE',
 28              'LOG_LEVEL',
 29              'BddVariableType',
 30              'VariableIdType',
 31              'ParameterIdType',
 32              'BoolType',
 33              'SignType',
 34              'BinaryOperator',
 35              'TemporalBinaryOperator',
 36              'TemporalUnaryOperator',
 37              'HybridOperator',
 38              'PhenotypeOscillation',
 39              'BoolClauseType',
 40              'BoolExpressionType',
 41              'Regulation',
 42              'IdRegulation',
 43              'NamedRegulation',
 44          ] + [x for x in biodivine_aeon.__all__ if not x.startswith("_")]
 45
 46LOG_NOTHING: Literal[0] = 0
 47"""
 48No progress messages are printed.
 49"""
 50LOG_ESSENTIAL: Literal[1] = 1
 51"""
 52Progress messages are printed only for operations of "non-trivial" complexity.
 53"""
 54LOG_VERBOSE: Literal[2] = 2
 55"""
 56All progress messages are printed.
 57"""
 58
 59LOG_LEVEL: Literal[0, 1, 2] = biodivine_aeon.LOG_LEVEL
 60"""
 61A global variable which specifies what logging messages should be printed to the standard output. These are mainly 
 62used to communicate progress during long-running algorithms. I.e. they typically do not communicate any new
 63errors or warnings, just a rough estimate of resources being used. Note that these messages introduce some overhead
 64into every algorithm. While we try to reduce this overhead as much as possible, especially `LOG_VERBOSE` can have
 65measurable impact in shorter computations. For longer computations, the overhead should tend towards zero. 
 66
 67 - `LOG_NOTHING`: No logging messages are printed. 
 68 - `LOG_ESSENTIAL`: Logging messages are printed when resource 
 69 consumption exceeds what is considered "trivial" in the context of a particular algorithm. 
 70 - `LOG_VERBOSE`: Prints all progress messages. This setting is useful for in-depth comparisons between algorithms, 
 71 but can be overwhelming under normal circumstances.
 72   
 73The default value is `LOG_NOTHING`. 
 74"""
 75
 76BddVariableType = Union[BddVariable, str]
 77"""
 78You can typically refer to a `Bdd` variable using its `BddVariable` ID object,
 79or you can use a "raw" `str` name. However, using names instead of IDs in frequently
 80running code incurs a performance penalty.
 81"""
 82
 83VariableIdType = Union[VariableId, str]
 84"""
 85You can typically refer to a network variable using its `VariableId` typed index,
 86or you can use a "raw" `str` name. However, using names instead of IDs in frequently
 87running code incurs a performance penalty.
 88"""
 89
 90ParameterIdType = Union[ParameterId, str]
 91"""
 92You can typically refer to a network parameter using its `ParameterId` typed index,
 93or you can use a "raw" `str` name. However, using names instead of IDs in frequently
 94running code incurs a performance penalty.
 95"""
 96
 97BoolType = Union[bool, int]
 98"""
 99Most methods can also accept `0`/`1` wherever `False`/`True` would be typically required.
100
101 > Note that `typing.Literal` is not used here due to how it behaves when typechecking in mappings/collections.
102"""
103
104SignType = Union[bool, Literal["positive", "+", "negative", "-"]]
105"""
106Sign is used in the context of regulatory networks to indicate positive/negative interaction,
107but can be also used for more general graph concepts, like positive/negative cycle.
108"""
109
110BinaryOperator = Literal["and", "or", "imp", "iff", "xor"]
111"""
112Lists the supported Boolean binary operators.
113"""
114
115TemporalBinaryOperator = Literal["exist_until", "all_until", "exist_weak_until", "all_weak_until"]
116"""
117List of temporal binary operators supported by the HCTL model checker.
118"""
119
120TemporalUnaryOperator = Literal["exist_next", "all_next", "exist_future", "all_future", "exist_global", "all_global"]
121"""
122List of temporal unary operators supported by the HCTL model checker.
123"""
124
125HybridOperator = Literal["exists", "forall", "bind", "jump"]
126"""
127List of hybrid quantifiers supported by the HCTL model checker.
128"""
129
130PhenotypeOscillation = Literal["required", "allowed", "forbidden"]
131"""
132The possible modes of oscillation in a phenotype set:
133 - `required`: To satisfy the phenotype, an attractor must visit the phenotype set intermittently
134 (i.e. it cannot be proper subset).
135 - `forbidden`: To satisfy the phenotype, an attractor must fully reside in the phenotype set.
136 - `allowed`: To satisfy the phenotype, an attractor must intersect the phenotype set, but it does not matter whether
137 it is fully contained in it or simply visits it intermittently.
138"""
139
140BoolClauseType = Union[BddPartialValuation, BddValuation, Mapping[str, BoolType], Mapping[BddVariable, BoolType]]
141"""
142A Boolean clause represents a collection of literals. This can be either done through one of the valuation types, 
143or through a regular dictionary. However, any representation other than `BddPartialValuation` incurs a performance
144penalty due to conversion.
145"""
146
147BoolExpressionType = Union[BooleanExpression, str]
148"""
149A `BooleanExpression` can be typically also substituted with its "raw" string representation. However, this
150requires the expression to be repeatedly parsed whenever used and is thus slower and more error prone.
151"""
152
153
154# IDT = TypeVar('IDT', covariant=True)
155# class Regulation(TypedDict, Generic[IDT]):
156#     source: IDT
157#     target: IDT
158#     sign: Optional[SignType]
159#     essential: BoolType
160#     """
161#     A typed dictionary that stores data about a single regulation. Parametrized by an "identifier type" which 
162#     can be either `str` or `VariableId`.
163
164#     Typically both `str` and `VariableId` are accepted as inputs, but only `VariableId` is provided as output.
165
166#     For backwards compatibility purposes, the `sign` key is also equivalent to `monotonicity` and `essential`
167#     is equivalent to `observable`. However, we do not include this in the type hints to discourage the
168#     usage of these deprecated dictionary keys.
169#     """
170
171class IdRegulation(TypedDict):
172    source: VariableId
173    target: VariableId
174    sign: Optional[SignType]
175    essential: BoolType
176    """
177    See `Regulation` type alias.
178    """
179
180
181class NamedRegulation(TypedDict):
182    source: str
183    target: str
184    sign: Optional[SignType]
185    essential: BoolType
186    """
187    See `Regulation` type alias.
188    """
189
190
191Regulation = Union[IdRegulation, NamedRegulation]
192"""
193A typed dictionary that stores data about a single regulation. Parametrized by an "identifier type" which 
194can be either `str` or `VariableId`.
195    
196Typically both `str` and `VariableId` are accepted as inputs, but only `VariableId` is provided as output.
197    
198For backwards compatibility purposes, the `sign` key is also equivalent to `monotonicity` and `essential`
199is equivalent to `observable`. However, we do not include this in the type hints to discourage the
200usage of these deprecated dictionary keys.
201
202 > For backwards compatibility, the type is currently not generic, but provided as two separate aliases.
203"""

LOG_NOTHING: Literal[0] = 0

No progress messages are printed.

LOG_ESSENTIAL: Literal[1] = 1

Progress messages are printed only for operations of "non-trivial" complexity.

LOG_VERBOSE: Literal[2] = 2

All progress messages are printed.

LOG_LEVEL: Literal[0, 1, 2] = 0

A global variable which specifies what logging messages should be printed to the standard output. These are mainly used to communicate progress during long-running algorithms. I.e. they typically do not communicate any new errors or warnings, just a rough estimate of resources being used. Note that these messages introduce some overhead into every algorithm. While we try to reduce this overhead as much as possible, especially LOG_VERBOSE can have measurable impact in shorter computations. For longer computations, the overhead should tend towards zero.

LOG_NOTHING: No logging messages are printed.
LOG_ESSENTIAL: Logging messages are printed when resource consumption exceeds what is considered "trivial" in the context of a particular algorithm.
LOG_VERBOSE: Prints all progress messages. This setting is useful for in-depth comparisons between algorithms, but can be overwhelming under normal circumstances.

The default value is LOG_NOTHING.

BddVariableType = typing.Union[BddVariable, str]

You can typically refer to a Bdd variable using its BddVariable ID object, or you can use a "raw" str name. However, using names instead of IDs in frequently running code incurs a performance penalty.

VariableIdType = typing.Union[VariableId, str]

You can typically refer to a network variable using its VariableId typed index, or you can use a "raw" str name. However, using names instead of IDs in frequently running code incurs a performance penalty.

ParameterIdType = typing.Union[ParameterId, str]

You can typically refer to a network parameter using its ParameterId typed index, or you can use a "raw" str name. However, using names instead of IDs in frequently running code incurs a performance penalty.

BoolType = typing.Union[bool, int]

Most methods can also accept 0/1 wherever False/True would be typically required.

Note that typing.Literal is not used here due to how it behaves when typechecking in mappings/collections.

SignType = typing.Union[bool, typing.Literal['positive', '+', 'negative', '-']]

Sign is used in the context of regulatory networks to indicate positive/negative interaction, but can be also used for more general graph concepts, like positive/negative cycle.

BinaryOperator = typing.Literal['and', 'or', 'imp', 'iff', 'xor']

Lists the supported Boolean binary operators.

TemporalBinaryOperator = typing.Literal['exist_until', 'all_until', 'exist_weak_until', 'all_weak_until']

List of temporal binary operators supported by the HCTL model checker.

TemporalUnaryOperator = typing.Literal['exist_next', 'all_next', 'exist_future', 'all_future', 'exist_global', 'all_global']

List of temporal unary operators supported by the HCTL model checker.

HybridOperator = typing.Literal['exists', 'forall', 'bind', 'jump']

List of hybrid quantifiers supported by the HCTL model checker.

PhenotypeOscillation = typing.Literal['required', 'allowed', 'forbidden']

The possible modes of oscillation in a phenotype set:

required: To satisfy the phenotype, an attractor must visit the phenotype set intermittently (i.e. it cannot be proper subset).
forbidden: To satisfy the phenotype, an attractor must fully reside in the phenotype set.
allowed: To satisfy the phenotype, an attractor must intersect the phenotype set, but it does not matter whether it is fully contained in it or simply visits it intermittently.

BoolClauseType = typing.Union[BddPartialValuation, BddValuation, typing.Mapping[str, typing.Union[bool, int]], typing.Mapping[BddVariable, typing.Union[bool, int]]]

A Boolean clause represents a collection of literals. This can be either done through one of the valuation types, or through a regular dictionary. However, any representation other than BddPartialValuation incurs a performance penalty due to conversion.

BoolExpressionType = typing.Union[BooleanExpression, str]

A BooleanExpression can be typically also substituted with its "raw" string representation. However, this requires the expression to be repeatedly parsed whenever used and is thus slower and more error prone.

Regulation = typing.Union[IdRegulation, NamedRegulation]

A typed dictionary that stores data about a single regulation. Parametrized by an "identifier type" which can be either str or VariableId.

Typically both str and VariableId are accepted as inputs, but only VariableId is provided as output.

For backwards compatibility purposes, the sign key is also equivalent to monotonicity and essential is equivalent to observable. However, we do not include this in the type hints to discourage the usage of these deprecated dictionary keys.

For backwards compatibility, the type is currently not generic, but provided as two separate aliases.

class IdRegulation(typing.TypedDict): View Source

172class IdRegulation(TypedDict):
173    source: VariableId
174    target: VariableId
175    sign: Optional[SignType]
176    essential: BoolType
177    """
178    See `Regulation` type alias.
179    """

source: VariableId

target: VariableId

sign: Union[bool, Literal['positive', '+', 'negative', '-'], NoneType]

essential: Union[bool, int]

See Regulation type alias.

Inherited Members

builtins.dict: get; setdefault; pop; popitem; keys; items; values; update; fromkeys; clear; copy

class NamedRegulation(typing.TypedDict): View Source

182class NamedRegulation(TypedDict):
183    source: str
184    target: str
185    sign: Optional[SignType]
186    essential: BoolType
187    """
188    See `Regulation` type alias.
189    """

source: str

target: str

sign: Union[bool, Literal['positive', '+', 'negative', '-'], NoneType]

essential: Union[bool, int]

See Regulation type alias.

Inherited Members

builtins.dict: get; setdefault; pop; popitem; keys; items; values; update; fromkeys; clear; copy

class Bdd:

BDD (binary decision diagram) is an acyclic, directed graph which is used to represent a Boolean function. BDDs can be used to efficiently represent large sets of states, functions, or spaces.

Bdd(ctx, data)

Bdd(valuation: Union[BddValuation, BddPartialValuation])

Bdd(ctx: BddVariableSet, data: Union[bytes, str])

A Bdd can be created as:

A conjunction of literals defined by a BddValuation or a BddPartialValuation.
Deserialization of an object created with Bdd.data_string() or Bdd.data_bytes().

When deserializing, a BddVariableSet has to be provided to interpret individual BDD variables.

def data_string(self) -> str:

Convert this Bdd into a serialized str format that can be read using the Bdd constructor.

def data_bytes(self) -> bytes:

Convert this Bdd into a serialized bytes format that can be read using the Bdd constructor.

def to_dot(self, zero_pruned: bool = True) -> str:

Produce a graphviz-compatible .dot representation of the underlying graph. If zero_pruned is set, edges leading to the 0 terminal are omitted for clarity.

You can use this in Jupyter notebooks to visualize the BDD:

bdd = ...

import graphviz
graphviz.Source(bdd.to_dot())

def to_expression(self) -> BooleanExpression:

Produce a BooleanExpression which is logically equivalent to the function represented by this Bdd.

The format uses an and-or expansion of the function graph, hence it is not very practical for complicated Bdd objects.

def to_dnf( self, optimize: bool = True, size_limit: Optional[int] = None) -> list[BddPartialValuation]:

Build a list of BddPartialValuation objects that represents a disjunctive normal form of this Boolean function.

When optimize is set to True, the method dynamically optimizes the BDD to obtain a smaller DNF. This process can be non-trivial for large BDDs. However, for such BDDs, we usually can't enumerate the full DNF anyway, hence the optimization is enabled by default. When optimize is set to False, the result should be equivalent to the actual canonical clauses of this BDD as reported by Bdd.clause_iterator.

Limitations

At the moment, the reduced variable cannot have a self-regulation. If such a variable is targeted with reduction, the function throws a RuntimeError. If a variable is inlined into a missing function, the function is given a name as a new parameter, and the variable is inlined into this new parameter function.

Note that variables that don't regulate anything (outputs) are simply removed by this reduction. However, this is correct behaviour, just not super intuitive.

Also note that because the set of variables is different between this and the resulting BooleanNetwork, any VariableId that is valid in this network is not valid in the resulting network.

Logical parameters

Finally, note the set of admissible parameter instantiations (interpretations of uninterpreted functions) can change between the original and the reduced model. The reason for this is the same as in the example of a "logically inconsistent" system described above. For example, consider a -> b and b -> c, but also a -| c. Then, let's have f_b = f(a) and f_c = b & !a. Then f(a) = a is the only admissible interpretation of f. However, suppose we inline variable b, obtaining f_c = f(a) & !a with regulation a -? c (because a -> b -> c and a -| c in the original system). Then f can actually be false, a, or !a.

This does not mean you cannot use reduction on systems with uninterpreted functions at all, but be careful about the new meaning of the static constraints on these functions.

def to_graph(self) -> RegulatoryGraph:

Return a copy of the underlying RegulatoryGraph for this BooleanNetwork.

def from_bnet(file_contents: str, repair_graph: bool = False) -> BooleanNetwork:

Try to load a Boolean network from the contents of a .bnet model file.

Note that this is currently only a "best effort" implementation, and you may encounter unsupported .bnet models.

We also support some features that .bnet does not, in particular, you can use Boolean constants (true/false). However, there are other things that we do not support, since .bnet can essentially use R syntax to define more complex functions, but in practice this is not used anywhere.

Note that .bnet files do not have any information about regulations. As such, by default regulations are loaded as non-essential with no fixed sign. If you set repair_graph=True, then we use a symbolic method that infers these annotations automatically.

def to_bnet(self, rename_if_necessary: bool = True) -> str:

Produce a .bnet string representation of this BooleanNetwork.

Returns an error if the network is parametrised and thus cannot be converted to .bnet.

By default, the method will rename any variables whose names are not supported in .bnet. However, you can instead ask it to throw a RuntimeError using the rename_if_necessary flag.

def from_sbml(file_contents: str) -> BooleanNetwork:

Try to load a BooleanNetwork from the contents of an .sbml model file.

def to_sbml(self) -> str:

Produce a .sbml string representation of this BooleanNetwork.

def explicit_parameter_count(self) -> int:

The number of explicit parameters, i.e. named uninterpreted functions in this network.

def implicit_parameter_count(self) -> int:

The number of implicit parameters, i.e. anonymous uninterpreted functions in this network.

def explicit_parameters(self) -> dict[ParameterId, int]:

Return the dictionary of ParameterId identifiers of explicit parameters and their corresponding arities.

Keep in mind that the iteration order of keys of this dictionary is not deterministic. If you need deterministic iteration, you have to sort the keys.

def implicit_parameters(self) -> dict[VariableId, int]:

Return the dictionary of VariableId identifiers for variables with anonymous update functions and their corresponding arities.

Keep in mind that the iteration order of keys of this dictionary is not deterministic. If you need deterministic iteration, you have to sort the keys.

def explicit_parameter_names(self) -> list[str]:

Return the list of explicit parameter names. The names as sorted in accordance with the ParameterId identifiers.

def get_explicit_parameter_name(self, parameter: Union[ParameterId, str]) -> str:

Return the name of the given explicit parameter.

def get_explicit_parameter_arity(self, parameter: Union[ParameterId, str]) -> int:

Return the arity of an explicit parameter.

def find_explicit_parameter( self, parameter: Union[ParameterId, str]) -> Optional[ParameterId]:

Return a ParameterId identifier of the requested parameter, or None if the uninterpreted function does not exist in this BooleanNetwork.

def add_explicit_parameter(self, name: str, arity: int) -> ParameterId:

Create a new explicit parameter.

the parameter name must be unique among existing variables and parameters.

def get_update_function( self, variable: Union[VariableId, str]) -> Optional[UpdateFunction]:

Get the UpdateFunction of a particular network variable, or None if the function is unknown (i.e. na implicit parameter).

def set_update_function( self, variable: Union[VariableId, str], function: Union[str, UpdateFunction, NoneType]) -> Optional[UpdateFunction]:

Update the current update function of the specified variable and return the previous function.

All variables and parameters used in the new function must already exist in the BooleanNetwork. Furthermore, the function can only use variables that are declared as regulators of the target variable.

def infer_valid_graph(self) -> BooleanNetwork:

Infer a sufficient local regulatory graph based on the update functions of this BooleanNetwork.

Notes

The method will simplify the update functions when it detects that a variable is not an essential input of the update function (for any instantiation).
This also removes any unused parameters (uninterpreted functions), or parameters that become unused due to the transformation.
For fully specified update functions, the method simply updates the regulations to match the actual behaviour of the function (i.e. any non-essential regulations are removed, sign is always specified unless the input is truly non-monotonic).
For regulations that interact with uninterpreted functions:
- Essentiality: If there are no instantiations where the regulation is essential, we remove the regulation completely. Otherwise, we preserve the original essentiality constraint.
- Monotonicity: Similarly, if every instantiation of the function has a known monotonicity, then we use the corresponding sign. Otherwise, if the original constraint is still satisfied for a subset of all instantiations, we use the original one.

Limitations

The result only guarantees that the constraints are locally consistent*, meaning they are valid when applied to the singular update function, not necessarily the whole model. In other words, uninterpreted functions that are used by multiple variables can still cause the model to be invalid if they use contradictory constraints, but this usually cannot be resolved deterministically because we would have to pick which constraint should be relaxed to resolve the conflict.

Output

The function can fail if, for whatever reason, it cannot create SymbolicContext for the input network.

def remove_regulation_constraints(self) -> BooleanNetwork:

Make a copy of this BooleanNetwork with all constraints on the regulations removed. In particular, every regulation is set to non-essential with an unknown sign.

def inline_constants( self, infer_constants: bool = False, repair_graph: bool = False) -> BooleanNetwork:

Similar to BooleanNetwork.inline_inputs, but inlines constant values (i.e. x=true or x=false).

By default, the constant check is purely syntactic, but we do perform basic constant propagation (e.g. x | true = true) in order to catch the most obvious non-trivial cases. However, you can set infer_constants to True, in which case a symbolic method will be used to check if the variable has a constant function. Note that this can also eliminate parameters in some cases (e.g. inlining x=true into y=x | f(z)).

Furthermore, similar to BooleanNetwork.inline_inputs, you can set repair_graph to true to fix any inconsistent regulations that arise due to the inlining (this is highly recommended if you are using infer_constants).

The inlining is performed iteratively, meaning if the inlining produces a new constant, it is eventually also inlined.

The method can fail if infer_constants or repair_graph is specified and the network does not have a valid symbolic representation.

def inline_inputs( self, infer_inputs: bool = False, repair_graph: bool = False) -> BooleanNetwork:

Try to inline the input nodes (variables) of the network as logical parameters (uninterpreted functions of arity 0).

Here, an "input" is a variable x such that:

x has no incoming regulations and a missing update function.
x has an identity update function. This is either checked syntactically (default), or semantically using BDDs (if infer_inputs is set to True).

Note that this does not include constant nodes (e.g. x=true). These are handled separately by BooleanNetwork.inline_constants. Also note that input variables that do not influence any other variable are removed.

Variables with update functions x=f(true, false) or x=a (where a is a zero-arity parameter) are currently not considered to be inputs, although their role is conceptually similar.

This method is equivalent to calling BooleanNetwork.inline_variable on each input, but the current implementation of BooleanNetwork.inline_variable does not permit inlining of self-regulating variables, hence we have a special method for inputs only.

Finally, just as BooleanNetwork.inline_variable, the method can generate an inconsistent regulatory graph. If repair_graph is set to True, the static properties of relevant regulations are inferred using BDDs.

def prune_unused_parameters(self) -> BooleanNetwork:

Return a copy of this network where all unused explicit parameters (uninterpreted functions) are removed.

Note that VariableId objects are still valid for the result network, but ParameterId objects can now refer to different parameters.

def assign_parameter_name( self, variable: Union[VariableId, str], name: str | None = None) -> ParameterId:

Replaces an implicit parameter (i.e. an anonymous update function) with an explicit parameter of the given name. If no name is provided, a default name is generated instead.

The arguments of the newly created update function follow the ordering of variable IDs.

def name_implicit_parameters(self) -> BooleanNetwork:

Replaces all implicit parameters with explicit counterparts using default names.

def is_variable_input( self, variable: Union[VariableId, str], ctx: SymbolicContext | None = None) -> bool:

Returns True if the given variable is an input of the BooleanNetwork.

Input can be either:

A variable with no incoming regulations and no update function.
A variable with a positive self-regulation and an update function that is equivalent to an identity function.

Note that by default, function equivalent is tested only syntactically (with basic simplifications applied). To test equivalence semantically, you have to provide a SymbolicContext object as the second argument.

def is_variable_constant( self, variable: Union[VariableId, str], ctx: SymbolicContext | None = None) -> bool | None:

Tests whether the given variable is a constant of the BooleanNetwork. A variable is a constant if it's update function is equivalent to True or False. Note that this differs from inputs, whose update function is equivalent to identity.

If the variable is not constant, the function returns None. If it is constant, it returns its constant value.

By default, function equivalent is tested only syntactically (with basic simplifications applied). To test equivalence semantically, you have to provide a SymbolicContext object as the second argument.

def inputs(self, infer: bool = False) -> list[VariableId]:

Return the list of all inputs that are present in this BooleanNetwork. See also BooleanNetwork.is_var_input.

If infer=True, the method will use symbolic equivalence check for identifying input variables, which is more accurate but also more resource intensive.

def input_names(self, infer: bool = False) -> list[str]:

Same as BooleanNetwork.inputs, but returns a list of variable names instead.

def constants(self, infer: bool = False) -> dict[VariableId, bool]:

Return the dictionary of all constants that are present in this BooleanNetwork. See also BooleanNetwork.is_var_constant.

If infer=True, the method will use symbolic equivalence check for identifying constant variables, which is more accurate but also more resource intensive.

def constant_names(self, infer: bool = False) -> dict[str, bool]:

Same as BooleanNetwork.constants, but the keys in the dictionary are variable names, not IDs.

Inherited Members

RegulatoryGraph: to_dot; variable_count; variable_names; variables; find_variable; get_variable_name; regulation_count; regulations; regulation_strings; find_regulation; predecessors; successors; backward_reachable; forward_reachable; feedback_vertex_set; independent_cycles; strongly_connected_components; weakly_connected_components; shortest_cycle

class UpdateFunction:

Describes a single update function that is used to describe the dynamics of a BooleanNetwork.

It is similar to a BooleanExpression, but additionally admits the use of uninterpreted functions (also called explicit parameters in the context of a BooleanNetwork). These are Boolean functions with unknown but fixed specification that stand in for any unknown behaviour in the corresponding BooleanNetwork.

Additionally, compared to a BooleanExpression, the UpdateFunction refers to network variables and parameters using VariableId and ParameterId. To that end, every UpdateFunction has an underlying BooleanNetwork which is used to resolve names to IDs and vice versa.

UpdateFunction( ctx: BooleanNetwork, value: Union[str, UpdateFunction, BooleanExpression])

Build a new UpdateFunction in the context of the specified BooleanNetwork. The value can be either a string (in which case it is parsed), an UpdateFunction, in which case it is "translated" into the given context (IDs are updated based on matching names), or a BooleanExpression, in which case it also translated using variable names.

def mk_const(ctx: BooleanNetwork, value: Union[bool, int]) -> UpdateFunction:

Return an UpdateFunction for a constant value.

def mk_var( ctx: BooleanNetwork, variable: Union[VariableId, str]) -> UpdateFunction:

Return an UpdateFunction of a single variable.

def mk_param( ctx: BooleanNetwork, parameter: Union[ParameterId, str], arguments: Sequence[Union[UpdateFunction, VariableId, str]]) -> UpdateFunction:

def mk_not(value: UpdateFunction) -> UpdateFunction:

Return a negation of an UpdateFunction.

def mk_and( left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Return an and of two UpdateFunction values.

def mk_or( left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Return an or of two UpdateFunction values.

def mk_imp( left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Return an imp of two BooleanExpression values.

def mk_iff( left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Return an iff of two BooleanExpression values.

def mk_xor( left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Return a xor of two BooleanExpression values.

def mk_binary( op: Literal['and', 'or', 'imp', 'iff', 'xor'], left: UpdateFunction, right: UpdateFunction) -> UpdateFunction:

Construct a binary expression using the given operator (and/or/imp/iff/xor).

def mk_conjunction( ctx: BooleanNetwork, args: Sequence[Union[UpdateFunction, str]]) -> UpdateFunction:

Build a conjunction of multiple expressions.

def mk_disjunction( ctx: BooleanNetwork, args: Sequence[Union[UpdateFunction, str]]) -> UpdateFunction:

Build a disjunction of multiple expressions.

def is_const(self) -> bool:

Return true if the root of this expression is a constant.

def is_var(self) -> bool:

Return true if the root of this expression is a variable.

def is_param(self) -> bool:

Return true if the root of this expression is a call to an uninterpreted function.

def is_not(self) -> bool:

Return true if the root of this expression is a not.

def is_and(self) -> bool:

Return true if the root of this expression is an and.

def is_or(self) -> bool:

Return true if the root of this expression is an or.

def is_imp(self) -> bool:

Return true if the root of this expression is an imp.

def is_iff(self) -> bool:

Return true if the root of this expression is an iff.

def is_xor(self) -> bool:

Return true if the root of this expression is a xor.

def is_literal(self) -> bool:

Return true if the root of this expression is a literal (var/!var).

def is_binary(self) -> bool:

Return true if the root of this expression is a binary operator (and/or/imp/iff/xor).

def as_const(self) -> Optional[bool]:

If the root of this expression is a constant, return its value, or None otherwise.

def as_var(self) -> Optional[VariableId]:

If the root of this expression is a var, return its ID, or None otherwise.

def as_param(self) -> Optional[tuple[ParameterId, list[UpdateFunction]]]:

If the root of this expression is a call to an uninterpreted function, return its ID and arguments, or None otherwise.

def as_not(self) -> Optional[UpdateFunction]:

If the root of this expression is a not, return its operand, or None otherwise.

def as_and(self) -> Optional[tuple[UpdateFunction, UpdateFunction]]:

If the root of this expression is an and, return its two operands, or None otherwise.

def as_or(self) -> Optional[tuple[UpdateFunction, UpdateFunction]]:

If the root of this expression is an or, return its two operands, or None otherwise.

def as_imp(self) -> Optional[tuple[UpdateFunction, UpdateFunction]]:

If the root of this expression is an imp, return its two operands, or None otherwise.

def as_iff(self) -> Optional[tuple[UpdateFunction, UpdateFunction]]:

If the root of this expression is an iff, return its two operands, or None otherwise.

def as_xor(self) -> Optional[tuple[UpdateFunction, UpdateFunction]]:

If the root of this expression is xor, return its two operands, or None otherwise.

def as_literal(self) -> Optional[tuple[VariableId, bool]]:

If this expression is either var or !var, return the ID of the variable and whether it is positive. Otherwise, return None.

def as_binary( self) -> Optional[tuple[Literal['and', 'or', 'imp', 'iff', 'xor'], UpdateFunction, UpdateFunction]]:

If the root of this expression is one of the and/or/imp/iff/xor operators, return the name of the operator and its two operands. Returns None if the root is not a binary operator.

def support_variables(self) -> set[VariableId]:

Return the set of variable IDs that are used in this UpdateFunction.

def support_parameters(self) -> set[ParameterId]:

Return the set of parameter IDs that are used in this UpdateFunction.

def substitute_all( self, substitution: Union[Mapping[str, Union[UpdateFunction, str]], Mapping[VariableId, Union[UpdateFunction, str]]]) -> UpdateFunction:

Create a copy of this UpdateFunction with every occurrence of the specified variables substituted for the corresponding function.

Note that at the moment, there is no substitution method for parameters, since we don't have a concept of an "expression with holes" which we could use here.

def rename_all( self, new_ctx: Optional[BooleanNetwork] = None, variables: Union[Mapping[str, Union[VariableId, str]], Mapping[VariableId, Union[VariableId, str]], NoneType] = None, parameters: Union[Mapping[str, Union[ParameterId, str]], Mapping[ParameterId, Union[ParameterId, str]], NoneType] = None) -> UpdateFunction:

Rename all occurrences of the specified variables and parameters to new IDs.

The variables and parameters dictionaries map the old variables (using VariableId or a string name) to new variables (again, using IDs or names). If the new names or IDs are not valid in the currently referenced BooleanNetwork, you can supply a new_ctx. If new_ctx is given, dictionary keys are resolved in the current context, but dictionary values are resolved in the newly provided context.

def simplify_constants(self) -> UpdateFunction:

Creates a copy of this UpdateFunction with all constant values propagated into the remaining expression. Consequently, the result contains constant values only if (a) the whole function is a constant, or (b) a constant value is used as an argument of an uninterpreted function (parameter).

def distribute_negation(self) -> UpdateFunction:

Creates a copy of this UpdateFunction where the negation operation is distributed to the propositions (constants, network variables, and function invocations).

The operation is also applied to each expression that is an argument of an uninterpreted function. However, we cannot distribute the negation of an uninterpreted function to its arguments without further knowledge about its behaviour.

def to_and_or_normal_form(self) -> UpdateFunction:

Creates a copy of this UpdateFunction where all binary operators are expanded into their and/or equivalents.

Note that in extreme cases, the result can be an exponentially larger formula compared to the original.

def as_expression(self) -> BooleanExpression:

Convert the UpdateFunction to a BooleanExpression, as long as the function contains no uninterpreted functions (otherwise throws a RuntimeError).

class ModelAnnotation:

Annotations are "meta" objects that can be declared as part of .aeon models to add additional properties that are not directly recognized by the main AEON toolbox.

An annotation object behaves like a tree, where each node can have an optional string value, and an unordered collection of children which behave mostly like a dictionary:

ann = ModelAnnotation()
# Empty ModelAnnotation is created automatically when key is first accessed.
desc = ann['description']
assert desc.value is None
desc.value = "Multiline...\n"
desc.value += "...test description"
desc['x'].value = "Variable X"
desc['y'].value = "Variable Y"

assert len(desc) == 2
assert ann['description']['x'].value == "Variable X"

This generates the following set of annotation comments:

#!description:Multiline...
#!description:...test description
#!description:x:Variable X
#!description:y:Variable Y

Annotation syntax

Annotations are comments which start with #!. After the #! "preamble", each annotation can contain a "path prefix" with path segments separated using : (path segments can be surrounded by white space that is automatically trimmed). Based on these path segments, the parser will create an annotation tree. If there are multiple annotations with the same path, their values are concatenated using newlines.

For example, annotations can be used to describe the model layout:

#! layout : var_1 : 10,20
#! layout : var_2 : 14,-3

Another usage for annotations are additional properties expected from the model, for example written in CTL:

#! property : AG (problem => AF apoptosis)

Obviously, you can also use annotations to specify model metadata:

#! name: My Awesome Model
#! description: This model describes ...
#! description:var_1: This variable describes ...

You can use "empty" path (e.g. #! is_multivalued), and you can use an empty annotation value with a non-empty path (e.g. #! is_multivalued:var_1:). Though this is not particularly encouraged: it is better to just have var_1 as the annotation value if you can do that. An exception to this may be a case where is_multivalued:var_1: has an "optional" value, and you want to express that while the "key" is provided, the "value" is missing. Similarly, for the sake of completeness, it is technically allowed to use empty path names (e.g. a::b:value translates to ["a", "", "b"] = "value"), but it is discouraged.

Note that the path segments should only contain alphanumeric characters and underscores, but can be escaped using backticks (`; other backticks in path segments are not allowed). Similarly, annotation values cannot contain colons (path segment separators) or backticks, unless escaped with #`ACTUAL_STRING`#. You can also use escaping if you wish to retain whitespace surrounding the annotation value. As mentioned, multi-line values can be split into multiple annotation comments.

ModelAnnotation(value: Optional[str] = None)

Create a new ModelAnnotation with an optional string value.

The child annotations can be then set similar to a normal dictionary, but this is not supported in the constructor for now.

def from_aeon(file_contents: str) -> ModelAnnotation:

Parse an annotation object from the string representing the contents of an .aeon file.

def from_file(path: str) -> ModelAnnotation:

Parse an annotation object from an .aeon file at the given path.

def values(self) -> list[ModelAnnotation]:

Return the list of annotations that are the direct descendants of this annotation.

def keys(self) -> list[str]:

Return the sorted list of keys that are stored in this annotation.

def items(self) -> list[tuple[str, ModelAnnotation]]:

Return the list key-value pairs that correspond to the direct descendants of this annotation.

value: Optional[str]

The optional string value of the model annotation.

class SymbolicContext:

Intuitively, a SymbolicContext encodes the entities of a BooleanNetwork into a set of symbolic variables managed by a BddVariableSet. Using this representation, we can ecode sets of states, sets of function interpretations, or relations over both.

Internally, each VariableId corresponds to one BddVariable, and each uninterpreted function corresponds to a table of 2^k BddVariable identifiers, which together represent the logical table of the uninterpreted function.

An uninterpreted function is created for each explicit and implicit parameter of the BooleanNetwork for which a SymbolicContext is constructed. The SymbolicContext is static and does not update even if the supplied network changes later. Also, keep in mind that implicit parameters are only created for variables with missing update functions, not all network variables.

Additionally, you can specify your own "extra" symbolic variables. These can be used to build more complex symbolic algorithms on top of the basic encoding, like model checking, control, or trap space detection. These extra variables are grouped with the network variables for convenience. This also determines their ordering within the BddVariableSet: the extra variables associated with variable x are created right after x for best locality.

Finally, SymbolicContext allows to build and interpret Bdd objects that are valid in the encoding it describes. For example, you can use SymbolicContext.mk_update_function to create a symbolic Bdd representation of an UpdateFunction.

Whenever a SymbolicContext returns a list of sortable objects (like BddVariable, VariableId, or ParameterId), it is expected that these objects are sorted.

SymbolicContext( network: BooleanNetwork, extra_variables: Union[Mapping[str, int], Mapping[VariableId, int], NoneType] = None)

A SymbolicContext is created by providing a BooleanNetwork and optional extra_variables dictionary.

At the moment, it is required that all explicit parameters (uninterpreted functions) that are declared in the given network are actually used by some update function in said network.

In the future, this restriction will be lifted, but it is not quite clear how soon will this happen.

Furthermore, due to this dependence on a BooleanNetwork structure, a SymbolicContext cannot be currently pickled. It is recommended that you instead save the .aeon representation of the BooleanNetwork in question.

def network_variable_count(self) -> int:

The number of the network variables (or state variables) that are encoded by this SymbolicContext.

def network_variable_names(self) -> list[str]:

The names of the network variables that are encoded by this SymbolicContext.

def network_variables(self) -> list[VariableId]:

The VariableId identifiers of the network variables that are encoded by this SymbolicContext.

def network_bdd_variables(self) -> list[BddVariable]:

The BddVariable IDs of symbolic variables that encode the network variables in this SymbolicContext.

def find_network_variable( self, variable: Union[VariableId, str, BddVariable]) -> Optional[VariableId]:

Return a VariableId of the specified network variable, assuming such variable exists.

Compare to methods like BooleanNetwork.find_variable, this method can also resolve a BddVariable to the corresponding VariableId (assuming said BddVariable encodes a network variable).

def find_network_bdd_variable( self, variable: Union[VariableId, str, BddVariable]) -> Optional[BddVariable]:

The same as SymbolicContext.find_network_variable, but returns the BddVariable which encodes the specified network variable.

def get_network_variable_name(self, variable: Union[VariableId, str, BddVariable]) -> str:

The name of a particular network variable.

def extra_bdd_variable_count(self) -> int:

The total number of extra symbolic variables that are present in this SymbolicContext.

def extra_bdd_variables_list(self) -> list[BddVariable]:

The list of all extra symbolic variable in this SymbolicContext.

def extra_bdd_variables(self) -> dict[VariableId, list[BddVariable]]:

A dictionary which returns the list of extra symbolic variables for each network variable.

def explicit_function_count(self) -> int:

The number of explicit functions (parameters) managed by this SymbolicContext.

def explicit_functions(self) -> list[VariableId]:

The list of ParameterId objects identifying the individual explicit functions in this SymbolicContext.

def explicit_functions_bdd_variables_list(self) -> list[BddVariable]:

The list of all symbolic variables which this SymbolicContext uses for the encoding of the explicit uninterpreted functions.

def explicit_functions_bdd_variables(self) -> dict[ParameterId, list[BddVariable]]:

A dictionary which maps the ParameterId of an explicit function to the list of symbolic variables that are used to encode said function.

def implicit_function_count(self) -> int:

The number of implicit functions (parameters) managed by this SymbolicContext.

def implicit_functions(self) -> list[VariableId]:

The list of variables that have an implicit function declared for them.

def implicit_functions_bdd_variables_list(self) -> list[BddVariable]:

The list of all symbolic variables which this SymbolicContext uses for the encoding of the implicit uninterpreted functions.

def implicit_functions_bdd_variables(self) -> dict[VariableId, list[BddVariable]]:

A dictionary which maps the VariableId of an implicit function to the list of symbolic variables that are used to encode said function.

def function_count(self) -> int:

The total number of uninterpreted functions in this encoding.

def functions(self) -> list[typing.Union[VariableId, ParameterId]]:

The list of all explicit and implicit uninterpreted functions in this encoding.

def functions_bdd_variables_list(self) -> list[BddVariable]:

The list of all symbolic variables which this SymbolicContext uses for the encoding of the uninterpreted functions (both implicit and explicit).

def functions_bdd_variables( self) -> dict[typing.Union[VariableId, ParameterId], list[BddVariable]]:

A dictionary which maps the VariableId and ParameterId objects identifying individual uninterpreted functions to the symbolic variables that are used to encode said function.

def find_function( self, function: Union[VariableId, ParameterId, BddVariable, str]) -> Union[VariableId, ParameterId, NoneType]:

Find a ParameterId (explicit function) or VariableId (implicit function) which identifies the specified function, or None if such function does not exist.

The function can accept a BddVariable. In such case, it will try to identify the function table in which the variable resides. Note that this is a linear search.

def get_function_name( self, function: Union[VariableId, ParameterId, BddVariable, str]) -> str:

Return the name of an uninterpreted function. For explicit functions, the name of the network parameter is returned. For implicit functions, the name of the corresponding network variable is returned.

def get_function_arity( self, function: Union[VariableId, ParameterId, BddVariable, str]) -> int:

Return the arity (the number of arguments) of the specified uninterpreted function.

def get_function_table( self, function: Union[VariableId, ParameterId, BddVariable, str]) -> list[tuple[list[bool], BddVariable]]:

Return the "function table" a specified uninterpreted function. A function table consists of tuples, where each tuple represents one input-output pair of the logical table of the function in question. The input is a list of Boolean values, the output is a symbolic variable that represents the output of the function for this input vector.

def mk_constant(self, value: Union[bool, int]) -> Bdd:

Create a new constant (True/False) Bdd.

def mk_network_variable(self, variable: Union[VariableId, str]) -> Bdd:

Create a new Bdd which is true if and only if the specified network variable is true.

This is equivalent to calling SymbolicContext.mk_update_function with UpdateFunction.mk_var(variable) as the argument.

def mk_extra_bdd_variable( self, variable: Union[VariableId, str, NoneType] = None, index: Optional[int] = None) -> Bdd:

Create a new Bdd which is true if and only if the specified extra symbolic variable is true. The variable is specified by its associated network variable and index (or offset).

If the arguments are not provided, the method uses the first network variable and index 0.

def mk_function( self, function: Union[VariableId, ParameterId, str], arguments: Sequence[Union[UpdateFunction, Bdd, VariableId, str]]) -> Bdd:

Create a Bdd which is valid if and only if the specified uninterpreted function is valid.

The function takes a vector of arguments which must match the arity of the uninterpreted function. An argument can be either an arbitrary Bdd object, or an UpdateFunction from which a Bdd is then constructed.

def mk_update_function(self, function: UpdateFunction) -> Bdd:

Create a Bdd which is valid if and only if the specified UpdateFunction is valid.

This can be used to build any Boolean function that depends on the network variables and the explicit uninterpreted functions. It cannot be used to operate on the extra symbolic variables or implicit uninterpreted functions.

def bdd_variable_set(self) -> BddVariableSet:

The underlying BddVariableSet used for the encoding.

def transfer_from(self, bdd: Bdd, old_ctx: SymbolicContext) -> Bdd:

This is similar to BddVariableSet.transfer_from, but is applied at the level of symbolic contexts.

In other words, you can use this method to translate Bdd objects between contexts that use similar variables and parameters, as long as the Bdd only uses objects that are present in both context, and are ordered the same in both contexts.

def to_canonical_context(self) -> SymbolicContext:

Compute a "canonical context" for this SymbolicContext. A canonical context has no extra symbolic variables. In other words, it is a context that contains only the elements necessary to encode the original BooleanNetwork and nothing else.

You can use this method in combination with SymbolicContext.transfer_from in algorithms that require more complicated symbolic contexts. After such algorithm computes a result, it can be safely transferred to the "canonical context" which ensures it can be then interpreted using only the input model, without any internal information about the algorithm that was used to obtain the result.

def eliminate_network_variable( self, variable: Union[VariableId, str, BddVariable]) -> SymbolicContext:

Create a new SymbolicContext which is compatible with the current context (it uses the same BddVariableSet), but is missing the given network variable.

The new context uses the same ParameterId identifiers as the old context, but has different VariableId identifiers, since one of the variables is no longer used, and VariableId identifiers must be always a contiguous sequence. You should use variable names to "translate" VariableId identifiers between the two symbolic context. Of course, SymbolicContext.transfer_from should also still work.

Note that the extra symbolic variables and implicit function tables do not disappear, even if they are only used by the eliminated variable. They will still appear in SymbolicContext.extra_bdd_variables_list and SymbolicContext.functions_bdd_variables_list. However, you will no longer find them in SymbolicContext.extra_bdd_variables and SymbolicContext.functions_bdd_variables, since their variable is eliminated.

class SymbolicSpaceContext(SymbolicContext):

An extension of the SymbolicContext which supports symbolic representation of network sub-spaces.

To implement this, SymbolicSpaceContext uses the "extra variables" feature of the standard SymbolicContext. On its own, SymbolicSpaceContext currently does not allow having any extra variables aside from those used for space representation. However, nothing fundamentally prevents us from including additional variables in the future.

SymbolicSpaceContext( network: BooleanNetwork, extra_variables: Union[Mapping[str, int], Mapping[VariableId, int], NoneType] = None)

A SymbolicSpaceContext is created from a BooleanNetwork, just as a regular SymbolicContext. However, no extra symbolic variables can be specified in this case.

def eliminate_network_variable( self, variable: Union[VariableId, str, BddVariable]) -> SymbolicSpaceContext:

See SymbolicContext.eliminate_network_variable.

def get_positive_space_variable(self, variable: Union[VariableId, str]) -> BddVariable:

The symbolic variable that encodes the fact that a specified network_variable can have value True in a particular subspace.

def get_negative_space_variable(self, variable: Union[VariableId, str]) -> BddVariable:

The symbolic variable that encodes the fact that a specified network_variable can have value False in a particular subspace.

def mk_can_go_to_true(self, functions: Bdd) -> Bdd:

Compute a Bdd which encodes all spaces in which the value of function can be true for some state. We assume that function can depend on state variables and parameter variables, but not on the dual variables used for space encoding.

In other words, a space S satisfies the result Bdd if and only if there exists a state x \in S such that function(x) = true.

To compute this, we evaluate the following (informal) expression: exists s_1...s_n: [(s_i => s_i_T) & (!s_i => s_i_F)] & function(s_1, ..., s_n)

WARNING: The resulting BDD also allows invalid space encodings, mostly because these are to some extent still interesting in some applications. You'll need to intersect it with SymbolicSpaceContext.mk_unit_bdd.

def mk_empty_colored_spaces(self) -> ColoredSpaceSet:

Compute an empty colored subspace relation.

def mk_empty_spaces(self) -> SpaceSet:

Compute an empty set of network subspaces.

def mk_unit_colored_spaces( self, graph: Optional[AsynchronousGraph] = None) -> ColoredSpaceSet:

Compute the colored set of all network sub-spaces.

Note that SymbolicSpaceContext has no notion of "unit colors". By default, the final relation contains all colors. If you want to restrict the relation in the same manner as AsynchronousGraph.mk_unit_colored_vertices, you have to provide an optional AsynchronousGraph.

def mk_unit_spaces(self) -> SpaceSet:

Compute the set of all network sub-spaces.

Note that this is different from a Bdd function True because not every valuation of the dual variables encodes a valid network space.

def mk_unit_bdd(self) -> Bdd:

Compute the Bdd which contains all correctly encoded spaces tracked by this SymbolicSpaceContext.

The Bdd only constraints the space variables and it has no impact on the network/parameter variables. Also note that this is not the true function, since not every valuation of space variables correctly encodes a space.

def mk_sub_spaces(self, set):

def mk_sub_spaces(self, set: ColoredSpaceSet) -> ColoredSpaceSet:

def mk_sub_spaces(self, set: SpaceSet) -> SpaceSet:

def mk_sub_spaces(self, set: Bdd) -> Bdd:

Extend the given set with all the sub-spaces for every element of the set.

For colored sets, this extension is happening color-wise, so new sub-spaces are added with the same color as their parent space.

def mk_super_spaces(self, set):

def mk_super_spaces(self, set: ColoredSpaceSet) -> ColoredSpaceSet:

def mk_super_spaces(self, set: SpaceSet) -> SpaceSet:

def mk_super_spaces(self, set: Bdd) -> Bdd:

Extend the given set with all the sub-spaces for every element of the set.

For colored sets, this extension is happening color-wise, so new sub-spaces are added with the same color as their parent space.

def mk_singleton( self, space: Union[Mapping[str, Union[bool, int]], Mapping[VariableId, Union[bool, int]]]) -> SpaceSet:

Compute the SpaceSet that represents a single network subspace.

def spaces_to_vertices(self, set: Bdd) -> Bdd:

A utility method which "materializes" the network spaces in the dual encoding into a set of vertices that reside in these places.

See also SymbolicSpaceContext::vertices_to_spaces, but note that these operations are not invertible, that is vertices_to_spaces(spaces_to_vertices(x)) does not produce the original set x.

def vertices_to_spaces(self, set: Bdd) -> Bdd:

Convert a set of vertices into a set of singleton spaces. That is, for each vertex, the corresponding space is created.

In other words, this does not try to decompose the set into maximal spaces or anything like that, it converts each vertex 1:1 into a space.

Inherited Members

SymbolicContext: network_variable_count; network_variable_names; network_variables; network_bdd_variables; find_network_variable; find_network_bdd_variable; get_network_variable_name; extra_bdd_variable_count; extra_bdd_variables_list; extra_bdd_variables; explicit_function_count; explicit_functions; explicit_functions_bdd_variables_list; explicit_functions_bdd_variables; implicit_function_count; implicit_functions; implicit_functions_bdd_variables_list; implicit_functions_bdd_variables; function_count; functions; functions_bdd_variables_list; functions_bdd_variables; find_function; get_function_name; get_function_arity; get_function_table; mk_constant; mk_network_variable; mk_extra_bdd_variable; mk_function; mk_update_function; bdd_variable_set; transfer_from; to_canonical_context

class VertexSet:

A symbolic representation of a set of "vertices", i.e. valuations of variables of a particular BooleanNetwork.

VertexSet(ctx: SymbolicContext, bdd: Bdd)

Normally, a new VertexSet is derived using an AsynchronousGraph. However, in some cases you may want to create it manually from a SymbolicContext and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid set of vertices.

def cardinality(self) -> int:

Returns the number of vertices that are represented in this set.

def intersect(self, other: VertexSet) -> VertexSet:

Set intersection.

def minus(self, other: VertexSet) -> VertexSet:

Set difference.

def union(self, other: VertexSet) -> VertexSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: VertexSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single vertex.

def is_subspace(self) -> bool:

True if this set is a subspace, i.e. it can be expressed using a single conjunctive clause.

def pick_singleton(self) -> VertexSet:

Deterministically pick a subset of this set that contains exactly a single vertex.

If this set is empty, the result is also empty.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this VertexSet.

def extend_with_colors(self, set: ColorSet) -> ColoredVertexSet:

Extend this set of vertices with all the colors from the given set.

This is essentially a cartesian product with the given ColorSet.

def items( self, retained: Optional[Sequence[Union[VariableId, str]]] = None) -> Iterator[VertexModel]:

Returns an iterator over all vertices in this VertexSet with an optional projection to a subset of network variables.

When no retained collection is specified, this is equivalent to VertexSet.__iter__. However, if a retained set is given, the resulting iterator only considers unique combinations of the retained variables. Consequently, the resulting VertexModel instances will fail with an IndexError if a value of a variable outside the retained set is requested.

def to_singleton_spaces(self, ctx: SymbolicSpaceContext) -> SpaceSet:

Represent this set of vertices as a set of singleton subspaces instead.

def enclosing_subspace(self) -> dict[VariableId, bool] | None:

Compute the smallest enclosing subspace, represented as dict[VariableId, bool] with missing variables being treated as unrestricted.

Returns None if the set is empty.

def enclosing_named_subspace(self) -> dict[str, bool] | None:

Compute the smallest enclosing subspace, represented as dict[str, bool], using variable names as keys and with missing variables being treated as unrestricted.

Returns None if the set is empty.

def enclosed_subspace(self) -> dict[VariableId, bool] | None:

Compute the largest subspace that is fully enclosed in this vertex set. Note that such subspace may not be unique (i.e. there can be other subspaces that are just as large).

Returns None if the set is empty.

def enclosed_named_subspace(self) -> dict[str, bool] | None:

Same as VertexSet.enclosed_subspace, but uses names instead of IDs.

class VertexModel:

Represents a single vertex stored in a VertexSet (or a ColoredVertexSet), or a projection of said vertex to the chosen variables.

Behaves like an immutable dictionary: Boolean variable values can be queried using a VariableId, a string name, or a BddVariable.

def keys(self) -> list[VariableId]:

The actual "retained" network variables in this model.

This is the list of all network variables if no projection was applied.

def values(self) -> list[bool]:

The list of values for individual variables from VertexModel.keys.

def items(self) -> list[tuple[VariableId, bool]]:

The list of key-value pairs represented in this model.

def to_dict(self) -> dict[VariableId, bool]:

The same as VertexModel.items, but returns a dictionary instead.

def to_named_dict(self) -> dict[str, bool]:

The same as VertexModel.to_dict, but the keys in the dictionary are names, not IDs.

def to_valuation(self) -> BddPartialValuation:

Return the underlying BddPartialValuation for this symbolic model.

def to_symbolic(self) -> VertexSet:

Return a VertexSet where all the variables are fixed according to the values in this VertexModel. Variables that are not present in the VertexModel are unrestricted.

class ColorSet:

A symbolic representation of a set of "colours", i.e. interpretations of explicit and implicit parameters within a particular BooleanNetwork.

ColorSet(ctx: SymbolicContext, bdd: Bdd)

Normally, a new ColorSet is derived using an AsynchronousGraph. However, in some cases you may want to create it manually from a SymbolicContext and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid set of colors.

def cardinality(self) -> int:

Returns the number of "colors" (function interpretations) that are represented in this set.

def intersect(self, other: ColorSet) -> ColorSet:

Set intersection.

def minus(self, other: ColorSet) -> ColorSet:

Set difference.

def union(self, other: ColorSet) -> ColorSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: ColorSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single function interpretation.

def is_subspace(self) -> bool:

True if this set is a subspace, i.e. it can be expressed using a single conjunctive clause.

def pick_singleton(self) -> ColorSet:

Deterministically pick a subset of this set that contains exactly a single function interpretation.

If this set is empty, the result is also empty.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this ColorSet.

def extend_with_vertices(self, set: VertexSet) -> ColoredVertexSet:

Extend this set of colors with all the vertices from the given set.

This is essentially a cartesian product with the given VertexSet.

def extend_with_spaces(self, set: SpaceSet) -> ColoredSpaceSet:

Extend this set of colors with all the spaces from the given set.

This is essentially a cartesian product with the given SpaceSet.

def extend_with_perturbations(self, set: PerturbationSet) -> ColoredPerturbationSet:

def items( self, retained: Optional[Sequence[Union[VariableId, ParameterId, str]]] = None) -> Iterator[ColorModel]:

Returns an iterator over all interpretations in this ColorSet with an optional projection to a subset of uninterpreted functions.

When no retained collection is specified, this is equivalent to ColorSet.__iter__. However, if a retained set is given, the resulting iterator only considers unique combinations of the retained functions. Consequently, the resulting ColorModel instances will fail with an IndexError if a value of a function outside the retained set is requested.

class ColorModel:

Represents a single "color" stored in a ColorSet (or a ColoredVertexSet), or a projection of said color to the chosen uninterpreted functions.

Behaves like an immutable dictionary: Uninterpreted functions can be queried using a VariableId/ParameterId (implicit/explicit parameters), a string name, or a BddVariable from the function table. The result is a BooleanExpression.

However, note that each function instantiation is by default represented as a BooleanExpression using anonymous variable names x_0 ... x_k (where k is the arity of the uninterpreted function). If you actually want to instantiate the function w.r.t. a set of arguments, specific UpdateFunction, or a parametrized BooleanNetwork, you can use the ColorModel.instantiate method.

def keys(self) -> list[typing.Union[VariableId, ParameterId]]:

The actual "retained" uninterpreted functions in this ColorModel.

This is the list of all ParameterId and VariableId objects that admit an associated uninterpreted function and said function is present in this ColorModel.

def values(self) -> list[BooleanExpression]:

The list of BooleanExpression objects representing the individual uninterpreted functions from ColorModel.keys.

def items( self) -> list[tuple[typing.Union[VariableId, ParameterId], BooleanExpression]]:

The list of key-value pairs represented in this model.

def to_dict( self) -> dict[typing.Union[VariableId, ParameterId], BooleanExpression]:

The same as VertexModel.items, but returns a dictionary instead.

def to_named_dict(self) -> dict[str, BooleanExpression]:

The same as ColorModel.to_dict, but the keys in the dictionary are names, not IDs.

def to_valuation(self) -> BddPartialValuation:

Return the underlying BddPartialValuation for this symbolic model.

def to_symbolic(self) -> ColorSet:

Return a ColorSet where all the implicit and explicit parameters are fixed according to the values in this ColorModel. Parameters that are not present in the ColorModel are unrestricted.

Note that this does not apply any constraints that may be relevant in the AsynchronousGraph that was used to create this model.

def instantiate(self, item, args):

def instantiate(self, item: UpdateFunction) -> UpdateFunction:

def instantiate( self, item: BooleanNetwork, infer_regulations: bool = False) -> BooleanNetwork:

def instantiate( self, item: Union[ParameterId, VariableId, str], args: Sequence[Union[UpdateFunction, Bdd, VariableId, str]]) -> UpdateFunction:

The ColorModel.instantiate method is used to "fill in" the actual implementation of the uninterpreted functions defined in this ColorModel into an object that depends on this implementation.

Specifically, there are three supported modes of operation:

If item is an UpdateFunction, the result is a new UpdateFunction that only depends on network variables and is the interpretation of the original function under this model.
If item is a BooleanNetwork, the result is a new BooleanNetwork where all uninterpreted functions that are retained in this model are instantiated. By default, the new BooleanNetwork has a regulatory graph that is inferred from the update functions (in particular, this removes all unused regulations). If you want to retain the original regulatory graph, use infer_regulations=False (this argument has no effect in the other use cases).
If item identifies an uninterpreted function (by ParameterId, VariableId, or a string name), the method returns an UpdateFunction that is an interpretation of the uninterpreted function with specified args under this model. This is equivalent to computing SymbolicContext.mk_function and then instantiating this function. Note that in this situation, the args argument is required, and it must match the arity of the uninterpreted function.

Note that in some cases, instantiating an UpdateFunction with two different interpretations can lead to the same UpdateFunction. This happens if parts of the function are redundant. For example, f(x) | !f(x) always instantiates to true, regardless of the interpretation of f. Hence, you can assume that while interpretations (i.e. model["f"]) are unique within a set, the instantiations of more complex functions that depend on them are not.

class SpaceSet:

A symbolic representation of a set of "spaces", i.e. hypercubes in the state space of a particular BooleanNetwork.

SpaceSet(ctx: SymbolicSpaceContext, bdd: Bdd)

Normally, a new SpaceSet is derived using a SymbolicSpaceContext. However, in some cases you may want to create it manually from a SymbolicSpaceContext and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid set of spaces.

def cardinality(self) -> int:

Returns the number of spaces that are represented in this set.

def intersect(self, other: SpaceSet) -> SpaceSet:

Set intersection.

def minus(self, other: SpaceSet) -> SpaceSet:

Set difference.

def union(self, other: SpaceSet) -> SpaceSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: SpaceSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single subspace.

def pick_singleton(self) -> SpaceSet:

Deterministically pick a subset of this set that contains exactly a single subspace.

If this set is empty, the result is also empty.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this SpaceSet.

def extend_with_colors(self, set: ColorSet) -> ColoredSpaceSet:

Extend this set of spaces with all the colors from the given set.

This is essentially a cartesian product with the given ColorSet.

def items( self, retained: Optional[Sequence[Union[VariableId, str]]] = None) -> Iterator[SpaceModel]:

Returns an iterator over all sub-spaces in this SpaceSet with an optional projection to a subset of network variables.

When no retained collection is specified, this is equivalent to SpaceSet.__iter__. However, if a retained set is given, the resulting iterator only considers unique valuations for the retained variables. Consequently, the resulting SpaceModel instances will fail with an IndexError if a value of a variable outside the retained set is requested.

def to_vertices(self, ctx: SymbolicSpaceContext) -> VertexSet:

Produce a set of vertices that are contained within the subspaces represented in this set.

def with_all_sub_spaces(self) -> SpaceSet:

Produce a set of spaces that is a superset of this set, and in addition contains all spaces that are a subspace of some item in this set.

def with_all_super_spaces(self) -> SpaceSet:

Produce a set of spaces that is a superset of this set, and in addition contains all spaces that are a super-spaces of some item in this set.

class SpaceModel:

Represents a single space stored in a SpaceSet (or a ColoredSpaceSet), or a projection of said space to the chosen variables.

Behaves like an immutable dictionary: Boolean variable values can be queried using a VariableId, a string name, or a BddVariable. If the value is unconstrained, the result is None. If the variable is projected away, the operation throws an IndexError.

def keys(self) -> list[VariableId]:

The actual "retained" network variables in this model.

This is the list of all network variables if no projection was applied.

def values(self) -> list[typing.Optional[bool]]:

The list of values for individual variables from SpaceModel.keys.

def items(self) -> list[tuple[VariableId, typing.Optional[bool]]]:

The list of key-value pairs represented in this symbolic model.

def to_dict(self) -> dict[VariableId, typing.Optional[bool]]:

The same as SpaceModel.items, but returns a dictionary instead.

def to_named_dict(self) -> dict[str, typing.Optional[bool]]:

The same as SpaceModel.to_dict, but the keys in the dictionary are names, not IDs.

def to_valuation(self) -> BddPartialValuation:

Return the underlying BddPartialValuation for this symbolic model.

def to_symbolic(self) -> SpaceSet:

Return a SpaceSet where all the variables are fixed according to the values in this SpaceModel. Variables that are not present in the SpaceModel are unrestricted, meaning their value can be any of 0, 1, and *.

class ColoredVertexSet:

A symbolic representation of a relation of "coloured vertices", i.e. pairs of vertices (see VertexSet) and colors (see ColorSet).

Together, such pair represents a specific interpretation of network parameters and valuation of network variables.

ColoredVertexSet(ctx: SymbolicContext, bdd: Bdd)

Normally, a new ColoredVertexSet is derived using an AsynchronousGraph. However, in some cases you may want to create it manually from a SymbolicContext and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid colored set of vertices.

def cardinality(self) -> int:

Returns the number of vertex-color pairs that are represented in this set.

def intersect(self, other: ColoredVertexSet) -> ColoredVertexSet:

Set intersection.

def minus(self, other: ColoredVertexSet) -> ColoredVertexSet:

Set difference.

def union(self, other: ColoredVertexSet) -> ColoredVertexSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: ColoredVertexSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single vertex-color pair.

def is_subspace(self) -> bool:

True if this set is a subspace, i.e. it can be expressed using a single conjunctive clause.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def colors(self) -> ColorSet:

Compute the existential projection of this relation to the color component. I.e. returns a set of colors such that for each color, there is at least one vertex-color pair in the original set.

def vertices(self) -> VertexSet:

Compute the existential projection of this relation to the vertex component. I.e. returns a set of vertices such that for each vertex, there is at least one vertex-color pair in the original set.

def intersect_colors(self, colors: ColorSet) -> ColoredVertexSet:

Retain only those vertex-color pairs for which the color is also contained in the given colors set.

def intersect_vertices(self, vertices: VertexSet) -> ColoredVertexSet:

Retain only those vertex-color pairs for which the vertex is also contained in the given vertex set.

def minus_colors(self, colors: ColorSet) -> ColoredVertexSet:

Remove all vertex-color pairs for which the color is present in the given colors set.

def minus_vertices(self, vertices: VertexSet) -> ColoredVertexSet:

Remove all vertex-color pairs for which the vertex is present in the given vertex set.

def pick_color(self) -> ColoredVertexSet:

Pick a subset of this relation such that each color that is in the original relation is only present with a single vertex in the result relation.

I.e. for each color that appears in this set, result.intersect_colors(color) is a singleton.

def pick_vertex(self) -> ColoredVertexSet:

Pick a subset of this relation such that each vertex that is in the original relation is only present with a single color in the result relation.

I.e. for each vertex that appears in this set, result.intersect_vertices(vertex) is a singleton.

def pick_singleton(self) -> ColoredVertexSet:

Deterministically pick a subset of this set that contains exactly a single vertex-color pair.

If this set is empty, the result is also empty.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this ColoredVertexSet.

def items( self, retained_variables: Optional[Sequence[Union[VariableId, str]]] = None, retained_functions: Optional[Sequence[Union[VariableId, ParameterId, str]]] = None) -> Iterator[tuple[ColorModel, VertexModel]]:

Returns an iterator over all interpretation-vertex pairs in this ColoredVertexSet relation, with an optional projection to a subset of network variables and uninterpreted functions.

When no retained collections are specified, this is equivalent to ColoredVertexSet.__iter__. However, if a retained collection is given, the resulting iterator only considers unique combinations of the retained functions and variables. Consequently, the resulting ColorModel and VertexModel instances will fail with an IndexError if a value outside the retained set is requested.

Note that if you set retained_variables = [] and retained_functions = None, this is equivalent to set.colors().items(). Similarly, with retained_variables = None and retained_functions = [], this is equivalent to set.vertices().items().

def to_singleton_spaces(self, ctx: SymbolicSpaceContext) -> ColoredSpaceSet:

Represent this colored set of vertices as a colored set of singleton subspaces instead.

class ColoredSpaceSet:

A symbolic representation of a colored relation of "spaces", i.e. hypercubes in the state space of a particular partially specified BooleanNetwork together with the instantiations of individual interpretations of network parameters.

ColoredSpaceSet(ctx: SymbolicContext, bdd: Bdd)

Normally, a new ColoredSpaceSet is derived using an SymbolicSpaceContext. However, in some cases you may want to create it manually from a SymbolicSpaceContext and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid colored set of vertices.

def cardinality(self) -> int:

Returns the number of space-color pairs that are represented in this set.

def intersect(self, other: ColoredSpaceSet) -> ColoredSpaceSet:

Set intersection.

def minus(self, other: ColoredSpaceSet) -> ColoredSpaceSet:

Set difference.

def union(self, other: ColoredSpaceSet) -> ColoredSpaceSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: ColoredSpaceSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single vertex-color pair.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def colors(self) -> ColorSet:

Compute the existential projection of this relation to the color component. I.e. returns a set of colors such that for each color, there is at least one space-color pair in the original set.

def spaces(self) -> SpaceSet:

Compute the existential projection of this relation to the subspace component. I.e. returns a set of spaces such that for each space, there is at least one space-color pair in the original set.

def intersect_colors(self, colors: ColorSet) -> ColoredSpaceSet:

Retain only those space-color pairs for which the color is also contained in the given colors set.

def intersect_spaces(self, vertices: SpaceSet) -> ColoredSpaceSet:

Retain only those space-color pairs for which the space is also contained in the given spaces set.

def minus_colors(self, colors: ColorSet) -> ColoredSpaceSet:

Remove all space-color pairs for which the color is present in the given colors set.

def minus_spaces(self, vertices: SpaceSet) -> ColoredSpaceSet:

Remove all space-color pairs for which the space is present in the given spaces set.

def pick_color(self) -> ColoredSpaceSet:

Pick a subset of this relation such that each color that is in the original relation is only present with a single vertex in the result relation.

I.e. for each color that appears in this set, result.intersect_colors(color) is a singleton.

def pick_space(self) -> ColoredSpaceSet:

Pick a subset of this relation such that each space that is in the original relation is only present with a single color in the result relation.

I.e. for each space that appears in this set, result.intersect_spaces(space) is a singleton.

def pick_singleton(self) -> ColoredSpaceSet:

Deterministically pick a subset of this set that contains exactly a single space-color pair.

If this set is empty, the result is also empty.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this ColoredSpaceSet.

Returns an iterator over all interpretation-space pairs in this ColoredSpaceSet relation, with an optional projection to a subset of network variables and uninterpreted functions.

When no retained collections are specified, this is equivalent to ColoredSpaceSet.__iter__. However, if a retained collection is given, the resulting iterator only considers unique combinations of the retained functions and variables. Consequently, the resulting ColorModel and SpaceModel instances will fail with an IndexError if a value outside the retained set is requested.

def to_colored_vertices(self, ctx: SymbolicSpaceContext) -> ColoredVertexSet:

Produce a set of vertices that are contained within the subspaces represented in this set.

def with_all_sub_spaces(self) -> ColoredSpaceSet:

Produce a set of spaces that is a superset of this set, and in addition contains all spaces that are a subspace of some item in this set.

Colors are retained on a per-space basis.

def with_all_super_spaces(self) -> ColoredSpaceSet:

Produce a set of spaces that is a superset of this set, and in addition contains all spaces that are a super-spaces of some item in this set.

Colors are retained on a per-space basis.

class AsynchronousGraph:

AsynchronousGraph( network: BooleanNetwork, context: Optional[SymbolicContext] = None, unit_bdd: Optional[Bdd] = None)

A new AsynchronousGraph is constructed from a BooleanNetwork. Optionally, you can also provide a SymbolicContext (that is compatible with said network), or a unit_bdd which restricts the set of vertices and colors of the AsynchronousGraph.

Note that the graph structure is immutable: if you change the original network, you have to create a new AsynchronousGraph.

def mk_for_model_checking( network: BooleanNetwork, requirement: Union[int, str, HctlFormula]) -> AsynchronousGraph:

Create a new AsynchronousGraph whose SymbolicContext contains enough additional symbolic variables to model-check the requirement HCTL formula (or explicit quantified variable count).

This uses the "extra" variables supported by the SymbolicContext object and hence cannot be used with other features that also rely on "extra" variables (like SymbolicSpaceContext).

Note that the symbolic representation in the resulting AsynchronousGraph likely won't be compatible with the "default" AsynchronousGraph either. However, you can translate between these representations using AsynchronousGraph.transfer_from.

def symbolic_context(self) -> SymbolicContext:

The underlying SymbolicContext of this graph.

def network_variable_count(self) -> int:

The number of the network variables (or state variables).

def network_variable_names(self) -> list[str]:

The names of the network variables.

def network_variables(self) -> list[VariableId]:

The VariableId identifiers of the network variables.

def find_network_variable(self, variable: Union[VariableId, str]) -> Optional[VariableId]:

Return a VariableId of the specified network variable, assuming such variable exists.

def get_network_variable_name(self, variable: Union[VariableId, str]) -> str:

The name of a particular network variable.

def reconstruct_network(self) -> BooleanNetwork:

Try to reconstruct the underlying BooleanNetwork from the symbolic functions of this AsynchronousGraph.

This is only possible when the graph does not use any non-trivial uninterpreted functions (i.e. arity more than zero), because there is no suitable way to reconstruct a function expression form a partially specified function. The only exception are implicit parameters (i.e. fully erased functions) that can be reconstructed as well.

def mk_empty_colored_vertices(self) -> ColoredVertexSet:

Return an empty ColoredVertexSet.

def mk_empty_colors(self) -> ColorSet:

Return an empty ColorSet.

def mk_empty_vertices(self) -> VertexSet:

Return an empty VertexSet.

def mk_unit_colored_vertices(self) -> ColoredVertexSet:

Return a "unit" (i.e. full) ColoredVertexSet.

def mk_unit_colors(self) -> ColorSet:

Return a "unit" (i.e. full) ColorSet.

def mk_unit_vertices(self) -> VertexSet:

Return a "unit" (i.e. full) VertexSet.

def mk_function_row_colors( self, function: Union[VariableId, ParameterId, str], row: Sequence[Union[bool, int]], value: Union[bool, int]) -> ColorSet:

Compute the set of colors where the function of the given id outputs the specified value for the given input row.

Note that this does not reflect the static constraints of the underlying network. It simply outputs all functions where given inputs evaluate to the given output.

def mk_function_colors( self, function: Union[VariableId, ParameterId, str], value: Union[Bdd, BooleanExpression, str]) -> ColorSet:

Compute a set of colors that corresponds to the given function interpretation (functions other than id remain unconstrained).

Note that the result of this operation does not have to be a subset of AsynchronousGraph.mk_unit_colors. In other words, this method allows you to also create instances of colors that represent valid functions, but are disallowed by the regulation constraints.

The first argument must identify an unknown function (i.e. explicit or implicit parameter). The second argument then represents a Boolean function of the arity prescribed for the specified unknown function. Such a Boolean function can be represented as:

A BooleanExpression (or a string that parses into a BooleanExpression) which uses only variables x_0 ... x_{A-1} (A being the function arity).
A Bdd that only depends on the first A symbolic variables.

In both cases, the support set of the function can be of course a subset of the prescribed variables (e.g. x_0 | x_3 is allowed for a function with A=4, even though x_1 and x_2 are unused).

def transfer_from(self, set, original_ctx):

def transfer_from( self, set: ColorSet, original_ctx: AsynchronousGraph) -> ColorSet:

def transfer_from( self, set: VertexSet, original_ctx: AsynchronousGraph) -> VertexSet:

def transfer_from( self, set: ColoredVertexSet, original_ctx: AsynchronousGraph) -> ColoredVertexSet:

Transfer a symbolic set (ColorSet, VertexSet, or ColoredVertexSet) from a compatible AsynchronousGraph into the encoding of this graph.

def mk_subspace( self, subspace: Union[Mapping[VariableId, Union[bool, int]], Mapping[str, Union[bool, int]], VertexModel]) -> ColoredVertexSet:

Create a symbolic ColoredVertexSet consisting of unit colors and vertices with the specified variables fixed to their respective values.

def mk_subspace_vertices( self, subspace: Union[Mapping[VariableId, Union[bool, int]], Mapping[str, Union[bool, int]], VertexModel]) -> VertexSet:

Create a symbolic VertexSet of vertices with the specified variables fixed to their respective values.

def mk_update_function(self, variable: Union[VariableId, str]) -> Bdd:

Compute the Bdd representation of the update function that is associated with the given variable.

def post(self, set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct successors of the given set.

def pre(self, set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct predecessors of the given set.

def var_post( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct successors of the given set by updating the specified var.

def var_post_out( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct successors of the given set by updating the specified var that are outside of the given set.

def var_post_within( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct successors of the given set by updating the specified var that are within the given set.

def var_pre( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct predecessors of the given set by updating the specified var.

def var_pre_out( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct predecessors of the given set by updating the specified var that are outside of the given set.

def var_pre_within( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the set of direct predecessors of the given set by updating the specified var that are within the given set.

def can_post(self, set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a successor.

def can_pre(self, set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a predecessor.

def var_can_post( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a successor by updating the variable var.

def var_can_post_out( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a successor by updating the variable var that is outside of the given set.

def var_can_post_within( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a successor by updating the variable var that is within the given set.

def var_can_pre( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a predecessor by updating the variable var.

def var_can_pre_out( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a predecessor by updating the variable var that is outside of the given set.

def var_can_pre_within( self, var: Union[VariableId, str], set: ColoredVertexSet) -> ColoredVertexSet:

Compute the subset of the given set that has a predecessor by updating the variable var that is within the given set.

def inline_variable_symbolic(self, var: Union[VariableId, str]) -> AsynchronousGraph:

Compute a version of the AsynchronousGraph where the specified variable is inlined.

This is similar to BooleanNetwork.inline_variable, but performs the operation symbolically on the Bdd update functions, not syntactically on the UpdateFunction of the BooleanNetwork.

As such, the result is often much smaller than the syntactic inlining. However, the process does not produce an actual BooleanNetwork and is slightly unusual in the context of biodivine_aeon: The new system uses new VariableId identifiers, shifted due to the removed network variable. However, to maintain compatibility with the original AsynchronousGraph, it uses the same underlying BddVariableSet.

In other words, the variable is inlined inside the AsynchronousGraph, but still (theoretically) exists in the symbolic representation, it is just eliminated everywhere, including the SymbolicContext of the AsynchronousGraph.

Currently, variables with a self-regulation cannot be inlined (raised a RuntimeError).

class TrapSpaces:

def essential_symbolic( ctx: SymbolicSpaceContext, graph: AsynchronousGraph, restriction: Optional[ColoredSpaceSet] = None) -> ColoredSpaceSet:

Computes the coloured set of "essential" trap spaces of a Boolean network.

A trap space is essential if it cannot be further reduced through percolation. In general, every minimal trap space is always essential.

def minimal_symbolic( ctx: SymbolicSpaceContext, graph: AsynchronousGraph, restriction: Optional[ColoredSpaceSet] = None) -> ColoredSpaceSet:

Computes the minimal coloured trap spaces of the provided network within the specified restriction set.

Currently, this method always slower than [Self::essential_symbolic], because it first has to compute the essential set.

def minimize( ctx: SymbolicSpaceContext, set: ColoredSpaceSet) -> ColoredSpaceSet:

Compute the inclusion-minimal spaces within a particular subset.

def maximize( ctx: SymbolicSpaceContext, set: ColoredSpaceSet) -> ColoredSpaceSet:

Compute the inclusion-maximal spaces within a particular subset.

class FixedPoints:

def symbolic( graph: AsynchronousGraph, set: Optional[ColoredVertexSet] = None) -> ColoredVertexSet:

Iteratively compute the colored set of fixed-points in an AsynchronousGraph that are the subset of the restriction set.

def symbolic_vertices( graph: AsynchronousGraph, set: Optional[ColoredVertexSet] = None) -> VertexSet:

Iteratively compute the set of fixed-point vertices in an AsynchronousGraph.

This is equivalent to FixedPoints.symbolic(graph, set).vertices(), but can be significantly faster because the projection is applied on-demand within the algorithm.

def symbolic_colors( graph: AsynchronousGraph, set: Optional[ColoredVertexSet] = None) -> ColorSet:

Iteratively compute the set of fixed-point vertices in an AsynchronousGraph.

This is equivalent to FixedPoints.symbolic(graph, set).colors(), but can be significantly faster because the projection is applied on-demand within the algorithm.

class Attractors:

def transition_guided_reduction( graph: AsynchronousGraph, restriction: Optional[ColoredVertexSet] = None, to_reduce: Optional[Sequence[Union[VariableId, str]]] = None) -> ColoredVertexSet:

Compute a subset of the given restriction set that is guaranteed to be a superset of all the attractors within the restriction set.

Note that the attractor property is evaluated globally, not with respect to the restriction set. The restriction set only specifies that the result must be a subset of the input. If no restriction is given, the whole state space is used.

Furthermore, note that the exact characterisation of the set that is retained is a bit complicated. You shouldn't assume that the result is a trap set or that it is forward/backward closed. Just that any attractor that is a subset of restriction is still a subset of the result.

You can limit which variables are reduced using the to_reduce list. For example, for some larger models, it may be sufficient to select a subset of variables.

def xie_beerel( graph: AsynchronousGraph, restriction: Optional[ColoredVertexSet] = None) -> list[ColoredVertexSet]:

Perform attractor detection on the given symbolic set.

This is similar to Attractors.attractors, but it does not perform Attractors.transition_guilded_reduction. Instead, it directly runs the attractor detection algorithm on the restriction set without any preprocessing.

Note that the result is a collection of sets, such that for each set and each color holds that if the color is present in the set, the vertices of this color in the set together form an attractor. It is not guaranteed that this "decomposition" into colored sets is in some sense canonical (but the method should be deterministic). If you only care about attractor states and not individual attractors, you can simply merge all the sets together.

def attractors( graph: AsynchronousGraph, restriction: Optional[ColoredVertexSet] = None, to_reduce: Optional[Sequence[Union[VariableId, str]]] = None) -> list[ColoredVertexSet]:

Compute the (colored) attractor set of the given AsynchronousGraph.

See Attractors.xie_beerel and Attractors.transition_guided_reduction for relevant documentation.

class Percolation:

def percolate_subspace( graph: AsynchronousGraph, subspace: Union[Mapping[VariableId, Union[bool, int]], Mapping[str, Union[bool, int]]]) -> dict[VariableId, bool]:

Performs a percolation of a single subspace.

Percolation propagates the values of variables that are guaranteed to be constant in the given subspace. Note that this function will not overwrite values fixed in the original space if they percolate to a conflicting value. Also note that the result is a subspace of the original space, i.e. it does not just contain the newly propagated variables.

This method should technically work on parametrized networks as well, but the constant check is performed across all interpretations, hence a lot of sub-spaces will not percolate meaningfully. We recommend using other symbolic methods for such systems.

class Reachability:

An "algorithm object" that facilitates reachability procedures, i.e. iterative computation of successors (or predecessors) of a particular symbolic set.

def reach_fwd( graph: AsynchronousGraph, initial: ColoredVertexSet) -> ColoredVertexSet:

Compute the (colored) set of vertices that are forward-reachable from the given initial set.

Note that this method should be faster than just iteratively calling AsynchronousGraph.post as it is based on the saturation technique.

def reach_bwd( graph: AsynchronousGraph, initial: ColoredVertexSet) -> ColoredVertexSet:

Compute the (colored) set of vertices that are backward-reachable from the given initial set.

Note that this method should be faster than just iteratively calling AsynchronousGraph.pre as it is based on the saturation technique.

class RegulationConstraint:

An "algorithm object" that can be used to compute symbolic constraints that correspond to typical properties of model regulations (i.e. monotonicity and essentiality).

However, you can use this to create symbolic constraints for arbitrary symbolic functions, not just the update functions of a BN.

def mk_activation( ctx: SymbolicContext, function: Bdd, variable: Union[VariableId, str]) -> Bdd:

Compute a Bdd which is satisfied exactly by those function interpretations for which the given function is positively monotonous in the specified input variable.

Note that the result only depends on the "parameter" variables of the given SymbolicContext. You can thus directly convert it to a ColorSet by calling ColorSet(context, result).

Also note that (at the moment), the input variable must be one of the network variables. For example, it cannot be one of the extra variables.

You can also use this function to check if a non-parametrized function is monotonous: simply check if the resulting Bdd is a true function.

def mk_inhibition( ctx: SymbolicContext, function: Bdd, variable: Union[VariableId, str]) -> Bdd:

Compute a Bdd which is satisfied exactly by those function interpretations for which the given function is negatively monotonous in the specified input variable.

Note that the result only depends on the "parameter" variables of the given SymbolicContext. You can thus directly convert it to a ColorSet by calling ColorSet(context, result).

Also note that (at the moment), the input variable must be one of the network variables. For example, it cannot be one of the extra variables.

You can also use this function to check if a non-parametrized function is monotonous: simply check if the resulting Bdd is a true function.

def mk_essential( ctx: SymbolicContext, function: Bdd, variable: Union[VariableId, str]) -> Bdd:

Compute a Bdd which is satisfied exactly by those function interpretations for which the given function is has the specified variable as an essential input (i.e. it plays a role in the function's outcome).

Note that the result only depends on the "parameter" variables of the given SymbolicContext. You can thus directly convert it to a ColorSet by calling ColorSet(context, result).

Also note that (at the moment), the input variable must be one of the network variables. For example, it cannot be one of the extra variables.

You can also use this function to check if a non-parametrized function has an essential input: simply check if the resulting Bdd is a true function.

def infer_sufficient_regulation( ctx: SymbolicContext, source: Union[VariableId, str], target: Union[VariableId, str], function: Bdd) -> Optional[IdRegulation]:

This method takes a symbolic (parametrized) function and two network variables (source and target).

It assumes the symbolic function represents the update function of the target variable. It then tries to infer the most specific IdRegulation that is valid for every interpretation of the provided function.

If the function is not parametrized, this simply infers the monotonicity and essentiality of source in the given function.

Note that the function returns None if no interpretation of the function depends on source. It returns essential=False only when the function has more than one interpretation, such that some depend on source, but not all.

class HctlFormula:

Represents the syntax tree of a HCTL formula.

The string format for representing these formulas is available on the repository site of the original Rust library.

Note that this format uses ~ instead of ! to represent negation (compared to other expression formats used in AEON).

HctlFormula( formula: str | HctlFormula, allow_extended: bool = True, minimize_with: Optional[SymbolicContext] = None)

Create a new HctlFormula, either parsing it from a string, or as a copy of an existing formula.

If allow_extended is specified, the parser will also recognize "extended" propositions (denoted %prop%) that can be used to reference pre-computed symbolic sets.

If minimize_with is specified with a SymbolicContext, the created formula is automatically converted to a canonical format, using standardized variable names and removing redundancies (for this, a SymbolicContext is required in order to check the mapping between hybrid state variables and their symbolic representation).

def mk_hybrid( op: Literal['exists', 'forall', 'bind', 'jump'], state_variable: str, inner: HctlFormula, domain: str | None = None) -> HctlFormula:

Create a new HctlFormula that uses a hybrid operator (see also HybridOperator).

Optionally, you can provide a named domain which further restricts the validity of the operator. Note that such formulas have separate pattern matching methods (e.g. HctlFormula.is_hybrid_in instead of HctlFormula.is_hybrid).

def mk_exists( state_variable: str, inner: HctlFormula, domain: str | None = None) -> HctlFormula:

Create a new HctlFormula that uses the 3{x} operator.

Optionally, you can provide a named domain which further restricts the validity of the operator (i.e. it creates the 3{x} in %domain% operator). Note that such formulas have separate pattern matching methods (e.g. HctlFormula.is_exists_in instead of HctlFormula.is_exists).

def mk_forall( state_variable: str, inner: HctlFormula, domain: str | None = None) -> HctlFormula:

Create a new HctlFormula that uses the V{x} operator.

Optionally, you can provide a named domain which further restricts the validity of the operator (i.e. it creates the V{x} in %domain% operator). Note that such formulas have separate pattern matching methods (e.g. HctlFormula.is_forall_in instead of HctlFormula.is_forall).

def mk_bind( state_variable: str, inner: HctlFormula, domain: str | None = None) -> HctlFormula:

Create a new HctlFormula that uses the !{x} operator.

Optionally, you can provide a named domain which further restricts the validity of the operator (i.e. it creates the !{x} in %domain% operator). Note that such formulas have separate pattern matching methods (e.g. HctlFormula.is_forall_in instead of HctlFormula.is_forall).

def mk_jump(state_variable: str, inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the @{x} operator.

def mk_temporal(op, a, b):

def mk_temporal( op: Literal['exist_next', 'all_next', 'exist_future', 'all_future', 'exist_global', 'all_global'], a: HctlFormula) -> HctlFormula:

def mk_temporal( op: Literal['exist_until', 'all_until', 'exist_weak_until', 'all_weak_until'], a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses a temporal operator (see TemporalUnaryOperator and TemporalBinaryOperator).

For unary operators, provide only one HctlFormula. For binary operators, provide both formulas.

def mk_boolean( op: Literal['and', 'or', 'imp', 'iff', 'xor'], a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses a binary Boolean operator (see BinaryOperator).

def mk_not(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the ~ operator.

def mk_and(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the & operator.

def mk_or(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the | operator.

def mk_imp(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the => operator.

def mk_iff(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the <=> operator.

def mk_xor(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the ^ operator.

def mk_exist_next(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the EX operator.

def mk_all_next(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the AX operator.

def mk_exist_future(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the EF operator.

def mk_all_future(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the AF operator.

def mk_exist_global(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the EG operator.

def mk_all_global(inner: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the AG operator.

def mk_exist_until(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the EU operator.

def mk_all_until(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the AU operator.

def mk_exist_weak_until(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the EW operator.

def mk_all_weak_until(a: HctlFormula, b: HctlFormula) -> HctlFormula:

Create a new HctlFormula that uses the AW operator.

def mk_state_var(name: str) -> HctlFormula:

Create a new HctlFormula that represents a quantified state variable.

def mk_network_var(name: str) -> HctlFormula:

Create a new HctlFormula that represents a network variable proposition.

def mk_const(value: bool) -> HctlFormula:

Create a new HctlFormula that represents a Boolean constant.

def mk_extended_prop(name: str) -> HctlFormula:

Create a new HctlFormula that represents an extended proposition.

def is_hybrid(self) -> bool:

Check if this HctlFormula represents on of the hybrid operators without a domain restriction (see HybridOperator).

def is_hybrid_in(self) -> bool:

Check if this HctlFormula represents on of the hybrid operators with a domain restriction (see HybridOperator).

def is_temporal(self) -> bool:

Check if this HctlFormula represents on of the temporal operators (see TemporalUnaryOperator and TemporalBinaryOperator).

def is_temporal_unary(self) -> bool:

Check if this HctlFormula represents on of the unary temporal operators (see TemporalUnaryOperator).

def is_temporal_binary(self) -> bool:

Check if this HctlFormula represents on of the binary temporal operators (see TemporalBinaryOperator).

def is_boolean(self) -> bool:

Check if this HctlFormula represents on of the binary Boolean operators (see BinaryOperator).

def is_state_var(self) -> bool:

Check if this HctlFormula represents a quantified state proposition.

def is_network_var(self) -> bool:

Check if this HctlFormula represents a network variable proposition.

def is_const(self) -> bool:

Check if this HctlFormula represents a constant.

def is_extended_prop(self) -> bool:

Check if this HctlFormula represents an extended proposition.

def is_exists(self) -> bool:

Check if this HctlFormula represents the 3{x} operator.

def is_exists_in(self) -> bool:

Check if this HctlFormula represents the 3{x} in %domain% operator.

def is_forall(self) -> bool:

Check if this HctlFormula represents the V{x} operator.

def is_forall_in(self) -> bool:

Check if this HctlFormula represents the V{x} in %domain% operator.

def is_bind(self) -> bool:

Check if this HctlFormula represents the !{x} operator.

def is_bind_in(self) -> bool:

Check if this HctlFormula represents the !{x} in %domain% operator.

def is_jump(self) -> bool:

Check if this HctlFormula represents the @{x} operator.

def is_not(self) -> bool:

Check if this HctlFormula represents the ~ operator.

def is_and(self) -> bool:

Check if this HctlFormula represents the & operator.

def is_or(self) -> bool:

Check if this HctlFormula represents the | operator.

def is_imp(self) -> bool:

Check if this HctlFormula represents the => operator.

def is_iff(self) -> bool:

Check if this HctlFormula represents the <=> operator.

def is_xor(self) -> bool:

Check if this HctlFormula represents the ^ (xor) operator.

def is_exist_next(self) -> bool:

Check if this HctlFormula represents the EX operator.

def is_all_next(self) -> bool:

Check if this HctlFormula represents the AX operator.

def is_exist_future(self) -> bool:

Check if this HctlFormula represents the EF operator.

def is_all_future(self) -> bool:

Check if this HctlFormula represents the AF operator.

def is_exist_global(self) -> bool:

Check if this HctlFormula represents the EG operator.

def is_all_global(self) -> bool:

Check if this HctlFormula represents the AG operator.

def is_exist_until(self) -> bool:

Check if this HctlFormula represents the EU operator.

def is_all_until(self) -> bool:

Check if this HctlFormula represents the AU operator.

def is_exist_weak_until(self) -> bool:

Check if this HctlFormula represents the EW operator.

def is_all_weak_until(self) -> bool:

Check if this HctlFormula represents the AW operator.

def as_hybrid( self) -> Optional[tuple[Literal['exists', 'forall', 'bind', 'jump'], str, HctlFormula]]:

Return the operator, variable and argument if this HctlFormula represents a hybrid operator without domain restriction.

def as_hybrid_in( self) -> Optional[tuple[Literal['exists', 'forall', 'bind', 'jump'], str, str, HctlFormula]]:

Return the operator, variable, domain and argument if this HctlFormula represents a hybrid operator with domain restriction.

def as_temporal_unary( self) -> Optional[tuple[Literal['exist_next', 'all_next', 'exist_future', 'all_future', 'exist_global', 'all_global'], HctlFormula]]:

Return the operator and argument if this HctlFormula represents a unary temporal operator.

def as_temporal_binary( self) -> Optional[tuple[Literal['exist_until', 'all_until', 'exist_weak_until', 'all_weak_until'], HctlFormula, HctlFormula]]:

Return the operator and arguments if this HctlFormula represents a binary temporal operator.

def as_boolean( self) -> Optional[tuple[Literal['and', 'or', 'imp', 'iff', 'xor'], HctlFormula, HctlFormula]]:

Return the operator and arguments if this HctlFormula represents a binary Boolean operator.

def as_state_var(self) -> Optional[str]:

Return the variable name if this HctlFormula represents a state variable proposition.

def as_network_var(self) -> Optional[str]:

Return the variable name if this HctlFormula represents a network variable proposition.

def as_const(self) -> Optional[bool]:

Return the Boolean value if this HctlFormula represents a constant.

def as_extended_prop(self) -> Optional[str]:

Return the property name if this HctlFormula represents an extended proposition (%name%).

def as_exists(self) -> Optional[tuple[str, HctlFormula]]:

Return the state variable name and the child formula if this HctlFormula represents the 3{x} hybrid operator.

(This method returns None if the formula represents the 3{x} in %domain% operator.)

def as_exists_in(self) -> Optional[tuple[str, str, HctlFormula]]:

Return the state variable name, domain name, and the child formula if this HctlFormula represents the 3{x} in %domain% hybrid operator.

def as_forall(self) -> Optional[tuple[str, HctlFormula]]:

Return the state variable name and the child formula if this HctlFormula represents the V{x} hybrid operator.

(This method returns None if the formula represents the V{x} in %domain% operator.)

def as_forall_in(self) -> Optional[tuple[str, str, HctlFormula]]:

Return the state variable name, domain name, and the child formula if this HctlFormula represents the V{x} in %domain% hybrid operator.

def as_bind(self) -> Optional[tuple[str, HctlFormula]]:

Return the state variable name and the child formula if this HctlFormula represents the !{x} hybrid operator.

(This method returns None if the formula represents the !{x} in %domain% operator.)

def as_bind_in(self) -> Optional[tuple[str, str, HctlFormula]]:

Return the state variable name, domain name, and the child formula if this HctlFormula represents the !{x} in %domain% hybrid operator.

def as_jump(self) -> Optional[tuple[str, HctlFormula]]:

Return the state variable name and the child formula if this HctlFormula represents the @{x} hybrid operator.

def as_not(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the ~ operator.

def as_and(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the & Boolean operator.

def as_or(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the | Boolean operator.

def as_imp(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the => Boolean operator.

def as_iff(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the <=> Boolean operator.

def as_xor(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the ^ Boolean operator.

def as_exist_next(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the EX temporal operator.

def as_all_next(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the AX temporal operator.

def as_exist_future(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the EF temporal operator.

def as_all_future(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the AF temporal operator.

def as_exist_global(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the EG temporal operator.

def as_all_global(self) -> Optional[HctlFormula]:

Return the child formula if this HctlFormula represents the AG temporal operator.

def as_exist_until(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the EU temporal operator.

def as_all_until(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the AU temporal operator.

def as_exist_weak_until(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the EW temporal operator.

def as_all_weak_until(self) -> Optional[tuple[HctlFormula, HctlFormula]]:

Return the two child formulas if this HctlFormula represents the AW temporal operator.

def is_compatible_with(self, context: AsynchronousGraph) -> bool:

Returns True if the provided AsynchronousGraph has enough extra symbolic variables such that it can be used to model-check this HctlFormula.

def used_state_variables(self) -> set[str]:

Returns the set of HCTL state variables that are used in this formula.

def used_extended_properties(self) -> set[str]:

Returns the set of extended property names and domain names that are used in this formula.

def children(self) -> list[HctlFormula]:

Return the direct child sub-formulas of this HctlFormula (one child for unary and hybrid operators, two children for binary operators, no children for atoms).

For binary operators, the left-most child is returned first.

def operator( self) -> Union[Literal['not'], Literal['and', 'or', 'imp', 'iff', 'xor'], Literal['exist_until', 'all_until', 'exist_weak_until', 'all_weak_until'], Literal['exist_next', 'all_next', 'exist_future', 'all_future', 'exist_global', 'all_global'], Literal['exists', 'forall', 'bind', 'jump'], NoneType]:

Return the string representation of the operator used by this HctlFormula, or None if this is an atom.

class ModelChecking:

def verify(graph, property, substitution):

def verify( graph: AsynchronousGraph, property: str | HctlFormula, substitution: Optional[dict[str, ColoredVertexSet]] = None) -> ColoredVertexSet:

def verify( graph: AsynchronousGraph, properties: Sequence[str | HctlFormula], substitution: Optional[dict[str, ColoredVertexSet]] = None) -> list[ColoredVertexSet]:

Verify the provided HCTL formula or formulas, returning the vertex-color pairs for which the property holds.

The property argument can be either a single formula (str or HctlFormula), in which case the result is a single ColoredVertexSet. Alternatively, you can provide a list of formulas, in which case the result is a list[ColoredVertexSet].

If the formulas contain extended propositions or quantifier domains, you should provide a substitution map which assigns each proposition a set of valid vertex-color pairs (the algorithm fails if the used extended propositions cannot be resolved).

The following only applies to HCTL formulas that use quantified state variables (i.e. "plain" CTL formulas do not need this):

Note that the provided AsynchronousGraph must contain enough symbolic variables to successfully represent all quantified variables in the provided formulae. You can create such graph using AsynchronousGraph.mk_for_model_checking, or by manually creating enough extra symbolic variables for each variable in the SymbolicContext.

The resulting ColoredVertexSet uses the symbolic encoding of the provided AsynchronousGraph that supports the extra symbolic variables necessary for model checking. If you want to output the result in a way that is compatible with the "default" AsynchronousGraph representation (i.e. AsynchronousGraph(network)), you can use AsynchronousGraph.transfer_from to translate the sets into the "default" symbolic encoding.

class Class:

A Class is an immutable collection of sorted "features", such that each feature is a described by its string name. A Class is used by the various classification workflows in AEON to label a specific mode of behavior that a system can exhibit.

Depending on which operations are used, a class can behave either as a set (each feature can only appear once in a Class), or a list (multiple features of the same name appear multiple times). This entirely depends on the classification workflow used and is not a property of a Class itself (you can even mix the set and list behavior depending on the exact feature you are adding). Note that an "empty" class is allowed.

The main reason why we even need Class is that lists and sets are not hash-able in Python, hence we can't use them as keys in dictionaries. Because Class is immutable, it has a stable hash and is safe to use as a dictionary key.

Class(items: str | list[str] | set[str])

Create a Class from a list of string features.

The items are sorted, but duplicates are not removed.

def feature_set(self) -> set[str]:

Return the set of unique features that appear in this Class.

def feature_list(self) -> list[str]:

Return the list of features, including duplicates, that appear in this Class.

def feature_count(self, feature: str) -> int:

Count the number of times a given feature appears in this Class.

def ensure(self, features: Union[str, Sequence[str], Class]) -> Class:

Create a Class instance that extends this class with the given feature (or features). If an added feature already exists (at least once), it is not added again.

def append(self, features: Union[str, Sequence[str], Class]) -> Class:

Create a Class instance where the given feature (or features) is added. If an added feature already exists, it is added again.

def erase(self, features: Union[str, Sequence[str], Class]) -> Class:

Create a Class with all occurrences of a particular feature (or features) removed.

def minus(self, features: Union[str, Sequence[str], Class]) -> Class:

Create a Class with the given feature (or features) removed. Only the specific provided number of occurrences is removed.

class Classification:

An "algorithm object" that groups all methods related to the classification of various model properties.

def ensure( classification: dict[Class, ColorSet], features: Class, colors: ColorSet) -> dict[Class, ColorSet]:

Extend an existing classification dictionary in such a way that every color in the colors set appears in a Class with the specified features.

For example: Extending { ['a']: [1,2,3], ['b']: [4,5,6] } with 'a': [3,4] results in {a: [1,2,3], ['b']: [5,6], ['a','b']: [4] }.

This does not "increase" the number of times a feature appears in a class, it merely creates new classes if the feature is not present.

def append( classification: dict[Class, ColorSet], features: Class, colors: ColorSet) -> dict[Class, ColorSet]:

Extend an existing classification dictionary in such a way that every color in the colors set has an additional features according to the specified Class.

For example: Extending { ['a']: [1,2,3], ['b']: [4,5,6] } with 'a': [3,4] results in {a: [1,2], ['b']: [5,6], ['a','a']: [3], ['a','b']: [4] }.

In other words, compared to Class.classification_ensure, this does "increase" the number of times a feature appears in a class.

def read_dynamic_assertions(source: str | ModelAnnotation) -> list[str]:

Read the list of dynamic assertions from .aeon model annotations.

An assertion typically encodes a HctlFormula that must be satisfied by all the relevant interpretations of a partially specified model.

The argument is either a ModelAnnotation dictionary, a path to an existing model file from which the annotations are extracted, or a multi-line string content that directly represents the annotations.

Assertions appear as a #! dynamic_assertion: CONTENT annotation comments in the .aeon file.

def read_dynamic_properties(source: str | ModelAnnotation) -> list[tuple[str, str]]:

Read the list of dynamic properties from .aeon model annotations.

A property typically encodes a HctlFormula that is of interest in a particular model, but is not necessarily satisfied by all relevant interpretations of a model. Each property is identified by a name (first item in the tuple).

The argument is either a ModelAnnotation dictionary, or a path to an existing model file from which the annotations are extracted, or a multi-line string content that directly represents the annotations.

Properties appear as a #! dynamic_property: NAME: CONTENT annotation comments in the .aeon file.

def write_dynamic_assertions(annotations: ModelAnnotation, assertions: list[str]):

Write the provided dynamic assertions into a ModelAnnotation dictionary. Note that this method does not modify any assertions that may already exist in the annotation dictionary.

Assertions appear as a #! dynamic_assertion: CONTENT annotation comments in the .aeon file.

def write_dynamic_properties(annotations: ModelAnnotation, properties: list[tuple[str, str]]):

Write the provided dynamic properties into a ModelAnnotation dictionary. Note that this method does not modify any properties that may already exist in the annotation dictionary. If a property of the same name already exists, the method fails with a RuntimeError.

Properties appear as a #! dynamic_property: NAME: CONTENT annotation comments in the .aeon file.

def save_classification( path: str, network: BooleanNetwork, classification: dict[Class, ColorSet], annotations: Optional[ModelAnnotation] = None):

Save the classification results into a .zip archive that can be analyzed by the BN Classifier.

The annotations dictionary is optional. If these include the HCTL properties and assertions that were used to create the classification dictionary, then the BN Classifier will be able to show the exact properties in the UI. Otherwise, names of the classes will be used.

Note that this method will automatically sanitize the ColorSet objects such that they use the "default" symbolic encoding for the provided network.

def load_classification( path: str) -> tuple[BooleanNetwork, dict[Class, ColorSet], ModelAnnotation]:

Load a BN Classifier archive into a usable representation. The result includes:

The original BooleanNetwork for which the classification is valid.
A classification mapping from (collections of) properties to sets of network interpretations.
A ModelAnnotation object that can (optionally) contain the properties that were used to generate the classification.

def classify_long_term_behavior( graph: AsynchronousGraph, component: ColoredVertexSet) -> dict[Class, ColorSet]:

Classify the interpretations (colors) of the provided component based on their long-term behavior. That is:

stable: the component is a single state;
cycle: all states in the component form a single (deterministic) cycle (each state has exactly one successor).
complex: any other set of states that has a non-trivial structure.

Note that this method is primarily intended to be used with attractors, but can be (in theory) also applied to any colored set of vertices. However, in such case, the result will typically be the complex behavior class.

However, the properties described above are only tested in a subgraph induced by the vertices in the given component. Hence, you can use the method to at least distinguish between cycles and other complex components, or to quickly identify colors for which a component is trivial (i.e. stable).

def classify_attractor_bifurcation( graph: AsynchronousGraph, attractor: Optional[list[ColoredVertexSet]] = None) -> dict[Class, ColorSet]:

Perform a full classification of attractor behavior in the given AsynchronousGraph.

This is a generalization of Classification.classify_long_term_behavior in the sense that the result covers all attractors, not just one component. Note that the Class instances produced by this process count the number of attractors of each behavior type.

If attractors are already known, or you wish to only consider a subset of attractors, you can provide them through the optional attractors argument.

Note that you can achieve similar results using Classification.classify_long_term_behavior and Classification.ensure (or Classification.append). However, this process is not limited to attractors and can be potentially combined with other features (like HCTL properties).

def classify_attractor_phenotypes( graph: AsynchronousGraph, phenotypes: dict[Class, VertexSet], oscillation_types: Optional[dict[Class, Literal['required', 'allowed', 'forbidden']]] = None, traps: Optional[list[ColoredVertexSet]] = None, count_multiplicity: bool = True) -> dict[Class, ColorSet]:

Classify the individual attractors of an AsynchronousGraph according to their affinity to biological phenotypes.

This is similar to Classification.classify_phenotypes, but it actually returns per-attractor results instead of lumping all attractors of one phenotype into a single class. This results in a sort-of nested classification, where each class consists of entries for individual attractors, but each entry is itself a class that describes the phenotypes of that particular attractor.

For example, given phenotypes "a" and "b", the result could contain a class Class(["Class(['a'])", "Class(['b'])", "Class(['a', 'b'])"]). This means that there are three attractors: One with only the "a" phenotype, one with only the "b" phenotype, and one with both phenotypes. Note that the "inner" classes are encoded as strings (you can convert such string into a proper class object by running c = eval(class_string)).

The meaning of oscillation_types is the same as in Classification.classify_phenotypes: Forbidden oscillation means the attractor must be a subset of the phenotype, allowed oscillation means the attractor must intersect the phenotype, and required oscillation means that the attractor must intersect the phenotype, but can't be its subset.

Similar to Classification.classify_phenotypes, the method allows you to provide a collection of traps that will be considered instead of the network attractors. The method checks that these sets are indeed trap sets, but they do not have to be minimal (i.e. attractors). If traps are given, the classification treats each trap set as a separate "attractor".

Finally, if count_multiplicity is set to False, the method will lump together attractors that satisfy the same phenotypes, meaning the resulting Class object will only contain up to one instance of the same phenotype configuration. For example, if I have two attractors, each satisfying phenotype "a", then by default the result is a Class(["Class(['a'])", "Class(['a'])"]) (and this situation is different compared to the case when I only have one such attractor). If I set count_multiplicity=False, the result will be Class(["Class(['a'])"]), regardless of how many attractors actually satisfy the "a" phenotype.

def classify_phenotypes( graph: AsynchronousGraph, phenotypes: dict[Class, VertexSet], oscillation_types: Optional[dict[Class, Literal['required', 'allowed', 'forbidden']]] = None, initial_trap: Optional[ColoredVertexSet] = None) -> dict[Class, ColorSet]:

Classify the colors of an AsynchronousGraph according to their affinity to biological phenotypes.

Each phenotype is given as an arbitrary VertexSet, identified by a Class instance. Most often, phenotypes are described through pair-wise disjoint sub-spaces (see also AsynchronousGraph.mk_subspace_vertices). The result of this method then associates each network color with a collection of phenotypes (i.e. Class) that are attainable in the corresponding fully instantiated network.

By default, the network exhibits a phenotype if it can stay in the phenotype set forever (i.e. there exists at least one attractor that is fully in this set). However, we also allow other types of phenotypes based on the PhenotypeOscillation:

[default] forbidden: There exists an attractor that is a subset of the given phenotype VertexSet (oscillation is forbidden).
required: There exists an attractor that intersects the phenotype set, but is not a proper subset (phenotype is visited intermittently).
allowed: There exists an attractor that intersects the phenotype set, but can be also a proper subset (i.e. the network either stays in the phenotype forever, or visits it intermittently, we don't care which one).

Colors that do not match any phenotype are returned with an empty class (i.e. Class([])).

Note that this method does not count the number of attractors, and it can assign the same attractor to multiple phenotypes (for example, a network with a fixed-point 111 exhibits both phenotype a=11* and b=*11, i.e. the network will be returned within the class Class(['a','b'])). This is usually not a problem for disjoint phenotypes with forbidden oscillation, just beware that for more complex phenotypes, you might need additional analysis of the relevant colors.

If you do also need to map attractors to phenotypes, have a look at Classification.classify_attractor_phenotypes.

You can (optionally) provide your own attractor states (or any other relevant set of states) as the initial_trap argument (the method assumes this is a trap set). However, computing phenotype classification does not require precise knowledge of attractors. Thus, it can be often much faster than exact attractor computation (especially if the number of attractors is high). However, you can use this option to restrict the input space if you want to explicitly ignore certain parts of the state space.

You can also combine the results of this analysis with other classifications (e.g. attractor bifurcations, or HCTL properties) using Classification.ensure or Classification.append.

def classify_dynamic_properties( graph: AsynchronousGraph, properties: dict[str, HctlFormula], assertions: Optional[list[HctlFormula]] = None, substitution: Optional[dict[str, ColoredVertexSet]] = None) -> dict[Class, ColorSet]:

Classify the behavior of the given graph based on the specified HctlFormula properties.

Optionally, you can also give a collection of assertions that restrict the applicable graph colors.

Note that this method internally creates a dedicated AsynchronousGraph with enough symbolic variables to check all the provided properties/assertions. However, the results are always transformed back into an encoding that is valid for the graph that is given as the first argument.

class AsynchronousPerturbationGraph(AsynchronousGraph):

An extension of AsynchronousGraph that admits various variable perturbations through additional colors/parameters. Such graph can then be analyzed to extract control strategies (perturbations) that are sufficient to achieve a particular outcome (an attractor or a phenotype).

This representation is similar to SymbolicSpaceContext in the sense that it introduces additional variables into the symbolic encoding in order to encode more complex modes of behavior in a BN. However, in this case, it is also necessary to modify the actual update functions of the network. Hence, this implementation extends the AsynchronousGraph directly.

To represent perturbations, AsynchronousPerturbedGraph introduces the following changes to the network dynamics:

For each variable (that can be perturbed), we create an explicit Boolean "perturbation parameter".
Implicit parameters are given explicit names, since we may need to augment the update functions of these variables with perturbation parameters.
We maintain two versions of network dynamics: original (unperturbed), meaning the additional parameters have no impact on the update functions, and perturbed, where a variable is allowed to evolve only if it is not perturbed.
This representation allows us to also encode sets of perturbations, since for a perturbed variable, we can use the state variable (that would otherwise be unused) to represent the value to which the variable is perturbed.

Note that this encoding does not implicitly assume any perturbation temporality (one-step, permanent, temporary). These aspects are managed by the analysis algorithms.

By default, PerturbationAsynchronousGraph behaves as if all variables are unperturbed and the newly introduced parameters are set to False, i.e. unperturbed. The perturbation parameters always appear in the symbolic encoding, they are just not considered in the update functions. To access the "perturbed" dynamics, see AsynchronousPerturbationGraph.to_perturbed.

AsynchronousPerturbationGraph( network: BooleanNetwork, perturb: Optional[Sequence[Union[VariableId, str]]] = None)

Build a new AsynchronousPerturbationGraph for the given BooleanNetwork. Optionally also specify a list of variables that can be perturbed in the resulting graph (otherwise all variables can be perturbed).

def reconstruct_network(self) -> BooleanNetwork:

Reconstruct the BooleanNetwork that represents the unperturbed dynamics of this graph. The network does not contain any perturbation parameters.

def mk_unit_colored_vertices(self) -> ColoredVertexSet:

Return a "unit" (i.e. full) ColoredVertexSet, with the perturbation parameters all fixed to False.

def mk_unit_colors(self) -> ColorSet:

Return a "unit" (i.e. full) ColorSet, with the perturbation parameters all fixed to False.

def mk_function_row_colors( self, function: Union[VariableId, ParameterId, str], row: Sequence[Union[bool, int]], value: Union[bool, int]) -> ColorSet:

A version of AsynchronousGraph.mk_function_row_colors that also fixes the perturbation parameters for False.

def mk_function_colors( self, function: Union[VariableId, ParameterId, str], value: Union[Bdd, BooleanExpression, str]) -> ColorSet:

A version of AsynchronousGraph.mk_function_colors that also fixes the perturbation parameters for False.

def mk_subspace( self, subspace: Union[Mapping[VariableId, Union[bool, int]], Mapping[str, Union[bool, int]], VertexModel]) -> ColoredVertexSet:

A version of AsynchronousGraph.mk_subspace that also fixes the perturbation parameters for False.

def base_network(self) -> BooleanNetwork:

A copy of the base BooleanNetwork that was used to create this graph, without additional perturbation parameters or any modification (e.g. still with all implicit parameters).

def unperturbed_network(self) -> BooleanNetwork:

A copy of the BooleanNetwork with the extra perturbation parameters, but with the update functions unaffected.

def perturbed_network(self) -> BooleanNetwork:

A copy of the BooleanNetwork with the extra perturbation parameters and with the update functions changed to reflect the perturbations.

def to_original(self) -> AsynchronousGraph:

A copy of the AsynchronousGraph that represents the unperturbed asynchronous dynamics of this network. It supports the additional parameters necessary to represent perturbations, but does not actually use them in any meaningful way.

This is effectively the "parent" implementation of this instance, so you can already access these methods directly by calling them on this graph. Just keep in mind that methods that return color sets do not fix the perturbation parameters to False in the "parent" implementation.

def to_perturbed(self) -> AsynchronousGraph:

A copy of the AsynchronousGraph that represents the perturbed asynchronous dynamics of this network. It supports the additional parameters necessary to represent perturbations, and they do affect the state-transitions: In colors where a variable is perturbed, it cannot be updated.

def perturbable_network_variables(self) -> list[VariableId]:

List of variables that can be perturbed in this graph.

def perturbable_network_variable_names(self) -> list[str]:

List of names of variables that can be perturbed in this graph.

def get_perturbation_parameter(self, variable: Union[VariableId, str]) -> ParameterId:

Find the ParameterId which corresponds to the synthetic parameter that is used to encode that the given variable is perturbed (i.e. fixed and cannot evolve).

def perturbation_parameters(self) -> list[ParameterId]:

The list of ParameterId objects that identify the perturbation parameters of this graph.

def perturbation_bdd_variables(self) -> dict[VariableId, BddVariable]:

The dictionary of all VariableId, BddVariable identifier pairs that correspond to the symbolic encoding of perturbation parameters of the respective network variables.

def post_via_perturbation( self, source: list[bool], target: ColoredVertexSet) -> ColoredPerturbationSet:

Compute the ColoredPerturbationSet which causes the network to go from the source state into one of the target states.

In other words, if you fix all the variables prescribed by one of the resulting perturbations in the source state, you obtain one of the target states.

This operation is mostly used internally in various control algorithms.

def mk_unit_perturbations(self) -> PerturbationSet:

Return the set of all perturbations that are valid in this graph.

def mk_empty_perturbations(self) -> PerturbationSet:

Return an empty set of perturbations.

def mk_unit_colored_perturbations(self) -> ColoredPerturbationSet:

Return the set of all perturbation-color pairs that are valid in this graph.

def mk_empty_colored_perturbations(self) -> ColoredPerturbationSet:

Return an empty set of color-perturbation pairs.

def mk_perturbable_unit_colors(self) -> ColorSet:

Create a ColorSet with unconstrained perturbation parameters, meaning every variable that is declared as perturbable can be actually perturbed.

Meanwhile, AsynchronousPerturbationGraph.mk_unit_colors returns a color set where perturbation parameters are set to False to better resemble the behavior of a "normal" AsynchronousGraph.

def mk_perturbable_unit_colored_vertices(self) -> ColoredVertexSet:

Create a ColoredVertexSet with unconstrained perturbation parameters, meaning every variable that is declared as perturbable can be actually perturbed.

Meanwhile, AsynchronousPerturbationGraph.mk_unit_colored_vertices returns a color set where perturbation parameters are set to False to better resemble the behavior of a "normal" AsynchronousGraph.

def mk_perturbation( self, perturbation: Union[Mapping[Union[VariableId, str], Optional[bool]], PerturbationModel]) -> PerturbationSet:

Create a singleton PerturbationSet based on the given values of perturbable variables.

The difference between this method and AsynchronousPerturbationGraph.mk_perturbations is in how missing values are treated: In mk_perturbations, a variable with an unspecified value is treated as unconstrained: i.e. it can be unperturbed, or perturbed to False/True. Meanwhile, mk_perturbation treats any unspecified value as unperturbed, since the result must always represent a single perturbation.

def mk_perturbations( self, perturbations: Union[Mapping[Union[VariableId, str], Optional[bool]], PerturbationModel]) -> PerturbationSet:

Create a set of perturbations that match the given dictionary of values.

The dictionary should contain True/False for a perturbed variable and None for an unperturbed variable. If all perturbable variables are specified, the result is a singleton set. If some of the perturbable variables is missing from the dictionary, it is unconstrained and the result contains any perturbation that matches the description w.r.t. the remaining (specified) variables.

def mk_perturbations_with_size(self, size: int, up_to: bool) -> PerturbationSet:

Create a set of perturbations of the given exact size (in terms of perturbed variables). If size is greater or equal to the number of perturbable variables, the result is equivalent to AsynchronousPerturbationGraph.mk_unit_perturbations.

If the up_to parameter is given, the result contains all perturbations up to (including) the specified size.

def colored_robustness(self, set: ColorSet) -> float:

Compute the robustness of the given color set w.r.t. the unit color set.

Note that this is essentially just set.cardinality() / unit.cardinality() with some additional measures taken to prevent floating point overflow with large numbers.

Inherited Members

AsynchronousGraph: mk_for_model_checking; symbolic_context; network_variable_count; network_variable_names; network_variables; find_network_variable; get_network_variable_name; mk_empty_colored_vertices; mk_empty_colors; mk_empty_vertices; mk_unit_vertices; transfer_from; mk_subspace_vertices; mk_update_function; post; pre; var_post; var_post_out; var_post_within; var_pre; var_pre_out; var_pre_within; can_post; can_pre; var_can_post; var_can_post_out; var_can_post_within; var_can_pre; var_can_pre_out; var_can_pre_within; inline_variable_symbolic

class PerturbationModel:

Represents a single perturbation stored in a PerturbationSet (or a ColoredPerturbationSet), or a projection of said perturbation to the chosen variables.

Behaves like an immutable dictionary: Boolean variable values can be queried using a VariableId, a string name, or a BddVariable. Values that are perturbable but not perturbed return None, while values that are not perturbable raise a KeyError exception.

def keys(self) -> list[VariableId]:

The actual "retained" network variables in this model.

This is the list of all network variables if no projection was applied.

def perturbed(self) -> list[VariableId]:

The list of variables that are perturbed in this model (either true or false).

def perturbed_dict(self) -> dict[VariableId, bool]:

Returns a dictionary of only the perturbed variables and their values.

def perturbed_named_dict(self) -> dict[str, bool]:

Returns a dictionary of only the perturbed variables (identified by names) and their values.

def unperturbed(self) -> list[VariableId]:

The list of variables that are unperturbed in this model (i.e. None).

def perturbation_size(self) -> int:

The size of this perturbation. That is, the number of perturbed variables.

def values(self) -> list[typing.Optional[bool]]:

The list of values for individual variables from PerturbationModel.keys.

def items(self) -> list[tuple[VariableId, typing.Optional[bool]]]:

The list of key-value pairs represented in this model.

def to_dict(self) -> dict[VariableId, typing.Optional[bool]]:

The same as PerturbationModel.items, but returns a dictionary instead.

def to_named_dict(self) -> dict[str, typing.Optional[bool]]:

The same as PerturbationModel.to_dict, but the keys in the dictionary are names, not IDs.

def to_valuation(self) -> BddPartialValuation:

Return the underlying BddPartialValuation for this symbolic model.

def to_symbolic(self) -> PerturbationSet:

Return a PerturbationSet where all the variables are fixed according to the values in this PerturbationModel. Variables that are not present in the PerturbationModel are unrestricted.

class PerturbationSet:

A symbolic representation of a set of "perturbations". A perturbation specifies for each variable whether it is fixed or not, and if it is fixed, it prescribes a value. To do so, it uses a combination of state variables and perturbation parameters declared by an AsynchronousPerturbationGraph.

Internally, the representation therefore uses the state variables of the perturbable network variables, plus the perturbation parameters. If a variable is not perturbed, the state variable should remain unconstrained, as this is the most "natural" representation. However, this introduces some issues in terms of cardinality computation and iterators, since we now have to account for the fact that if a variable is unperturbed, it actually generates two perturbation instances (one with state variable true, one with false). We generally address this by manually fixing the state variable to false within these operations.

PerturbationSet(ctx: SymbolicSpaceContext, bdd: Bdd)

Normally, a new PerturbationSet is derived using an AsynchronousPerturbationGraph. However, in some cases you may want to create it manually from a AsynchronousPerturbationGraph and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid set of spaces.

def cardinality(self) -> int:

Returns the number of vertices that are represented in this set.

def intersect(self, other: PerturbationSet) -> PerturbationSet:

Set intersection.

def minus(self, other: PerturbationSet) -> PerturbationSet:

Set difference.

def union(self, other: PerturbationSet) -> PerturbationSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: PerturbationSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single vertex.

def pick_singleton(self) -> PerturbationSet:

Deterministically pick a subset of this set that contains exactly a single vertex.

If this set is empty, the result is also empty.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this PerturbationSet.

def to_internal(self) -> ColoredVertexSet:

Obtain the internal representation of this PerturbationSet, which uses the AsynchronousPerturbationGraph encoding. This is a colored set of vertices, where the colors only depend on the perturbation parameters, and the vertices are only constrained in case the variable is perturbed.

def extend_with_colors(self, set: ColorSet) -> ColoredPerturbationSet:

Extend this set of perturbations with all the colors from the given set.

This is essentially a cartesian product with the given ColorSet.

def items( self, retained: Optional[Sequence[Union[VariableId, str]]] = None) -> Iterator[PerturbationModel]:

Returns an iterator over all perturbations in this PerturbationSet with an optional projection to a subset of network variables.

When no retained collection is specified, this is equivalent to PerturbationSet.__iter__. However, if a retained set is given, the resulting iterator only considers unique combinations of the retained variables. Consequently, the resulting PerturbationModel instances will fail with an IndexError if a value of a variable outside the retained set is requested.

Similarly, IndexError is raised if you request a value of a variable that is not perturbable in the underlying AsynchronousPerturbationGraph.

class ColoredPerturbationSet:

A symbolic representation of a colored set of "perturbations". A perturbation specifies for each variable whether it is fixed or not, and if it is fixed, it prescribes a value. To do so, it uses a combination of state variables and perturbation parameters declared by an AsynchronousPerturbationGraph. The colors then prescribes the interpretations of the remaining network parameters.

ColoredPerturbationSet(ctx: SymbolicContext, bdd: Bdd)

Normally, a new ColoredPerturbationSet is derived using an AsynchronousPerturbationGraph. However, in some cases you may want to create it manually from a AsynchronousPerturbationGraph and a Bdd.

Just keep in mind that this method does not check that the provided Bdd is semantically a valid colored set of vertices.

def cardinality(self) -> int:

Returns the number of vertex-color pairs that are represented in this set.

def intersect(self, other: ColoredPerturbationSet) -> ColoredPerturbationSet:

Set intersection.

def minus(self, other: ColoredPerturbationSet) -> ColoredPerturbationSet:

Set difference.

def union(self, other: ColoredPerturbationSet) -> ColoredPerturbationSet:

Set union.

def is_empty(self) -> bool:

True if this set is empty.

def is_subset(self, other: ColoredPerturbationSet) -> bool:

True if this set is a subset of the other set.

Should be faster than just calling set.minus(superset).is_empty()

def is_singleton(self) -> bool:

True if this set is a singleton, i.e. a single perturbation-color pair.

def symbolic_size(self) -> int:

The number of Bdd nodes that are used to represent this set.

def colors(self) -> ColorSet:

Compute the existential projection of this relation to the color component. I.e. returns a set of colors such that for each color, there is at least one perturbation-color pair in the original set.

Note that this also fixes perturbation parameters to False, meaning the set no longer meaningfully depends on them. However, they do still appear in the symbolic encoding to ensure that the result is compatible with the underlying AsynchronousPerturbationGraph.

def perturbations(self) -> PerturbationSet:

Compute the existential projection of this relation to the perturbation component. I.e. returns a set of perturbations such that for each perturbation, there is at least one perturbation-color pair in the original set.

def intersect_colors(self, colors: ColorSet) -> ColoredPerturbationSet:

Retain only those perturbation-color pairs for which the color is also contained in the given colors set.

def intersect_perturbations(self, vertices: PerturbationSet) -> ColoredPerturbationSet:

Retain only those perturbation-color pairs for which the perturbation is also contained in the given perturbations set.

def minus_colors(self, colors: ColorSet) -> ColoredPerturbationSet:

Remove all perturbation-color pairs for which the color is present in the given colors set.

def minus_perturbations(self, vertices: PerturbationSet) -> ColoredPerturbationSet:

Remove all perturbation-color pairs for which the perturbation is present in the given perturbations set.

def select_perturbations( self, perturbations: Union[Mapping[Union[VariableId, str], Optional[bool]], PerturbationModel]) -> ColoredPerturbationSet:

Return the subset of this relation that has all the perturbations fixed according to the provided values.

To specify that a variable should be unperturbed, use "var": None. Any variable that should remain unrestricted should be completely omitted from the perturbations dictionary. This is similar to AsynchronousPerturbationGraph.mk_perturbations. If a PerturbationModel is given, only values that are omitted through projection will be considered as unrestricted.

def select_perturbation( self, perturbation: Union[Mapping[Union[VariableId, str], Optional[bool]], PerturbationModel]) -> ColorSet:

Return the set of colors for which the given perturbation exists in this set.

Note that here, we assume that the dictionary represents a single perturbation. Therefore, any missing perturbable variables are treated as unperturbed. This is the same behavior as in AsynchronousPerturbationGraph.mk_perturbation. Similarly, if a PerturbationModel is provided with some values eliminated through projection, these are assumed to be unperturbed.

def perturbation_robustness( self, perturbation: Union[Mapping[Union[VariableId, str], Optional[bool]], PerturbationModel]) -> float:

Return the global robustness of the given perturbation as represented in this colored set.

This is the fraction of colors for which the perturbation is present w.r.t. all colors that are admissible in the unperturbed system. Note that this has no relation to the total set of colors stored in this relation (i.e. set.colors()).

Note that here, we assume that the dictionary represents a single perturbation. Therefore, any missing perturbable variables are treated as unperturbed.

def select_by_size(self, size: int, up_to: bool) -> ColoredPerturbationSet:

Only retain those perturbations that have the given size. If up_to is set to True, then retain perturbations that have smaller or equal size.

def select_by_robustness( self, threshold: float, result_limit: Optional[int] = None) -> list[tuple[PerturbationModel, float, ColorSet]]:

Select all perturbations from this relation whose robustness is at least the given threshold.

Since this operation cannot be completed symbolically, the result is a list of explicit PerturbationModel instances, together with their robustness and their ColorSet. The perturbations are returned from smallest to largest (in terms of the number of perturbed variables, not robustness). Optionally, you can use result_limit to restrict the maximal number of returned perturbations.

You can also use ColoredPerturbationSet.select_by_size to first only select perturbations of a specific size and only then enumerate their robustness.

def pick_singleton(self) -> ColoredPerturbationSet:

Deterministically pick a subset of this set that contains exactly a single perturbation-color pair.

If this set is empty, the result is also empty.

def to_bdd(self) -> Bdd:

Obtain the underlying Bdd of this ColoredPerturbationSet.

def to_internal(self) -> ColoredVertexSet:

Obtain the internal representation of this ColoredPerturbationSet, which uses the AsynchronousPerturbationGraph encoding. This is a colored set of vertices, where the colors depend on the perturbation parameters and normal parameters, but the vertices are only constrained in case the variable is perturbed.

Returns an iterator over all perturbation-color pairs in this ColoredPerturbationSet relation, with an optional projection to a subset of network variables and uninterpreted functions.

Note that the perturbation parameters are automatically projected away from the returned ColorModel instances.

When no retained collections are specified, this is equivalent to ColoredPerturbationSet.__iter__. However, if a retained collection is given, the resulting iterator only considers unique combinations of the retained functions and variables. Consequently, the resulting ColorModel and PerturbationModel instances will fail with an IndexError if a value outside the retained set is requested (for the PerturbationModel, IndexError is also thrown if a value of a variable that is not perturbable is requested).

class Control:

def attractor_one_step( graph: AsynchronousPerturbationGraph, source: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], target: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], colors: Optional[ColorSet] = None) -> ColoredPerturbationSet:

Compute the color-perturbation pairs which guarantee that the network reaches a target attractor from the given source state, assuming the perturbation is applied for a single time step.

Optionally, you can provide a subset of relevant colors that will be considered. If not given, the method considers all colors.

def attractor_temporary( graph: AsynchronousPerturbationGraph, source: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], target: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], colors: Optional[ColorSet] = None) -> ColoredPerturbationSet:

Compute the color-perturbation pairs which guarantee that the network reaches a target attractor from the given source state, assuming the perturbation is applied indefinitely, but the system eventually returns to its original dynamics.

Optionally, you can provide a subset of relevant colors that will be considered. If not given, the method considers all colors.

def attractor_permanent( graph: AsynchronousPerturbationGraph, source: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], target: Union[VertexSet, Mapping[Union[VariableId, str], Optional[bool]]], colors: Optional[ColorSet] = None) -> ColoredPerturbationSet:

Compute the color-perturbation pairs which guarantee that the network reaches a target attractor from the given source state, assuming the perturbation is applied indefinitely.

Optionally, you can provide a subset of relevant colors that will be considered. If not given, the method considers all colors.

def phenotype_permanent( graph: AsynchronousPerturbationGraph, phenotype: VertexSet, oscillation_type: Optional[Literal['required', 'allowed', 'forbidden']] = None, size_limit: Optional[int] = None, stop_when_found: bool = False) -> ColoredPerturbationSet:

Compute the color-perturbation pairs which guarantee that the network reaches the specified target phenotype from any initial state, assuming the perturbation is applied indefinitely.

Optionally, you can provide an PhenotypeOscillation type that specifies whether the attractors must fully reside in the phenotype set (forbidden), can only intersect the phenotype set but still be proper subsets (allowed), or must intersect the phenotype while not being subsets (required). Default behavior is forbidden, i.e. each attractor fully resides in the phenotype set.

To reduce the search space (and speed up the computation), you can also specify an size_limit constraint (only perturbations that are smaller or equal will be considered). Furthermore, if stop_when_found is set, the method terminates early if a perturbation with robustness 1.0 is discovered (i.e. a perturbation is found that is effective for all network colors). When this option is active, other results that have been computed so far are still returned.