Struct biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph

pub struct SymbolicAsyncGraph { /* private fields */ }

A symbolic encoding of asynchronous transition system of a BooleanNetwork.

Provides standard pre/post operations for exploring the graph symbolically.

Implementations

impl SymbolicAsyncGraph

pub fn new(network: &BooleanNetwork) -> Result<SymbolicAsyncGraph, String>

Create a SymbolicAsyncGraph based on the default symbolic encoding of the supplied BooleanNetwork as implemented by the default SymbolicContext.

pub fn with_space_context( network: &BooleanNetwork, context: &SymbolicSpaceContext ) -> Result<SymbolicAsyncGraph, String>

Create a SymbolicAsyncGraph that is compatible with an existing SymbolicSpaceContext.

The BooleanNetwork argument must be the same as used for the creation of the SymbolicSpaceContext object.

pub fn with_custom_context( network: &BooleanNetwork, context: SymbolicContext, unit_bdd: Bdd ) -> Result<SymbolicAsyncGraph, String>

Create a SymbolicAsyncGraph based on the given BooleanNetwork and a SymbolicContext (i.e. the network’s encoding, possibly with extra symbolic variables). Also takes an initial “unit” Bdd representing the full set of vertices and colors.

However, note that we do not validate that the provided SymbolicContext and the Bdd are compatible with the BooleanNetwork. If you use a context that was not created for the given network, the behaviour is undefined (you’ll likely see something fail rather quickly though).

Several notes to keep in mind while using this method:

1. The unit_bdd is used as an “initial value” for the set of all states and colors of this graph. However, it is still modified to only allow valid parameter valuations, so you can use it to reduce the space of valid states/colors, but it is not necessarily the final “unit set” of the graph.
2. The presence of extra symbolic variables can modify the semantics of symbolic operations implemented on SymbolicAsyncGraph, GraphVertices, GraphColors and GraphColoredVertices. The SymbolicAsyncGraph will not use or depend on the extra variables in any capacity. Hence, as long as the extra variables remain unused, all operations should behave as expected. However, once you introduce the variables externally (e.g. using a “raw” BDD operation instead of the “high level” API), you should verify that the semantics of symbolic operations are really what you expect them to be. For example, an intersection on sets will now also depend on the values of the extra variables, not just states and colors.
3. In general, unit_bdd should be a cartesian product of a set of vertices, a set of colors, and a set of valuations on the extra variables. If you don’t follow this requirement, almost everything remains valid, but ultimately, some symbolic operations may not have the same semantics as in the “officially supported” case. In particular, you can find that some operations will automatically expand the result based on this cartesian product assumption, so again, use at your own risk.

TODO: If we ever get a chance to rewrite SymbolicAsyncGraph, all of this should be handled much more transparently. I.e. it should be possible to create a graph on custom subset of states/colors without the cartesian product requirement. Also, we should be able to be more transparent/explicit about the presence of extra symbolic variables.

pub unsafe fn new_raw( network: Option<BooleanNetwork>, symbolic_context: SymbolicContext, unit_bdd: Bdd, functions: Vec<Bdd> ) -> SymbolicAsyncGraph

Construct a new SymbolicAsyncGraph completely using raw Bdd values. You can also supply an optional BooleanNetwork, but this will not be used in any meaningful way.

• Here, the unit_bdd will be used as the set of colors/vertices without any further postprocessing.
• The functions vector contains a BDD for each variable which is true if and only if the update function of said variable is true.

Safety

This is an unsafe function because it is extremely easy to use to create an invalid graph.

impl SymbolicAsyncGraph

Examine the general properties of the graph.

pub fn as_network(&self) -> Option<&BooleanNetwork>

Return a reference to the original Boolean network, if there is any.

pub fn get_symbolic_fn_update(&self, variable: VariableId) -> &Bdd

Get the symbolic representation of the update function for the given VariableId.

pub fn get_variable_name(&self, variable: VariableId) -> String

Return the string name of the specified VariableId.

pub fn symbolic_context(&self) -> &SymbolicContext

Return a reference to the symbolic context of this graph.

pub fn fix_network_variable( &self, variable: VariableId, value: bool ) -> GraphColoredVertices

Create a colored vertex set with a fixed value of the given variable.

pub fn fix_vertices_with_network_variable( &self, variable: VariableId, value: bool ) -> GraphVertices

