Struct biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph

pub struct SymbolicAsyncGraph {
    network: BooleanNetwork,
    symbolic_context: SymbolicContext,
    vertex_space: (GraphColoredVertices, GraphColoredVertices),
    color_space: (GraphColors, GraphColors),
    unit_bdd: Bdd,
    update_functions: Vec<Bdd>,
}

A symbolic encoding of asynchronous transition system of a BooleanNetwork.

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

Fields

network: BooleanNetwork

symbolic_context: SymbolicContext

vertex_space: (GraphColoredVertices, GraphColoredVertices)

color_space: (GraphColors, GraphColors)

unit_bdd: Bdd

update_functions: Vec<Bdd>

Implementations

impl SymbolicAsyncGraph

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

impl SymbolicAsyncGraph

Examine the general properties of the graph.

pub fn as_network(&self) -> &BooleanNetwork

Return a reference to the original Boolean network.

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 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_vertices(&self) -> &GraphColoredVertices

Reference to an empty colored vertex set.

pub fn mk_empty_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 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:

• (a) 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).
• (b) This is already used by the internal BDD API, so the conversion is less involved.

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

fn select_partial_valuation(
    &self,
    partial_valuation: &[(BddVariable, bool)]
) -> GraphColoredVertices

(internal) Construct a subset of the unit_bdd with respect to the given partial valuation of BDD variables.

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).

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 sub-network.

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 sub-network 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 sub-network must have the same update function (tested using the abstract syntax tree, not semantics).
• If the main network has an erased update function, the sub-network can have a fully specified function (no parameters) instead.
• The sub-network 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 sub-network represented using the main network encoding. Otherwise, an error indicates which conditions were not met.

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.

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.