1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

//! *Legacy* semi-symbolic representation of the coloured asynchronous state-transition graph.
//!
//! It represents states explicitly (see `IdState`), but uses symbolic representation (`BddParams`)
//! for sets of parameters.
//!
//! **`AsyncGraph` in its current form and the related structures are deprecated in favour of
//! `SymbolicAsyncGraph`. We may re-implement it later under a new name and a new API, because
//! in some niche use cases it seems to be faster and/or easier to use than a fully symbolic
//! approach. However, try not to rely on this implementation too much.**
//!
#![allow(deprecated)]

use crate::bdd_params::{BddParameterEncoder, BddParams};
use crate::biodivine_std::structs::{IdState, IdStateRange};
use crate::biodivine_std::traits::{Graph, InvertibleGraph, Set};
use crate::{BooleanNetwork, VariableId, VariableIdIterator};

mod _impl_async_graph;
mod _impl_default_edge_params;
mod _impl_evolution_operators;

/// An asynchronous transition system of a `BooleanNetwork`. The states of the graph
/// are standard `IdState`s. The parameter sets are given by the associated `AsyncGraphEdgeParams`.
///
/// Async graph implements the standard "asynchronous update", i.e. every variable can be
/// non-deterministically updated at any time, but the actual parameters for which this
/// happens are determined by the `AsyncGraphEdgeParams`.
///
/// This actually hides a lot of complexity, because implementing `AsyncGraphEdgeParams` is typically
/// much easier than re-implementing the whole async graph structure.
///
/// **`AsyncGraph` in its current form and the related structures are deprecated in favour of
/// `SymbolicAsyncGraph`. We may re-implement it later under a new name and a new API, because
/// in some niche use cases it seems to be faster than fully symbolic approach. However,
/// try not to rely on this implementation too much.**
#[deprecated]
pub struct AsyncGraph<P: AsyncGraphEdgeParams> {
    edges: P,
}

/// Default implementation for edge parameters which adheres to the monotonicity and observability
/// constraints  of the network, but poses no other restrictions.
pub struct DefaultEdgeParams {
    network: BooleanNetwork,
    encoder: BddParameterEncoder,
    /// The parameter valuations which satisfy the static regulation constraints.
    unit_set: BddParams,
    empty_set: BddParams,
}

/// Async graph edges implement the edge colouring (parametrisation) of a graph. Instances of
/// this trait are used together with the `AsyncGraph` to produce a semantic coloured graph
/// of a parametrised Boolean network.
///
/// See `DefaultEdgeParams` for default implementation of edge colours.
///
/// This trait is especially useful when constructing things like wrappers of existing graphs,
/// which need to modify the behaviour of the graph. Another option are various custom
/// parameter encoders, where we simply do not want to re-implement the whole graph trait
/// front scratch.
pub trait AsyncGraphEdgeParams {
    type ParamSet: Set;
    // A reference to the underlying Boolean network.
    fn network(&self) -> &BooleanNetwork;
    /// Create a new empty set of parameters.
    fn empty_params(&self) -> &Self::ParamSet;
    /// Create a new full set of parameters.
    fn unit_params(&self) -> &Self::ParamSet;
    /// Create parameters for the edge starting in the given `state`,
    /// flipping the given `variable`.
    fn edge_params(&self, state: IdState, variable: VariableId) -> Self::ParamSet;
    /// Construct a witness network for the given set of parameters.
    ///
    /// TODO: It is not really essential in this trait. Think of a way to move it elsewhere.
    fn make_witness(&self, params: &Self::ParamSet) -> BooleanNetwork;
}

/// A forward `EvolutionOperator` of the `AsyncGraph`.
pub struct Fwd<'a, Edges: AsyncGraphEdgeParams> {
    graph: &'a AsyncGraph<Edges>,
}

/// A backward `EvolutionOperator` of the `AsyncGraph`.
pub struct Bwd<'a, Edges: AsyncGraphEdgeParams> {
    graph: &'a AsyncGraph<Edges>,
}

/// An iterator over successors of a state in the `AsyncGraph`.
pub struct FwdIterator<'a, Edges: AsyncGraphEdgeParams> {
    graph: &'a AsyncGraph<Edges>,
    state: IdState,
    variables: VariableIdIterator,
}

/// An iterator over predecessors of a state in the `AsyncGraph`.
pub struct BwdIterator<'a, Edges: AsyncGraphEdgeParams> {
    graph: &'a AsyncGraph<Edges>,
    state: IdState,
    variables: VariableIdIterator,
}

impl<'a, Edges: AsyncGraphEdgeParams> Graph for &'a AsyncGraph<Edges> {
    type State = IdState;
    type Params = Edges::ParamSet;
    type States = IdStateRange;
    type FwdEdges = Fwd<'a, Edges>;
    type BwdEdges = Bwd<'a, Edges>;

    fn states(&self) -> Self::States {
        IdStateRange::new(self.num_states())
    }

    fn fwd(&self) -> Self::FwdEdges {
        Fwd { graph: self }
    }

    fn bwd(&self) -> Self::BwdEdges {
        Bwd { graph: self }
    }
}

impl<'a, Edges: AsyncGraphEdgeParams> InvertibleGraph for &'a AsyncGraph<Edges> {
    type FwdEdges = Fwd<'a, Edges>;
    type BwdEdges = Bwd<'a, Edges>;
}