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>

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 vertex(&self, state: &ArrayBitVector) -> GraphColoredVertices

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

impl SymbolicAsyncGraph

Basic symbolic graph operators.

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

Compute the colored vertex set which is a result of applying the update function of the given variable to the initial set.

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

Compute the subset of set that can perform post using given variable.

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

Compute the colored vertex set which can create some valuation in initial by applying the update function of the given variable.

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

Compute the subset of set that can perform pre using given variable.

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

Compute the subset of set that can perform post using the given variable, such that the successor is also within set.

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

Compute the subset of set that can perform pre using the given variable, such that the predecessor is also within set.

impl SymbolicAsyncGraph

Derived operators.

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 post operation leads to a state within the same set.

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 pre operation leads to a state within the same set.

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.