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
126
127
128

use crate::biodivine_std::traits::Set;
use crate::symbolic_async_graph::{GraphColoredVertices, 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.
impl SymbolicAsyncGraph {
    /// 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_forward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
        let mut result = initial.clone();
        'fwd: loop {
            for var in self.network.variables().rev() {
                let step = self.var_post_out(var, &result);
                if !step.is_empty() {
                    result = result.union(&step);
                    continue 'fwd;
                }
            }

            return result;
        }
    }

    /// 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 reach_backward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
        let mut result = initial.clone();
        'bwd: loop {
            for var in self.network.variables().rev() {
                let step = self.var_pre_out(var, &result);
                if !step.is_empty() {
                    result = result.union(&step);
                    continue 'bwd;
                }
            }

            return result;
        }
    }

    /// 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_forward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
        let mut result = initial.clone();
        'fwd: loop {
            for var in self.network.variables().rev() {
                let step = self.var_can_post_out(var, &result);
                if !step.is_empty() {
                    result = result.minus(&step);
                    continue 'fwd;
                }
            }

            return result;
        }
    }

    /// 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 trap_backward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
        let mut result = initial.clone();
        'bwd: loop {
            for var in self.network.variables().rev() {
                let step = self.var_can_pre_out(var, &result);
                if !step.is_empty() {
                    result = result.minus(&step);
                    continue 'bwd;
                }
            }

            return result;
        }
    }
}

#[cfg(test)]
mod tests {
    use crate::biodivine_std::traits::Set;
    use crate::symbolic_async_graph::SymbolicAsyncGraph;
    use crate::BooleanNetwork;

    #[test]
    pub fn basic_algorithms_test() {
        // Right now, there isn't really a strategy on how this should be tested, so for now
        // we only test if we can run through all the code and get reasonable results.
        let bn = BooleanNetwork::try_from(
            r"
            b ->? a
            c ->? a
            a -|? a
            a -> b
            a -> c
            c -| b
        ",
        )
        .unwrap();

        let stg = SymbolicAsyncGraph::new(bn).unwrap();

        let pivot = stg.unit_colored_vertices().pick_vertex();
        let fwd = stg.reach_forward(&pivot);
        let bwd = stg.reach_backward(&pivot);
        let scc = fwd.intersect(&bwd);

        // Should contain all cases where pivot is in an attractor.
        let attractor_basin = stg.trap_forward(&bwd);
        // Should contain all cases where pivot is in a repeller.
        let repeller_basin = stg.trap_backward(&fwd);

        assert!(fwd.approx_cardinality() > pivot.approx_cardinality());
        assert!(bwd.approx_cardinality() > pivot.approx_cardinality());
        assert!(scc.approx_cardinality() > pivot.approx_cardinality());
        assert!(attractor_basin.approx_cardinality() > pivot.approx_cardinality());
        // For some reason, there is only a very small number of parameter valuations
        // where this is not empty -- less than in the pivot in fact.
        assert!(!repeller_basin.is_empty());
    }
}