Create a vertex set with a fixed value of the given network variable.

Note that if you only need the vertices, this can be slightly faster than running SymbolicAsyncGraph::fix_network_variable().vertices().

pub fn pick_witness(&self, colors: &GraphColors) -> BooleanNetwork

Make a witness network for one color in the given set.

pub fn empty_colors(&self) -> &GraphColors

Reference to an empty color set.

pub fn mk_empty_colors(&self) -> GraphColors

Make a new copy of empty color set.

pub fn unit_colors(&self) -> &GraphColors

Reference to a unit color set.

pub fn mk_unit_colors(&self) -> GraphColors

Make a new copy of unit color set.

pub fn empty_colored_vertices(&self) -> &GraphColoredVertices

Reference to an empty colored vertex set.

pub fn mk_empty_colored_vertices(&self) -> GraphColoredVertices

Make a new copy of empty vertex set.

pub fn unit_colored_vertices(&self) -> &GraphColoredVertices

Reference to a unit colored vertex set.

pub fn mk_unit_colored_vertices(&self) -> GraphColoredVertices

Make a new copy of unit vertex set.

pub fn empty_vertices(&self) -> &GraphVertices

pub fn mk_empty_vertices(&self) -> GraphVertices

pub fn unit_vertices(&self) -> &GraphVertices

pub fn mk_unit_vertices(&self) -> GraphVertices

pub fn num_vars(&self) -> usize

pub fn variables(&self) -> VariableIdIterator

pub fn mk_subspace(&self, values: &[(VariableId, bool)]) -> GraphColoredVertices

Compute a subset of the unit vertex set that is specified using the given list of (variable, value) pairs. That is, the resulting set contains only those vertices that have all the given variables set to their respective values.

Note: The reason this method takes a slice and not, e.g., a HashMap is that:

• If constant, slices are much easier to write in code (i.e. we can write graph.mk_subspace(&[(a, true), (b, false)]) – there is no such syntax for a map).
• This is already used by the internal BDD API, so the conversion is less involved.

pub fn is_trap_set(&self, set: &GraphColoredVertices) -> bool

Return true of the given set is a trap set (also invariant set; set with no outgoing transitions).

pub fn mk_partial_vertex(&self, state: &[Option<bool>]) -> GraphColoredVertices

This is the same as mk_subspace, but it allows you to specify the partial valuation using a slice of optional Booleans instead of mapping VariableId objects.

Such slice may be easier obtain for example when one is starting with a network state (vertex) that is already represented as a Vec<bool>. In this case, it may be easier to convert Vec<bool> to Vec<Option<bool>> and then simply erase the undesired values.

pub fn vertex(&self, state: &ArrayBitVector) -> GraphColoredVertices

Construct a vertex set that only contains one vertex, but all colors

pub fn inline_symbolic( &self, variable: VariableId ) -> Option<SymbolicAsyncGraph>

Create a new SymbolicAsyncGraph which inlines VariableId into all target update functions.

The inlining is currently not allowed on variables that have a self-regulation.

The new SymbolicAsyncGraph has no associated BooleanNetwork.

pub fn restrict(&self, set: &GraphColoredVertices) -> SymbolicAsyncGraph

Create a copy of this SymbolicAsyncGraph where the vertex space is restricted to the given set (including possible transitions). The resulting graph is symbolically compatible with this graph, so the sets of vertices and colors are interchangeable.

However, note that in a restricted graph, it may not hold that the unit vertex set is a product of some subset of vertices and some subset of colours (i.e. there may be vertices that are present for some colors and not for others, and vice-versa).

pub fn wrap_in_symbolic_subspace( &self, set: &GraphColoredVertices ) -> GraphColoredVertices

Fined the smallest subspace (hypercube) that encapsulates all the vertices within this set (colors are not affected).

Keep in mind that since the colors are not affected, the result might not pass through GraphColoredVertices::is_subspace, but the vertices() set should pass this check.

pub fn wrap_in_subspace(&self, set: &GraphVertices) -> Space

Find the smallest subspace (hypercube) that contains the given set of vertices.

pub fn restrict_variable_in_graph( &self, var: VariableId, value: bool ) -> SymbolicAsyncGraph

Fix a variable in the underlying symbolic representation and then erase it completely from the result. The resulting representation still “contains” the variable, but the update functions no longer depend on it.

