biodivine_lib_param_bn/tutorial/
p04_graph_algorithm_sample.rs

1//! # SCC Detection Algorithm
2//!
3//! Finally, let us examine a very basic algorithm built using this library:
4//! symbolic detection of SCC components.
5//!
6//! First, we need to define simple forward/backward reachability procedures:
7//!
8//! ```rust
9//! use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
10//! use biodivine_lib_param_bn::biodivine_std::traits::Set;
11//!
12//! fn fwd(graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices) -> GraphColoredVertices {
13//!     let mut result = initial.clone();
14//!     loop {
15//!         let post = graph.post(&result);
16//!         if post.is_subset(&result) {
17//!             return result;
18//!         } else {
19//!             result = result.union(&post);
20//!         }
21//!     }
22//! }
23//!
24//! fn bwd(graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices) -> GraphColoredVertices {
25//!     let mut result = initial.clone();
26//!     loop {
27//!         let post = graph.pre(&result);
28//!         if post.is_subset(&result) {
29//!             return result;
30//!         } else {
31//!             result = result.union(&post);
32//!         }
33//!     }
34//! }
35//! ```
36//!
37//! Note that in practice, it would be much better to use something like *saturation*, where
38//! the transitions which are applied are selected greedily one at a time, instead of applying
39//! them all at once using full `post` or `pre`. However, for the purpose of this tutorial, this
40//! should be sufficient.
41//!
42//! Now we can observe that an SCC of vertex `v` is always the intersection of forward and backward
43//! reachable vertices from `v`. Hence, we can write the following simple algorithm:
44//!
45//! ```rust
46//! # use biodivine_lib_param_bn::symbolic_async_graph::{SymbolicAsyncGraph, GraphColoredVertices};
47//! # use biodivine_lib_param_bn::BooleanNetwork;
48//! # use std::convert::TryFrom;
49//! # use biodivine_lib_param_bn::biodivine_std::traits::Set;
50//! # fn fwd(graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices) -> GraphColoredVertices {
51//! #     let mut result = initial.clone();
52//! #     loop {
53//! #         let post = graph.post(&result);
54//! #         if post.is_subset(&result) {
55//! #             return result;
56//! #         } else {
57//! #             result = result.union(&post);
58//! #         }
59//! #     }
60//! # }
61//!
62//! # fn bwd(graph: &SymbolicAsyncGraph, initial: &GraphColoredVertices) -> GraphColoredVertices {
63//! #     let mut result = initial.clone();
64//! #     loop {
65//! #         let post = graph.pre(&result);
66//! #         if post.is_subset(&result) {
67//! #             return result;
68//! #         } else {
69//! #             result = result.union(&post);
70//! #         }
71//! #     }
72//! # }
73//! fn scc(graph: &SymbolicAsyncGraph) -> Vec<GraphColoredVertices> {
74//!     let mut universe = graph.mk_unit_colored_vertices();
75//!     let mut components = Vec::new();
76//!     while !universe.is_empty() {
77//!         // Pick one vertex in universe for every color in universe
78//!         let pivots = universe.pick_vertex();
79//!         let fwd = fwd(graph, &pivots);
80//!         let bwd = bwd(graph, &pivots);
81//!         let scc = fwd.intersect(&bwd);
82//!         universe = universe.minus(&scc);
83//!         components.push(scc);
84//!     }
85//!     components
86//! }
87//! // Boolean network from the previous tutorial:
88//! let bn = BooleanNetwork::try_from(r"
89//!     A -> B
90//!     C -|? B
91//!     $B: A
92//!     C -> A
93//!     B -> A
94//!     A -| A
95//!     $A: C | f(A, B)
96//! ").unwrap();
97//! let stg = SymbolicAsyncGraph::new(&bn).unwrap();
98//!
99//! // Note that since the symbolic graph contains different transitions for different colors,
100//! // this will create SCCs that overlap for some colors but are completely different for others.
101//! // Hence, the same vertex can appear in multiple SCCs for different colors.
102//! let components = scc(&stg);
103//! assert_eq!(7, components.len());
104//! assert_eq!(2.0, components[0].vertices().approx_cardinality());
105//! assert_eq!(1.0, components[1].vertices().approx_cardinality());
106//! assert_eq!(2.0, components[2].vertices().approx_cardinality());
107//! assert_eq!(1.0, components[3].vertices().approx_cardinality());
108//! assert_eq!(2.0, components[4].vertices().approx_cardinality());
109//! assert_eq!(2.0, components[5].vertices().approx_cardinality());
110//! assert_eq!(1.0, components[6].vertices().approx_cardinality());
111//! ```
112//!
113//!
biodivine_lib_param_bn/tutorial/p04_graph_algorithm_sample.rs

biodivine_lib_param_bn/tutorial/
p04_graph_algorithm_sample.rs