pub fn existential_extra_variable_projection<T: BddSet>(&self, set: &T) -> T

Uses projection to eliminate any extra variables that a given symbolic set might depend on.

You can use this method to “reset” the set such that it is guaranteed to be compliant with the SymbolicAsyncGraph representation. However, keep in mind that “existential” projection will include all items, even if they are valid only for a subset of the extra-variable valuations (i.e. it’s a big union).

pub fn universal_extra_variable_projection<T: BddSet>(&self, set: &T) -> T

Uses projection to eliminate any extra variables that a given symbolic set might depend on.

You can use this method to “reset” the set such that it is guaranteed to be compliant with the SymbolicAsyncGraph representation. However, keep in mind that “universal” projection will include only items that are valid for any valuation of the extra variables (i.e. it’s a big intersection).

impl SymbolicAsyncGraph

pub fn mk_subnetwork_colors( &self, network: &BooleanNetwork ) -> Result<GraphColors, String>

Compute the set of all possible colours (instantiations) of this (main) network that are represented by the supplied more specific subnetwork.

Note that this is a rather non-trivial theoretical problem. Consequently, the implementation is currently limited such that it only supports the following special case. In the future, these restrictions may be lifted as we add better equivalence checking algorithms:

• The two networks have the same variables.
• All parameters used in the subnetwork must also be declared in the main network (with the same arity).
• The regulations are identical in both networks (including monotonicity/observability).
• If the main network has an update function, the subnetwork must have the same update function (tested using the abstract syntax tree, not semantics).
• If the main network has an erased update function, the subnetwork can have a fully specified function (no parameters) instead.
• The subnetwork and main network are consistent with the shared regulatory graph.

If all of these conditions are met, the function returns a ColorSet representing all instantiations of the subnetwork represented using the main network encoding. Otherwise, an error indicates which conditions were not met.

Panics

The method requires that Self::as_network is Some.

pub fn transfer_colors_from( &self, colors: &GraphColors, graph: &SymbolicAsyncGraph ) -> Option<GraphColors>

Translate a symbolic set from a compatible graph such that it is valid in this SymbolicAsyncGraph.

The graph is considered compatible if:

1. All parameters which appear in colors also appear in this graph under the same name (parameters not used in colors do not matter).
2. The internal ordering of symbolic parameter variables is equivalent between graphs.

At the moment, condition (2) depends on network structure and is hard to directly influence unless you use SymbolicAsyncGraph::with_custom_context. In the future, we plan to relax this restriction by automatically reordering the variables as part of the translation (TODO).

pub fn transfer_vertices_from( &self, vertices: &GraphVertices, graph: &SymbolicAsyncGraph ) -> Option<GraphVertices>

Translate a symbolic set from a compatible graph such that it is valid in this SymbolicAsyncGraph.

The graph is considered compatible if:

1. All variables which appear in vertices also appear in this graph under the same name (variables not used in vertices do not matter).
2. The internal ordering of symbolic variables is equivalent between the two graphs.

At the moment, variables are by default ordered alphabetically, hence condition (2) should be only broken if one of the graphs uses a custom ordering. In the future, we plan to relax this restriction by automatically reordering the variables as part of the translation (TODO).

pub fn transfer_from( &self, set: &GraphColoredVertices, graph: &SymbolicAsyncGraph ) -> Option<GraphColoredVertices>

Translate a symbolic set from a compatible graph such that it is valid in this SymbolicAsyncGraph.

The graph is considered compatible if:

1. All parameters and state variables which appear in set also appear in this graph under the same name (variables not used in set do not matter).
2. The internal ordering of relevant symbolic variables is equivalent between graphs.

At the moment, condition (2) depends on network structure and is hard to directly influence if parameters are used extensively unless you use SymbolicAsyncGraph::with_custom_context. In the future, we plan to relax this restriction by automatically reordering the variables as part of the translation (TODO). For state variables, the ordering should be by default equivalent, since they are ordered alphabetically.

pub fn reconstruct_network(&self) -> Option<BooleanNetwork>

Try to reconstruct a BooleanNetwork that is semantically equivalent to the one encoded by this SymbolicAsyncGraph. Currently, this operation returns None if the network uses any non-trivial parameters (i.e. arity more than zero). This is because we have no reasonable procedure to reconstruct the original function expression from such a BDD.

impl SymbolicAsyncGraph

Here, we provide several basic symbolic algorithms for exploring the SymbolicAsyncGraph. This mainly includes reachability and similar fixed-point properties.

In some cases, you may want to re-implement these algorithms, since they do not have more advanced features, like logging or cancellation. But for most general use-cases, these should be the best we can do right now in terms of performance.

pub fn reach_forward( &self, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the set of forward-reachable vertices from the given initial set.

In other words, the result is the smallest forward-closed superset of initial.

pub fn reach_backward( &self, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the set of backward-reachable vertices from the given initial set.

In other words, the result is the smallest backward-closed superset of initial.

pub fn trap_forward( &self, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the subset of initial vertices that can only reach other vertices within the initial set.

In other words, the result is the largest forward-closed subset of initial.

pub fn trap_backward( &self, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the subset of initial vertices that can only be reached from vertices within the initial set.

In other words, the result is the largest backward-closed subset of initial.

pub fn space_has_var_false(&self, var: VariableId, space: &Space) -> bool

Returns true if the update function of VariableId can evaluate to false in the given space.

pub fn space_has_var_true(&self, var: VariableId, space: &Space) -> bool

Returns true if the update function of VariableId can evaluate to true in the given space.

pub fn percolate_space(&self, space: &Space, fix_subspace: bool) -> Space

Compute a percolation of the given space.

The method has two modes: If fix_subspace is set to true, the method will only try to update variables that are not fixed yet. If fix_subspace is false, the method can also update variables that are fixed in the original space.

If the input is a trap space, these two modes should give the same result.

impl SymbolicAsyncGraph

Basic symbolic graph operators. For convenience, there is a wide variety of different operators fulfilling different needs. Here, all operators only analyse transitions with respect to a single network variable and every operation implemented using one symbolic operation.

The general recommendation is to use var_post / var_pre for most tasks (implementing additional logic using extra symbolic operations), and once the algorithm is tested and stable, replace these functions with the more efficient “fused” operations.

We provide the following variable-specific operations:

• var_post / var_pre: General successors or predecessors.
• var_post_out / var_pre_out: Successors or predecessors, but only outside of the given initial set.
• var_post_within / var_pre_within: Successors or predecessors, but only inside the given initial set.
• var_can_post / var_can_pre: Subset of the initial set that has some successors / predecessors.
• var_can_post_out / var_can_pre_out: Subset of the initial set that can perform a transition leading outside of the initial set.
• var_can_post_within / var_can_pre_within: Subset of the initial set that can perform a transition leading into the initial set.

Note that the output of some of these functions is technically equivalent (e.g. var_post_within and var_can_pre_within) but we nevertheless provided all for completeness.

pub fn var_post( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the successors of the vertices in the given initial set that are reached by updating the given variable. Formally:

$$ \texttt{VarPost}(v, X) = \{(y, c) \mid \exists x.(x, c) \in X \land x \xrightarrow{v}_c y~\} $$

pub fn var_pre( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the predecessors of the vertices in the given initial set that are reached by updating the given variable. Formally:

$$ \texttt{VarPre}(v, X) = \{(x, c) \mid \exists y.(y, c) \in X \land x \xrightarrow{v}_{c} y~\} $$

pub fn var_post_out( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the successors of the vertices in the given initial set that are reached by updating the given variable, but are not in the initial set. Formally:

$$ \texttt{VarPostOut}(v, X) = \{(y, c) \mid (y, c) \notin X \land \exists x.(x, c) \in X \land x \xrightarrow{v}_{c} y~\} $$

pub fn var_pre_out( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the predecessors of the vertices in the given initial set that are reached by updating the given variable, but are not in the initial set. Formally:

$$ \texttt{VarPreOut}(v, X) = \{(x, c) \mid (x, c) \notin X \land \exists y.(y, c) \in X \land x \xrightarrow{v}_{c} y~\} $$

pub fn var_post_within( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the successors of the vertices in the given initial set that are reached by updating the given variable, but are within the initial set. Formally:

$$ \texttt{VarPostWithin}(v, X) = \{(y, c) \mid (y, c) \in X \land \exists x.(x, c) \in X \land x \xrightarrow{v}_{c} y~\} $$

pub fn var_pre_within( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the predecessors of the vertices in the given initial set that are reached by updating the given variable, but are within the initial set. Formally:

$$ \texttt{VarPreWithin}(v, X) = \{(x, c) \mid (x, c) \in X \land \exists y.(y, c) \in X \land x \xrightarrow{v}_{c} y~\} $$

pub fn var_can_post( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an outgoing transition using the given variable. Formally:

$$ \texttt{VarCanPost}(v, X) = \{~ (x, c) \in X \mid \exists y.~ x \xrightarrow{v}_{c} y ~\} $$

pub fn var_can_pre( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an incoming transition using the given variable. Formally:

$$ \texttt{VarCanPre}(v, X) = \{~ (y, c) \in X \mid \exists x.~ x \xrightarrow{v}_{c} y ~\} $$

pub fn var_can_post_out( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an outgoing transition using the given variable that leads outside of the initial set. Formally:

$$ \texttt{VarCanPostOut}(v, X) = \{~ (x, c) \in X \mid \exists y.~(y, c) \notin X \land x \xrightarrow{v}_{c} y ~\} $$

pub fn var_can_pre_out( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an incoming transition using the given variable that originates outside of the initial set. Formally:

$$ \texttt{VarCanPreOut}(v, X) = \{~ (y, c) \in X \mid \exists x.~(x, c) \notin X \land x \xrightarrow{v}_{c} y ~\} $$

pub fn var_can_post_within( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an outgoing transition using the given variable that leads into the initial set. Formally:

$$ \texttt{VarCanPostWithin}(v, X) = \{~ (x, c) \in X \mid \exists y.~(y, c) \in X \land x \xrightarrow{v}_{c} y ~\} $$

pub fn var_can_pre_within( &self, variable: VariableId, initial: &GraphColoredVertices ) -> GraphColoredVertices

Compute the GraphColoredVertices representing the subset of the initial set for which there exists an incoming transition using the given variable that originates inside the initial set. Formally:

$$ \texttt{VarCanPreWithin}(v, X) = \{~ (y, c) \in X \mid \exists x.~(x, c) \in X \land x \xrightarrow{v}_{c} y ~\} $$

impl SymbolicAsyncGraph

Here, we give several operators derived from the variable-specific operators. These have complexity O(|vars|) since they are internally represented using the variable-specific operators.

We provide the following functions:

• post / pre: General successors and predecessors functions.
• can_post / can_pre: Subsets of the initial states that have some successors or predecessors.
• can_post_within / can_pre_within: Subsets of initial states that have some successors / predecessors within the initial set.
• will_post_within / will_pre_within: Subsets of initial states that have all successors / predecessors withing the initial set.
• can_post_out / can_pre_out: Subsets of initial states that have some successors / predecessors outside of the initial set.
• will_post_out / will_pre_out: Subsets of initial states that have all successors / predecessors outside of the initial set.

pub fn post(&self, initial: &GraphColoredVertices) -> GraphColoredVertices

Compute the result of applying post with all update functions to the initial set.

pub fn pre(&self, initial: &GraphColoredVertices) -> GraphColoredVertices

Compute the result of applying pre with all update functions to the initial set.

pub fn can_post(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set that can perform some post operation.

pub fn can_pre(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set that can perform some pre operation.

pub fn can_post_within( &self, set: &GraphColoredVertices ) -> GraphColoredVertices

Compute the subset of set that can perform some post operation which leads to a state within set.

pub fn will_post_within( &self, set: &GraphColoredVertices ) -> GraphColoredVertices

Compute the subset of set such that every admissible post operation leads to a state within the same set.

Note that this also includes states which cannot perform any post operation.

pub fn can_pre_within(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set that can perform some pre operation which leads to a state within set.

pub fn will_pre_within( &self, set: &GraphColoredVertices ) -> GraphColoredVertices

Compute the subset of set such that every admissible pre operation leads to a state within the same set.

Note that this also includes states which cannot perform any pre operation.

pub fn can_post_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set that can perform some post operation which leads to a state outside of set.

pub fn will_post_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set such that every admissible post operation leads to a state outside the set.

Note that this also includes states which cannot perform any post operation.

pub fn can_pre_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set that can perform some pre operation which leads to a state outside of set.

pub fn will_pre_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices

Compute the subset of set such that every admissible pre operation leads to a state outside of set.

Note that this also includes states which cannot perform any pre operation.

Trait Implementations

impl Clone for SymbolicAsyncGraph

fn clone(&self) -> SymbolicAsyncGraph

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.