From 1fc3e25c045709c4a9e83364525d2ff5657a5378 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Wed, 13 Dec 2023 14:39:22 +0100
Subject: [PATCH] Disconnect `SymbolicAsyncGraph` from the underlying
 `BooleanNetwork`.

---
 .../_from_string_for_boolean_network.rs       |   6 +-
 src/_impl_fn_update.rs                        | 159 ++++---
 src/_impl_space.rs                            |   6 +-
 src/bin/bench_fixed_points_naive.rs           |   2 +-
 src/bin/bench_fixed_points_symbolic.rs        |   2 +-
 src/bin/bench_fixed_points_symbolic_colors.rs |   2 +-
 .../bench_fixed_points_symbolic_iterator.rs   |   2 +-
 .../bench_fixed_points_symbolic_vertices.rs   |   2 +-
 src/bin/bench_reach.rs                        |   2 +-
 src/bin/bench_trap_spaces_minimal.rs          |   2 +-
 src/bin/check_fixed_points.rs                 |   2 +-
 src/bin/check_fixed_points_solver.rs          |   2 +-
 src/fixed_points/mod.rs                       |  19 +-
 src/fixed_points/solver_iterator.rs           |   2 +-
 src/fixed_points/symbolic_iterator.rs         |   6 +-
 .../_impl_graph_colored_vertices.rs           |   2 +-
 .../_impl_symbolic_async_graph.rs             | 390 +++++++++++-------
 .../_impl_symbolic_async_graph_algorithm.rs   |  10 +-
 .../_impl_symbolic_async_graph_operators.rs   | 192 +++------
 .../_impl_symbolic_context.rs                 |  25 +-
 src/symbolic_async_graph/mod.rs               |  18 +-
 .../projected_iteration.rs                    |  98 ++---
 .../_impl_network_colored_spaces.rs           |   2 +-
 src/trap_spaces/_impl_trap_spaces.rs          |   2 +-
 src/tutorial/p03_symbolic_async_graph.rs      |  14 +-
 src/tutorial/p04_graph_algorithm_sample.rs    |   2 +-
 26 files changed, 529 insertions(+), 442 deletions(-)

diff --git a/src/_aeon_parser/_from_string_for_boolean_network.rs b/src/_aeon_parser/_from_string_for_boolean_network.rs
index 828bf32..228cddc 100644
--- a/src/_aeon_parser/_from_string_for_boolean_network.rs
+++ b/src/_aeon_parser/_from_string_for_boolean_network.rs
@@ -204,9 +204,9 @@ a -?? a
 b -|? c
 c -? a
 c -> d
-$a: (a & (p(c) => (c | c)))
-$b: (p(a) <=> q(a, a))
-$c: (q(b, b) => !(b ^ k))
+$a: a & (p(c) => (c | c))
+$b: p(a) <=> q(a, a)
+$c: q(b, b) => !(b ^ k)
 ";
 
         assert_eq!(
diff --git a/src/_impl_fn_update.rs b/src/_impl_fn_update.rs
index 02d0213..ad47e3d 100644
--- a/src/_impl_fn_update.rs
+++ b/src/_impl_fn_update.rs
@@ -3,7 +3,7 @@ use crate::BinaryOp::{And, Iff, Imp, Or, Xor};
 use crate::FnUpdate::*;
 use crate::_aeon_parser::FnUpdateTemp;
 use crate::{BinaryOp, BooleanNetwork, FnUpdate, ParameterId, VariableId};
-use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable};
+use biodivine_lib_bdd::{Bdd, BddVariable};
 use std::collections::{HashMap, HashSet};
 
 /// Constructor and destructor utility methods. These mainly avoid unnecessary boxing
@@ -118,6 +118,26 @@ impl FnUpdate {
             _ => None,
         }
     }
+
+    /// Build an expression which is equivalent to the conjunction of the given expressions.
+    pub fn mk_conjunction(items: &[FnUpdate]) -> FnUpdate {
+        let Some(first) = items.get(0) else {
+            // Empty conjunction is `true`.
+            return Self::mk_true();
+        };
+        let rest = &items[1..];
+        rest.iter().fold(first.clone(), |a, b| a.and(b.clone()))
+    }
+
+    /// Build an expression which is equivalent to the disjunction of the given expressions.
+    pub fn mk_disjunction(items: &[FnUpdate]) -> FnUpdate {
+        let Some(first) = items.get(0) else {
+            // Empty disjunction is `false`.
+            return Self::mk_false();
+        };
+        let rest = &items[1..];
+        rest.iter().fold(first.clone(), |a, b| a.or(b.clone()))
+    }
 }
 
 /// Other utility methods.
@@ -148,54 +168,40 @@ impl FnUpdate {
             return FnUpdate::mk_false();
         }
 
-        let state_variables: HashMap<BddVariable, VariableId> = context
+        let translation_map: HashMap<BddVariable, VariableId> = context
             .state_variables()
             .iter()
             .enumerate()
             .map(|(i, v)| (*v, VariableId::from_index(i)))
             .collect();
-        let support = bdd.support_set();
-        for k in &support {
-            if !state_variables.contains_key(k) {
-                panic!("Non-state variables found in the provided BDD.")
-            }
-        }
 
-        // Because the BDD isn't constant, there must be at least one clause and each clause
-        // must have at least one literal.
-
-        fn build_clause(
-            map: &HashMap<BddVariable, VariableId>,
-            clause: BddPartialValuation,
-        ) -> FnUpdate {
-            fn build_literal(
-                map: &HashMap<BddVariable, VariableId>,
-                literal: (BddVariable, bool),
-            ) -> FnUpdate {
-                let var = FnUpdate::mk_var(*map.get(&literal.0).unwrap());
-                if literal.1 {
-                    var
-                } else {
-                    FnUpdate::mk_not(var)
-                }
-            }
-
-            let mut literals = clause.to_values().into_iter();
-            let mut clause = build_literal(map, literals.next().unwrap());
-            for literal in literals {
-                let literal = build_literal(map, literal);
-                clause = FnUpdate::mk_binary(And, clause, literal);
-            }
-            clause
+        // All variables must be state variables.
+        for var in bdd.support_set() {
+            assert!(translation_map.contains_key(&var));
         }
 
-        let mut clauses = bdd.sat_clauses();
-        let mut result = build_clause(&state_variables, clauses.next().unwrap());
-        for clause in clauses {
-            let clause = build_clause(&state_variables, clause);
-            result = FnUpdate::mk_binary(Or, result, clause);
-        }
-        result
+        // Now, we transform the BDD into DNF and that into a FnUpdate.
+        let dnf = bdd.to_dnf();
+        let dnf = dnf
+            .into_iter()
+            .map(|valuation| {
+                let literals = valuation
+                    .to_values()
+                    .into_iter()
+                    .map(|(var, value)| {
+                        let bn_var = translation_map[&var];
+                        let literal = FnUpdate::mk_var(bn_var);
+                        if value {
+                            literal
+                        } else {
+                            literal.negation()
+                        }
+                    })
+                    .collect::<Vec<_>>();
+                FnUpdate::mk_conjunction(&literals)
+            })
+            .collect::<Vec<_>>();
+        FnUpdate::mk_disjunction(&dnf)
     }
 
     /// Return a sorted vector of all variables that are actually used as inputs in this function.
@@ -254,25 +260,48 @@ impl FnUpdate {
 
     /// Convert this update function to a string, taking names from the provided `BooleanNetwork`.
     pub fn to_string(&self, context: &BooleanNetwork) -> String {
-        match self {
-            Const(value) => value.to_string(),
-            Var(id) => context.get_variable_name(*id).to_string(),
-            Not(inner) => format!("!{}", inner.to_string(context)),
-            Binary(op, l, r) => {
-                format!("({} {} {})", l.to_string(context), op, r.to_string(context))
-            }
-            Param(id, args) => {
-                if args.is_empty() {
-                    context[*id].get_name().to_string()
-                } else {
-                    let mut arg_string = format!("({}", args[0].to_string(context));
-                    for arg in args.iter().skip(1) {
-                        arg_string = format!("{}, {}", arg_string, arg.to_string(context));
+        fn to_string_rec(function: &FnUpdate, context: &BooleanNetwork, no_paren: bool) -> String {
+            match function {
+                Const(value) => value.to_string(),
+                Var(id) => context.get_variable_name(*id).to_string(),
+                Not(inner) => format!("!{}", to_string_rec(inner, context, false)),
+                Binary(op, l, r) => {
+                    // And/Or have special treatments so that chains don't produce
+                    // unnecessary parenthesis.
+                    let l_nested_and = *op == And && matches!(**l, Binary(And, _, _));
+                    let r_nested_and = *op == And && matches!(**r, Binary(And, _, _));
+                    let l_nested_or = *op == Or && matches!(**l, Binary(Or, _, _));
+                    let r_nested_or = *op == Or && matches!(**r, Binary(Or, _, _));
+
+                    let l_no_paren = l_nested_and || l_nested_or;
+                    let r_no_paren = r_nested_and || r_nested_or;
+
+                    let l = to_string_rec(l, context, l_no_paren);
+                    let r = to_string_rec(r, context, r_no_paren);
+
+                    if no_paren {
+                        format!("{} {} {}", l, op, r)
+                    } else {
+                        format!("({} {} {})", l, op, r)
+                    }
+                }
+                Param(id, args) => {
+                    if args.is_empty() {
+                        context[*id].get_name().to_string()
+                    } else {
+                        // No need for top-level parenthesis in parameters, since commas
+                        // serve the same purpose.
+                        let mut arg_string = format!("({}", to_string_rec(&args[0], context, true));
+                        for arg in args.iter().skip(1) {
+                            arg_string =
+                                format!("{}, {}", arg_string, to_string_rec(arg, context, true));
+                        }
+                        format!("{}{})", context[*id].get_name(), arg_string)
                     }
-                    format!("{}{})", context[*id].get_name(), arg_string)
                 }
             }
         }
+        to_string_rec(self, context, true)
     }
 
     /// If possible, evaluate this function using the given network variable valuation.
@@ -997,4 +1026,22 @@ mod tests {
             FnUpdate::try_from_str("f(false, c) => g(a, b) | a", &bn).unwrap(),
         );
     }
+
+    #[test]
+    fn test_operator_coalescing() {
+        let bn = BooleanNetwork::try_from(
+            r"
+            a -> b
+            b -> c
+            c -> a
+        ",
+        )
+        .unwrap();
+        assert_eq!(
+            FnUpdate::try_from_str("(a & !b & c) | (!a & b) | c", &bn)
+                .unwrap()
+                .to_string(&bn),
+            "(a & !b & c) | (!a & b) | c"
+        );
+    }
 }
diff --git a/src/_impl_space.rs b/src/_impl_space.rs
index 6e9391f..05e1d9f 100644
--- a/src/_impl_space.rs
+++ b/src/_impl_space.rs
@@ -54,7 +54,11 @@ impl Space {
     /// Create a new space tracking the variables of the given network, where all values are
     /// initially assigned as `Any`.
     pub fn new(network: &BooleanNetwork) -> Space {
-        Space(vec![Any; network.num_vars()])
+        Self::new_raw(network.num_vars())
+    }
+
+    pub fn new_raw(num_vars: usize) -> Space {
+        Space(vec![Any; num_vars])
     }
 
     /// Convert a list of values (such as used by `SymbolicAsyncGraph`) into a proper "space" object.
diff --git a/src/bin/bench_fixed_points_naive.rs b/src/bin/bench_fixed_points_naive.rs
index 1d5ff39..1ad2cae 100644
--- a/src/bin/bench_fixed_points_naive.rs
+++ b/src/bin/bench_fixed_points_naive.rs
@@ -14,7 +14,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let fixed_points = FixedPoints::naive_symbolic(&stg, stg.unit_colored_vertices());
     println!(
diff --git a/src/bin/bench_fixed_points_symbolic.rs b/src/bin/bench_fixed_points_symbolic.rs
index 9796f84..e137184 100644
--- a/src/bin/bench_fixed_points_symbolic.rs
+++ b/src/bin/bench_fixed_points_symbolic.rs
@@ -14,7 +14,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let fixed_points = FixedPoints::symbolic(&stg, stg.unit_colored_vertices());
     println!(
diff --git a/src/bin/bench_fixed_points_symbolic_colors.rs b/src/bin/bench_fixed_points_symbolic_colors.rs
index 253e5bf..fc48923 100644
--- a/src/bin/bench_fixed_points_symbolic_colors.rs
+++ b/src/bin/bench_fixed_points_symbolic_colors.rs
@@ -14,7 +14,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let fixed_points = FixedPoints::symbolic_colors(&stg, stg.unit_colored_vertices());
     println!(
diff --git a/src/bin/bench_fixed_points_symbolic_iterator.rs b/src/bin/bench_fixed_points_symbolic_iterator.rs
index 635f57d..fe793cf 100644
--- a/src/bin/bench_fixed_points_symbolic_iterator.rs
+++ b/src/bin/bench_fixed_points_symbolic_iterator.rs
@@ -15,7 +15,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
     let stg = Arc::new(stg);
 
     let dimensions = usize::from(stg.symbolic_context().bdd_variable_set().num_vars());
diff --git a/src/bin/bench_fixed_points_symbolic_vertices.rs b/src/bin/bench_fixed_points_symbolic_vertices.rs
index fe19fc3..6215524 100644
--- a/src/bin/bench_fixed_points_symbolic_vertices.rs
+++ b/src/bin/bench_fixed_points_symbolic_vertices.rs
@@ -14,7 +14,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let fixed_points = FixedPoints::symbolic_vertices(&stg, stg.unit_colored_vertices());
     println!(
diff --git a/src/bin/bench_reach.rs b/src/bin/bench_reach.rs
index 5d652e1..f5fcd9f 100644
--- a/src/bin/bench_reach.rs
+++ b/src/bin/bench_reach.rs
@@ -15,7 +15,7 @@ fn main() {
         model.num_parameters()
     );
 
-    let stg = SymbolicAsyncGraph::new(model.clone()).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model.clone()).unwrap();
 
     let mut universe = stg.mk_unit_colored_vertices();
     while !universe.is_empty() {
diff --git a/src/bin/bench_trap_spaces_minimal.rs b/src/bin/bench_trap_spaces_minimal.rs
index 46fae55..4108d8f 100644
--- a/src/bin/bench_trap_spaces_minimal.rs
+++ b/src/bin/bench_trap_spaces_minimal.rs
@@ -6,7 +6,7 @@ fn main() {
     let args = std::env::args().collect::<Vec<_>>();
     let bn = BooleanNetwork::try_from_file(args[1].as_str()).unwrap();
     let ctx = SymbolicSpaceContext::new(&bn);
-    let stg = SymbolicAsyncGraph::with_space_context(bn.clone(), &ctx).unwrap();
+    let stg = SymbolicAsyncGraph::with_space_context(&bn.clone(), &ctx).unwrap();
 
     let unit_set = ctx.mk_unit_colored_spaces(&stg);
     let essential_traps = TrapSpaces::essential_symbolic(&bn, &ctx, &unit_set);
diff --git a/src/bin/check_fixed_points.rs b/src/bin/check_fixed_points.rs
index 01c9272..1ee1c56 100644
--- a/src/bin/check_fixed_points.rs
+++ b/src/bin/check_fixed_points.rs
@@ -26,7 +26,7 @@ fn main() {
         model.num_vars(),
         model.num_parameters()
     );
-    let stg = SymbolicAsyncGraph::new(model).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let start = SystemTime::now();
     println!("Search for fixed-point colors...");
diff --git a/src/bin/check_fixed_points_solver.rs b/src/bin/check_fixed_points_solver.rs
index 587c765..be1f000 100644
--- a/src/bin/check_fixed_points_solver.rs
+++ b/src/bin/check_fixed_points_solver.rs
@@ -25,7 +25,7 @@ fn main() {
 
     let z3 = z3::Context::new(&z3::Config::new());
     let ctx = BnSolverContext::new(&z3, model.clone());
-    let stg = SymbolicAsyncGraph::new(model.clone()).unwrap();
+    let stg = SymbolicAsyncGraph::new(&model).unwrap();
 
     let all_vertices = vec![Space::new(&model)];
     let iterator = FixedPoints::solver_iterator(&ctx, &all_vertices, &[]);
diff --git a/src/fixed_points/mod.rs b/src/fixed_points/mod.rs
index 0e518de..f789f36 100644
--- a/src/fixed_points/mod.rs
+++ b/src/fixed_points/mod.rs
@@ -31,7 +31,7 @@ use crate::Space;
 /// (The module is hidden, but we re-export iterator in this module)
 mod symbolic_iterator;
 use crate::symbolic_async_graph::projected_iteration::MixedProjection;
-use crate::VariableId;
+use crate::{BooleanNetwork, VariableId};
 pub use symbolic_iterator::SymbolicIterator;
 
 /// Implements the iterator used by `FixedPoints::solver_iterator`.
@@ -74,7 +74,6 @@ impl FixedPoints {
         }
 
         let mut to_merge: Vec<GraphColoredVertices> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -157,7 +156,6 @@ impl FixedPoints {
         }
 
         let mut to_merge: Vec<Bdd> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -219,6 +217,7 @@ impl FixedPoints {
     /// to subset of states/functions. For now, we do not provide extra methods for this, as it
     /// is not a very common use case. But if you want it, get in touch.
     pub fn symbolic_projection<'a>(
+        network: &BooleanNetwork,
         stg: &'a SymbolicAsyncGraph,
         restriction: &GraphColoredVertices,
         retain_state: &[VariableId],
@@ -233,7 +232,6 @@ impl FixedPoints {
         }
 
         let mut to_merge: Vec<Bdd> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -260,7 +258,7 @@ impl FixedPoints {
             project.remove(&ctx.get_state_variable(*var));
         }
         for var in retain_function {
-            if let Some(function) = stg.as_network().get_update_function(*var) {
+            if let Some(function) = network.get_update_function(*var) {
                 for p_id in function.collect_parameters() {
                     for p in ctx.get_explicit_function_table(p_id).symbolic_variables() {
                         project.remove(p);
@@ -451,7 +449,6 @@ impl FixedPoints {
         }
 
         let mut to_merge: Vec<Bdd> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -482,7 +479,7 @@ impl FixedPoints {
         let bdd =
             Self::symbolic_merge(stg.symbolic_context().bdd_variable_set(), to_merge, project);
 
-        let vertices = stg.empty_vertices().vertices().copy(bdd);
+        let vertices = stg.empty_colored_vertices().vertices().copy(bdd);
 
         if cfg!(feature = "print-progress") {
             println!(
@@ -510,7 +507,6 @@ impl FixedPoints {
         }
 
         let mut to_merge: Vec<Bdd> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -541,7 +537,7 @@ impl FixedPoints {
         let bdd =
             Self::symbolic_merge(stg.symbolic_context().bdd_variable_set(), to_merge, project);
 
-        let colors = stg.empty_vertices().colors().copy(bdd);
+        let colors = stg.empty_colored_vertices().colors().copy(bdd);
 
         if cfg!(feature = "print-progress") {
             println!(
@@ -695,7 +691,7 @@ mod tests {
     #[test]
     pub fn simple_fixed_point_test() {
         let bn = BooleanNetwork::try_from_file("aeon_models/g2a_p9.aeon").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let naive = FixedPoints::naive_symbolic(&stg, stg.unit_colored_vertices());
         let symbolic = FixedPoints::symbolic(&stg, stg.unit_colored_vertices());
@@ -732,13 +728,14 @@ mod tests {
     #[test]
     pub fn simple_projected_fixed_point_test() {
         let bn = BooleanNetwork::try_from_file("aeon_models/g2a_p9.aeon").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn.clone()).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let ccr_m = bn.as_graph().find_variable("CcrM").unwrap();
         let dna = bn.as_graph().find_variable("DnaA").unwrap();
 
         // Compute how DnaA/CcrM fixed-points depend on the CcrM function.
         let projection = FixedPoints::symbolic_projection(
+            &bn,
             &stg,
             stg.unit_colored_vertices(),
             &[ccr_m, dna],
diff --git a/src/fixed_points/solver_iterator.rs b/src/fixed_points/solver_iterator.rs
index 92b9194..d9842be 100644
--- a/src/fixed_points/solver_iterator.rs
+++ b/src/fixed_points/solver_iterator.rs
@@ -200,7 +200,7 @@ mod tests {
         let z3 = z3::Context::new(&z3::Config::new());
 
         let bn = BooleanNetwork::try_from_file("aeon_models/g2a_p1026.aeon").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn.clone()).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let ctx = BnSolverContext::new(&z3, bn.clone());
 
         let mut fixed_points = FixedPoints::naive_symbolic(&stg, stg.unit_colored_vertices());
diff --git a/src/fixed_points/symbolic_iterator.rs b/src/fixed_points/symbolic_iterator.rs
index 0d33691..aef009a 100644
--- a/src/fixed_points/symbolic_iterator.rs
+++ b/src/fixed_points/symbolic_iterator.rs
@@ -186,7 +186,7 @@ impl<'a> Iterator for SymbolicIterator<'a> {
     fn next(&mut self) -> Option<Self::Item> {
         self.inner
             .next()
-            .map(|bdd| self.stg.empty_vertices().copy(bdd))
+            .map(|bdd| self.stg.empty_colored_vertices().copy(bdd))
     }
 }
 
@@ -199,7 +199,6 @@ impl<'a> SymbolicIterator<'a> {
         limit: usize,
     ) -> SymbolicIterator<'a> {
         let mut to_merge: Vec<Bdd> = stg
-            .as_network()
             .variables()
             .map(|var| {
                 let can_step = stg.var_can_post(var, stg.unit_colored_vertices());
@@ -221,7 +220,6 @@ impl<'a> SymbolicIterator<'a> {
         }
 
         let mut clauses: Vec<BddPartialValuation> = stg
-            .as_network()
             .variables()
             .flat_map(|it| {
                 let can_step = stg.var_can_post(it, restriction);
@@ -299,7 +297,7 @@ mod tests {
     #[test]
     pub fn test_symbolic_iterator() {
         let bn = BooleanNetwork::try_from_file("aeon_models/g2a_p1026.aeon").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let mut set = FixedPoints::naive_symbolic(&stg, stg.unit_colored_vertices());
 
diff --git a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs
index 20fbe3f..712c412 100644
--- a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs
+++ b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs
@@ -246,7 +246,7 @@ mod tests {
     #[test]
     fn basic_colored_spaces_set_test() {
         let bn = BooleanNetwork::try_from_file("aeon_models/005.aeon").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn.clone()).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let unit = stg.mk_unit_colored_vertices();
         assert!(!unit.is_singleton());
diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs
index 6dda911..afb9868 100644
--- a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs
+++ b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs
@@ -1,30 +1,34 @@
 use crate::biodivine_std::bitvector::{ArrayBitVector, BitVector};
 use crate::biodivine_std::traits::Set;
 use crate::symbolic_async_graph::_impl_regulation_constraint::apply_regulation_constraints;
+use crate::symbolic_async_graph::_impl_symbolic_async_graph_operators::a_and_b_and_c;
 use crate::symbolic_async_graph::bdd_set::BddSet;
 use crate::symbolic_async_graph::{
     GraphColoredVertices, GraphColors, GraphVertices, SymbolicAsyncGraph, SymbolicContext,
 };
 use crate::trap_spaces::SymbolicSpaceContext;
-use crate::{BooleanNetwork, FnUpdate, VariableId};
+use crate::{
+    BooleanNetwork, FnUpdate, Regulation, RegulatoryGraph, VariableId, VariableIdIterator,
+};
 use crate::{ExtendedBoolean, Space};
 use biodivine_lib_bdd::{bdd, Bdd, BddVariable};
 use std::collections::HashMap;
 
 impl SymbolicAsyncGraph {
-    /// Create a `SymbolicAsyncGraph` based on the default symbolic encoding of the supplied
-    /// `BooleanNetwork` as implemented by `SymbolicContext`.
-    pub fn new(network: BooleanNetwork) -> Result<SymbolicAsyncGraph, String> {
-        let context = SymbolicContext::new(&network)?;
+    /// Create a [SymbolicAsyncGraph] based on the default symbolic encoding of the supplied
+    /// [BooleanNetwork] as implemented by the default [SymbolicContext].
+    pub fn new(network: &BooleanNetwork) -> Result<SymbolicAsyncGraph, String> {
+        let context = SymbolicContext::new(network)?;
         let unit = context.mk_constant(true);
         Self::with_custom_context(network, context, unit)
     }
 
     /// Create a [SymbolicAsyncGraph] that is compatible with an existing [SymbolicSpaceContext].
     ///
-    /// The `network` argument must be the same as used for the creation of the `context` object.
+    /// The [BooleanNetwork] argument must be the same as used for the creation of the
+    /// [SymbolicSpaceContext] object.
     pub fn with_space_context(
-        network: BooleanNetwork,
+        network: &BooleanNetwork,
         context: &SymbolicSpaceContext,
     ) -> Result<SymbolicAsyncGraph, String> {
         let context = context.inner_context().clone();
@@ -32,29 +36,29 @@ impl SymbolicAsyncGraph {
         Self::with_custom_context(network, context, unit)
     }
 
-    /// Create a `SymbolicAsyncGraph` using a given `network`, the symbolic `context` (encoding)
-    /// of said network (possibly with extra symbolic variables), and an initial `unit_bdd` which
-    /// is used to restrict all valid BDDs corresponding to this graph.
+    /// Create a [SymbolicAsyncGraph] based on the given [BooleanNetwork] and a [SymbolicContext]
+    /// (i.e. the network's encoding, possibly with extra symbolic variables). Also takes an
+    /// initial "unit" [Bdd] representing the full set of vertices and colors.
     ///
-    /// However, note that we do not validate that the provided `SymbolicContext` and `Bdd` are
-    /// compatible with the provided network. If you use a context that was not created for the
+    /// However, note that we do not validate that the provided [SymbolicContext] and the [Bdd] are
+    /// compatible with the [BooleanNetwork]. If you use a context that was not created for the
     /// given network, the behaviour is undefined (you'll likely see something fail rather
     /// quickly though).
     ///
     /// Several notes to keep in mind while using this method:
     ///  1. The `unit_bdd` is used as an "initial value" for the set of all states and colors of
     ///     this graph. However, it is still modified to only allow valid parameter valuations,
-    ///     so you can use it to reduce the space of valid states/colors, but it is not necessarily
-    ///     the final "unit set" of the graph.
+    ///     so you can use it to reduce the space of valid states/colors, but it is not
+    ///     necessarily the final "unit set" of the graph.
     ///  2. The presence of extra symbolic variables can modify the semantics of symbolic
     ///     operations implemented on `SymbolicAsyncGraph`, `GraphVertices`, `GraphColors` and
     ///     `GraphColoredVertices`. The `SymbolicAsyncGraph` will not use or depend on the extra
     ///     variables in any capacity. Hence, as long as the extra variables remain unused, all
-    ///     operations should behave as expected. However, once you introduce the variables externally
-    ///     (e.g. using a "raw" BDD operation instead of the "high level" API), you should verify
-    ///     that the semantics of symbolic operations are really what you expect them to be. For
-    ///     example, an intersection on sets will now also depend on the values of the extra
-    ///     variables, not just states and colors.
+    ///     operations should behave as expected. However, once you introduce the variables
+    ///     externally (e.g. using a "raw" BDD operation instead of the "high level" API), you
+    ///     should verify that the semantics of symbolic operations are really what you expect
+    ///     them to be. For example, an intersection on sets will now also depend on the values
+    ///     of the extra variables, not just states and colors.
     ///  3. In general, `unit_bdd` should be a cartesian product of a set of vertices, a set
     ///     of colors, and a set of valuations on the extra variables. If you don't follow this
     ///     requirement, almost everything remains valid, but ultimately, some symbolic operations
@@ -68,52 +72,100 @@ impl SymbolicAsyncGraph {
     ///     subset of states/colors without the cartesian product requirement. Also, we should be
     ///     able to be more transparent/explicit about the presence of extra symbolic variables.
     pub fn with_custom_context(
-        network: BooleanNetwork,
+        network: &BooleanNetwork,
         context: SymbolicContext,
         unit_bdd: Bdd,
     ) -> Result<SymbolicAsyncGraph, String> {
         assert_eq!(network.num_vars(), context.num_state_variables());
-        let unit_bdd = apply_regulation_constraints(unit_bdd, &network, &context)?;
+        let unit_bdd = apply_regulation_constraints(unit_bdd, network, &context)?;
 
-        // For each variable, pre-compute contexts where the update function can be applied, i.e.
-        // (F = 1 & var = 0) | (F = 0 & var = 1)
         let update_functions = network
-            .graph
             .variables()
-            .map(|variable| {
-                let regulators = network.regulators(variable);
-                let function_is_one = network
-                    .get_update_function(variable)
-                    .as_ref()
-                    .map(|fun| context.mk_fn_update_true(fun))
-                    .unwrap_or_else(|| context.mk_implicit_function_is_true(variable, &regulators));
-                let variable_is_zero = context.mk_state_variable_is_true(variable).not();
-                bdd!(variable_is_zero <=> function_is_one)
+            .map(|var| {
+                if let Some(function) = network.get_update_function(var) {
+                    context.mk_fn_update_true(function)
+                } else {
+                    let regulators = network.regulators(var);
+                    context.mk_implicit_function_is_true(var, &regulators)
+                }
             })
-            .collect();
+            .collect::<Vec<_>>();
 
-        Ok(SymbolicAsyncGraph {
-            vertex_space: (
-                GraphColoredVertices::new(context.bdd.mk_false(), &context),
-                GraphColoredVertices::new(unit_bdd.clone(), &context),
-            ),
-            color_space: (
-                GraphColors::new(context.bdd.mk_false(), &context),
-                GraphColors::new(unit_bdd.clone(), &context),
-            ),
-            symbolic_context: context,
-            unit_bdd,
+        unsafe {
+            Ok(SymbolicAsyncGraph::new_raw(
+                Some(network.clone()),
+                context,
+                unit_bdd,
+                update_functions,
+            ))
+        }
+    }
+
+    /// Construct a new [SymbolicAsyncGraph] completely using raw [Bdd] values. You can also
+    /// supply an optional [BooleanNetwork], but this will not be used in any meaningful way.
+    ///
+    ///  - Here, the `unit_bdd` will be used as the set of colors/vertices without any further
+    ///    postprocessing.
+    ///  - The `functions` vector should contains a BDD for each variable which is true if and
+    ///    only if the update function of said variable is true.
+    ///
+    /// # Safety
+    ///
+    /// This is an unsafe function because it is extremely easy to use to create an invalid graph.
+    pub unsafe fn new_raw(
+        network: Option<BooleanNetwork>,
+        symbolic_context: SymbolicContext,
+        unit_bdd: Bdd,
+        functions: Vec<Bdd>,
+    ) -> SymbolicAsyncGraph {
+        assert_eq!(functions.len(), symbolic_context.state_variables().len());
+
+        let fn_update = functions;
+        let fn_transition = fn_update
+            .iter()
+            .enumerate()
+            .map(|(i, fun)| {
+                let var = VariableId::from_index(i);
+                let var = symbolic_context.mk_state_variable_is_true(var);
+                // Either (var=0 and fun=1), or (var=1 and fun=0).
+                bdd!(var ^ fun)
+            })
+            .collect::<Vec<_>>();
+        let colored_vertex_space = (
+            GraphColoredVertices::new(symbolic_context.mk_constant(false), &symbolic_context),
+            GraphColoredVertices::new(unit_bdd.clone(), &symbolic_context),
+        );
+        let vertex_space = (
+            colored_vertex_space.0.vertices(),
+            colored_vertex_space.1.vertices(),
+        );
+        let color_space = (
+            colored_vertex_space.0.colors(),
+            colored_vertex_space.1.colors(),
+        );
+        SymbolicAsyncGraph {
             network,
-            update_functions,
-        })
+            symbolic_context,
+            colored_vertex_space,
+            vertex_space,
+            color_space,
+            unit_bdd,
+            fn_update,
+            fn_transition,
+        }
     }
 }
 
 /// Examine the general properties of the graph.
 impl SymbolicAsyncGraph {
-    /// Return a reference to the original Boolean network.
-    pub fn as_network(&self) -> &BooleanNetwork {
-        &self.network
+    /// Return a reference to the original Boolean network, if there is any.
+    pub fn as_network(&self) -> Option<&BooleanNetwork> {
+        self.network.as_ref()
+    }
+
+    /// Get the symbolic representation of the update function for the given [VariableId].
+    pub fn get_symbolic_fn_update(&self, variable: VariableId) -> &Bdd {
+        &self.fn_update[variable.to_index()]
     }
 
     /// Return a reference to the symbolic context of this graph.
@@ -156,32 +208,51 @@ impl SymbolicAsyncGraph {
             panic!("Cannot create witness for empty color set.");
         }
         let witness_valuation = colors.bdd.sat_witness().unwrap();
-        let mut witness = self.network.clone();
-        for variable in witness.graph.variables() {
-            if let Some(function) = &mut witness.update_functions[variable.0] {
-                let instantiated_expression = self
-                    .symbolic_context
-                    .instantiate_fn_update(&witness_valuation, function);
-
-                *function =
-                    FnUpdate::build_from_bdd(self.symbolic_context(), &instantiated_expression);
-            } else {
-                let regulators = self.network.regulators(variable);
-                let instantiated_expression = self.symbolic_context.instantiate_implicit_function(
-                    &witness_valuation,
-                    variable,
-                    &regulators,
-                );
-                witness.update_functions[variable.0] = Some(FnUpdate::build_from_bdd(
-                    self.symbolic_context(),
-                    &instantiated_expression,
-                ));
+
+        let mut regulators: Vec<Vec<VariableId>> = Vec::new();
+        let mut fn_update: Vec<FnUpdate> = Vec::new();
+        for fn_bdd in &self.fn_update {
+            let dnf = self
+                .symbolic_context
+                .mk_instantiated_fn_update(&witness_valuation, fn_bdd);
+            let regs = dnf.collect_arguments();
+            fn_update.push(dnf);
+            regulators.push(regs);
+        }
+
+        let variables = self
+            .symbolic_context
+            .state_variables()
+            .iter()
+            .map(|it| self.symbolic_context.bdd_variable_set().name_of(*it))
+            .collect::<Vec<_>>();
+        let mut rg = RegulatoryGraph::new(variables);
+        for (i, regs) in regulators.into_iter().enumerate() {
+            let target = VariableId::from_index(i);
+            for regulator in regs {
+                rg.add_raw_regulation(Regulation {
+                    regulator,
+                    target,
+                    observable: false,
+                    monotonicity: None,
+                })
+                .unwrap_or_else(|_| {
+                    unreachable!("Unconstrained regulation should be always allowed here.");
+                });
             }
         }
-        // Remove all explicit parameters since they have been eliminated.
-        witness.parameters.clear();
-        witness.parameter_to_index.clear();
-        witness
+        let mut bn = BooleanNetwork::new(rg);
+        for (i, function) in fn_update.into_iter().enumerate() {
+            let var = VariableId::from_index(i);
+            bn.set_update_function(var, Some(function))
+                .unwrap_or_else(|_| {
+                    unreachable!("Instantiated update function should be always valid here.");
+                })
+        }
+
+        bn.infer_valid_graph().unwrap_or_else(|_| {
+            unreachable!("Symbolic context already exists, so it must not fail.")
+        })
     }
 
     /// Reference to an empty color set.
@@ -191,7 +262,7 @@ impl SymbolicAsyncGraph {
 
     /// Make a new copy of empty color set.
     pub fn mk_empty_colors(&self) -> GraphColors {
-        self.color_space.0.clone()
+        self.empty_colors().clone()
     }
 
     /// Reference to a unit color set.
@@ -201,27 +272,51 @@ impl SymbolicAsyncGraph {
 
     /// Make a new copy of unit color set.
     pub fn mk_unit_colors(&self) -> GraphColors {
-        self.color_space.1.clone()
+        self.unit_colors().clone()
     }
 
     /// Reference to an empty colored vertex set.
-    pub fn empty_vertices(&self) -> &GraphColoredVertices {
-        &self.vertex_space.0
+    pub fn empty_colored_vertices(&self) -> &GraphColoredVertices {
+        &self.colored_vertex_space.0
     }
 
     /// Make a new copy of empty vertex set.
-    pub fn mk_empty_vertices(&self) -> GraphColoredVertices {
-        self.vertex_space.0.clone()
+    pub fn mk_empty_colored_vertices(&self) -> GraphColoredVertices {
+        self.empty_colored_vertices().clone()
     }
 
     /// Reference to a unit colored vertex set.
     pub fn unit_colored_vertices(&self) -> &GraphColoredVertices {
-        &self.vertex_space.1
+        &self.colored_vertex_space.1
     }
 
     /// Make a new copy of unit vertex set.
     pub fn mk_unit_colored_vertices(&self) -> GraphColoredVertices {
-        self.vertex_space.1.clone()
+        self.unit_colored_vertices().clone()
+    }
+
+    pub fn empty_vertices(&self) -> &GraphVertices {
+        &self.vertex_space.0
+    }
+
+    pub fn mk_empty_vertices(&self) -> GraphVertices {
+        self.empty_vertices().clone()
+    }
+
+    pub fn unit_vertices(&self) -> &GraphVertices {
+        &self.vertex_space.1
+    }
+
+    pub fn mk_unit_vertices(&self) -> GraphVertices {
+        self.unit_vertices().clone()
+    }
+
+    pub fn num_vars(&self) -> usize {
+        self.symbolic_context.num_state_variables()
+    }
+
+    pub fn variables(&self) -> VariableIdIterator {
+        (0..self.num_vars()).map(VariableId::from_index)
     }
 
     /// Compute a subset of the unit vertex set that is specified using the given list
@@ -268,7 +363,7 @@ impl SymbolicAsyncGraph {
     /// Construct a vertex set that only contains one vertex, but all colors
     ///
     pub fn vertex(&self, state: &ArrayBitVector) -> GraphColoredVertices {
-        assert_eq!(state.len(), self.network.num_vars());
+        assert_eq!(state.len(), self.num_vars());
         // TODO: When breaking changes will be possible, this should add a `mk_` prefix.
         let partial_valuation: Vec<(BddVariable, bool)> = state
             .values()
@@ -302,11 +397,17 @@ impl SymbolicAsyncGraph {
         SymbolicAsyncGraph {
             network: self.network.clone(),
             symbolic_context: self.symbolic_context.clone(),
-            vertex_space: (self.mk_empty_vertices(), set.clone()),
+            colored_vertex_space: (self.mk_empty_colored_vertices(), set.clone()),
+            vertex_space: (self.mk_empty_vertices(), set.vertices()),
             color_space: (self.mk_empty_colors(), set.colors()),
-            unit_bdd: set.bdd.clone(),
-            update_functions: self
-                .update_functions
+            unit_bdd: set.as_bdd().clone(),
+            // We do not restrict the update functions in any way, because they are still the same,
+            // even in the restricted state space
+            fn_update: self.fn_update.clone(),
+            // However, we restrict the transitions to ensure the source/target state are both
+            // present in the new graph.
+            fn_transition: self
+                .fn_transition
                 .iter()
                 .enumerate()
                 .map(|(i, function)| {
@@ -318,16 +419,7 @@ impl SymbolicAsyncGraph {
                         (&set.bdd, None),
                         (&set.bdd, Some(symbolic_var)),
                         None,
-                        |a, b, c| {
-                            // a & b & c
-                            match (a, b, c) {
-                                (Some(true), Some(true), Some(true)) => Some(true),
-                                (Some(false), _, _) => Some(false),
-                                (_, Some(false), _) => Some(false),
-                                (_, _, Some(false)) => Some(false),
-                                _ => None,
-                            }
-                        },
+                        a_and_b_and_c,
                     )
                 })
                 .collect(),
@@ -349,11 +441,11 @@ impl SymbolicAsyncGraph {
         ) -> GraphColoredVertices {
             let bdd_var = stg.symbolic_context().get_state_variable(var);
             let relaxed_bdd = cube.as_bdd().var_exists(bdd_var);
-            stg.empty_vertices().copy(relaxed_bdd)
+            stg.empty_colored_vertices().copy(relaxed_bdd)
         }
 
         let mut result = set.clone();
-        for var in self.as_network().variables() {
+        for var in self.variables() {
             let var_true = self.fix_network_variable(var, true);
             let var_false = self.fix_network_variable(var, false);
             if !(result.is_subset(&var_true) || result.is_subset(&var_false)) {
@@ -366,8 +458,8 @@ impl SymbolicAsyncGraph {
     /// Find the smallest subspace (hypercube) that contains the given set of vertices.
     pub fn wrap_in_subspace(&self, set: &GraphVertices) -> Space {
         let clause = set.bdd.necessary_clause().unwrap();
-        let mut result = Space::new(self.as_network());
-        for var in self.as_network().variables() {
+        let mut result = Space::new_raw(self.num_vars());
+        for var in self.variables() {
             let bdd_var = self.symbolic_context.state_variables[var.to_index()];
             if let Some(value) = clause.get_value(bdd_var) {
                 if value {
@@ -385,20 +477,24 @@ impl SymbolicAsyncGraph {
     /// update functions no longer depend on it.
     pub fn restrict_variable_in_graph(&self, var: VariableId, value: bool) -> SymbolicAsyncGraph {
         let bdd_var = self.symbolic_context.state_variables[var.0];
+        let new_unit = self.unit_bdd.var_restrict(bdd_var, value);
+        let new_unit_set = GraphColoredVertices::new(new_unit, self.symbolic_context());
         SymbolicAsyncGraph {
             network: self.network.clone(),
             symbolic_context: self.symbolic_context.clone(),
-            vertex_space: (
-                self.mk_empty_vertices(),
-                self.unit_colored_vertices()
-                    .restrict_network_variable(var, value),
-            ),
-            color_space: (self.mk_empty_colors(), self.mk_unit_colors()),
-            unit_bdd: self.unit_bdd.var_restrict(bdd_var, value),
-            update_functions: self
-                .update_functions
+            colored_vertex_space: (self.mk_empty_colored_vertices(), new_unit_set.clone()),
+            vertex_space: (self.mk_empty_vertices(), new_unit_set.vertices()),
+            color_space: (self.mk_empty_colors(), new_unit_set.colors()),
+            unit_bdd: new_unit_set.into_bdd(),
+            fn_update: self
+                .fn_update
+                .iter()
+                .map(|it| it.var_restrict(bdd_var, value))
+                .collect(),
+            fn_transition: self
+                .fn_transition
                 .iter()
-                .map(|f| f.var_restrict(bdd_var, value))
+                .map(|it| it.var_restrict(bdd_var, value))
                 .collect(),
         }
     }
@@ -459,8 +555,14 @@ impl SymbolicAsyncGraph {
     /// instantiations of the sub-network represented using the main network encoding. Otherwise,
     /// an error indicates which conditions were not met.
     ///
+    /// ## Panics
+    ///
+    /// The method requires that [Self::as_network] is `Some`.
+    ///
     pub fn mk_subnetwork_colors(&self, network: &BooleanNetwork) -> Result<GraphColors, String> {
-        let main_network = self.as_network();
+        let main_network = self.as_network().unwrap_or_else(|| {
+            panic!("Requires original network to compute sub-network colors.");
+        });
         let sub_network = network;
         {
             // 1.1 Verify that the networks have the same variables.
@@ -608,7 +710,7 @@ impl SymbolicAsyncGraph {
         }
 
         // 5. Check that the sub-network is valid.
-        let sub_network_graph = SymbolicAsyncGraph::new(sub_network.clone());
+        let sub_network_graph = SymbolicAsyncGraph::new(sub_network);
         if sub_network_graph.is_err() {
             return Err("Sub-network is not consistent with the regulatory graph.".to_string());
         }
@@ -757,11 +859,11 @@ mod tests {
         ",
         )
         .unwrap();
-        let sg = SymbolicAsyncGraph::new(network_1).unwrap();
+        let sg = SymbolicAsyncGraph::new(&network_1).unwrap();
 
         assert_eq!(
             sg.mk_unit_colors(),
-            sg.mk_subnetwork_colors(sg.as_network()).unwrap()
+            sg.mk_subnetwork_colors(&network_1).unwrap()
         );
 
         // Fixes only the function of `a`, not the remaining variables:
@@ -801,7 +903,7 @@ mod tests {
         let sub_colors = sg.mk_subnetwork_colors(&network_3).unwrap();
         assert_eq!(2.0, sub_colors.approx_cardinality());
 
-        let sg_2 = SymbolicAsyncGraph::new(network_2).unwrap();
+        let sg_2 = SymbolicAsyncGraph::new(&network_2).unwrap();
         let sub_colors = sg_2.mk_subnetwork_colors(&network_3).unwrap();
         assert_eq!(2.0, sub_colors.approx_cardinality());
 
@@ -956,22 +1058,22 @@ mod tests {
     #[test]
     fn test_constraints_1() {
         let network = BooleanNetwork::try_from("a -> t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(1.0, graph.unit_colors().approx_cardinality());
         let network = BooleanNetwork::try_from("a -| t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(1.0, graph.unit_colors().approx_cardinality());
         let network = BooleanNetwork::try_from("a ->? t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(3.0, graph.unit_colors().approx_cardinality());
         let network = BooleanNetwork::try_from("a -|? t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(3.0, graph.unit_colors().approx_cardinality());
         let network = BooleanNetwork::try_from("a -? t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(2.0, graph.unit_colors().approx_cardinality());
         let network = BooleanNetwork::try_from("a -?? t \n $a: true").unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(4.0, graph.unit_colors().approx_cardinality());
     }
 
@@ -989,7 +1091,7 @@ mod tests {
             $a: true \n $b: true
         ";
         let network = BooleanNetwork::try_from(network).unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(3.0, graph.unit_colors().approx_cardinality());
     }
 
@@ -1002,7 +1104,7 @@ mod tests {
             $a: true \n $b: true
         ";
         let network = BooleanNetwork::try_from(network).unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(6.0, graph.unit_colors().approx_cardinality());
     }
 
@@ -1013,7 +1115,7 @@ mod tests {
             $a: true \n $b: true \n $c: true
         ";
         let network = BooleanNetwork::try_from(network).unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(20.0, graph.unit_colors().approx_cardinality());
     }
 
@@ -1024,7 +1126,7 @@ mod tests {
             $a: true \n $b: true \n $c: true \n $d: true
         ";
         let network = BooleanNetwork::try_from(network).unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert_eq!(168.0, graph.unit_colors().approx_cardinality());
     }
 
@@ -1035,7 +1137,7 @@ mod tests {
             $a: true \n $b: true \n $t: b
         ";
         let network = BooleanNetwork::try_from(network).unwrap();
-        let graph = SymbolicAsyncGraph::new(network);
+        let graph = SymbolicAsyncGraph::new(&network);
         assert!(graph.is_err());
     }
 
@@ -1053,9 +1155,9 @@ mod tests {
         ",
         )
         .unwrap();
-        let graph = SymbolicAsyncGraph::new(bn).unwrap();
-        let a = graph.as_network().as_graph().find_variable("A").unwrap();
-        let c = graph.as_network().as_graph().find_variable("C").unwrap();
+        let graph = SymbolicAsyncGraph::new(&bn).unwrap();
+        let a = bn.as_graph().find_variable("A").unwrap();
+        let c = bn.as_graph().find_variable("C").unwrap();
         let sub_space_a = graph.fix_network_variable(a, true);
         let sub_space_c = graph.fix_network_variable(c, false);
         let sub_space = sub_space_a.intersect(&sub_space_c);
@@ -1081,10 +1183,10 @@ mod tests {
         ",
         )
         .unwrap();
-        let graph = SymbolicAsyncGraph::new(bn).unwrap();
-        let a = graph.as_network().as_graph().find_variable("A").unwrap();
-        let b = graph.as_network().as_graph().find_variable("B").unwrap();
-        let c = graph.as_network().as_graph().find_variable("C").unwrap();
+        let graph = SymbolicAsyncGraph::new(&bn).unwrap();
+        let a = bn.as_graph().find_variable("A").unwrap();
+        let b = bn.as_graph().find_variable("B").unwrap();
+        let c = bn.as_graph().find_variable("C").unwrap();
 
         let original_a = graph
             .var_can_post(a, graph.unit_colored_vertices())
@@ -1137,7 +1239,7 @@ mod tests {
         ",
         )
         .unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         assert_eq!(32.0, stg.unit_colored_vertices().approx_cardinality());
         assert_eq!(
             8.0,
@@ -1147,12 +1249,12 @@ mod tests {
             4.0,
             stg.unit_colored_vertices().colors().approx_cardinality()
         );
-        assert!(stg.empty_vertices().is_empty());
+        assert!(stg.empty_colored_vertices().is_empty());
         assert!(stg.mk_empty_colors().is_empty());
         assert_eq!(stg.mk_unit_colors(), stg.unit_colored_vertices().colors());
-        assert_eq!(3, stg.as_network().num_vars());
+        assert_eq!(3, bn.num_vars());
 
-        let id_a = stg.as_network().as_graph().find_variable("A").unwrap();
+        let id_a = bn.as_graph().find_variable("A").unwrap();
         stg.fix_network_variable(id_a, true);
         let witness = stg.pick_witness(stg.unit_colors());
         assert_eq!(0, witness.parameters().count());
@@ -1204,7 +1306,7 @@ mod tests {
         let context = SymbolicContext::with_extra_state_variables(&bn, &extra_vars).unwrap();
         // Only allow states where a=1
         let unit = context.mk_state_variable_is_true(a);
-        let stg = SymbolicAsyncGraph::with_custom_context(bn, context, unit).unwrap();
+        let stg = SymbolicAsyncGraph::with_custom_context(&bn, context, unit).unwrap();
 
         // It's not 8, but 4, since the state space is restricted.
         let states = stg.unit_colored_vertices().vertices();
@@ -1253,13 +1355,15 @@ mod tests {
         let g2_c = bn_reduced.as_graph().find_variable("c").unwrap();
 
         // These two graphs should be compatible.
-        let g1 = SymbolicAsyncGraph::new(bn).unwrap();
-        let g2 = SymbolicAsyncGraph::new(bn_reduced).unwrap();
+        let g1 = SymbolicAsyncGraph::new(&bn).unwrap();
+        let g2 = SymbolicAsyncGraph::new(&bn_reduced).unwrap();
 
         // Basic set translation:
         assert_eq!(
-            g1.empty_vertices().as_bdd(),
-            g1.transfer_from(g2.empty_vertices(), &g2).unwrap().as_bdd(),
+            g1.empty_colored_vertices().as_bdd(),
+            g1.transfer_from(g2.empty_colored_vertices(), &g2)
+                .unwrap()
+                .as_bdd(),
         );
         assert_eq!(
             g1.unit_colored_vertices().as_bdd(),
diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs
index a69974e..72d4071 100644
--- a/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs
+++ b/src/symbolic_async_graph/_impl_symbolic_async_graph_algorithm.rs
@@ -14,7 +14,7 @@ impl SymbolicAsyncGraph {
     pub fn reach_forward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
         let mut result = initial.clone();
         'fwd: loop {
-            for var in self.network.variables().rev() {
+            for var in self.variables().rev() {
                 let step = self.var_post_out(var, &result);
                 if !step.is_empty() {
                     result = result.union(&step);
@@ -32,7 +32,7 @@ impl SymbolicAsyncGraph {
     pub fn reach_backward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
         let mut result = initial.clone();
         'bwd: loop {
-            for var in self.network.variables().rev() {
+            for var in self.variables().rev() {
                 let step = self.var_pre_out(var, &result);
                 if !step.is_empty() {
                     result = result.union(&step);
@@ -51,7 +51,7 @@ impl SymbolicAsyncGraph {
     pub fn trap_forward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
         let mut result = initial.clone();
         'fwd: loop {
-            for var in self.network.variables().rev() {
+            for var in self.variables().rev() {
                 let step = self.var_can_post_out(var, &result);
                 if !step.is_empty() {
                     result = result.minus(&step);
@@ -70,7 +70,7 @@ impl SymbolicAsyncGraph {
     pub fn trap_backward(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
         let mut result = initial.clone();
         'bwd: loop {
-            for var in self.network.variables().rev() {
+            for var in self.variables().rev() {
                 let step = self.var_can_pre_out(var, &result);
                 if !step.is_empty() {
                     result = result.minus(&step);
@@ -105,7 +105,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let pivot = stg.unit_colored_vertices().pick_vertex();
         let fwd = stg.reach_forward(&pivot);
diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph_operators.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph_operators.rs
index 79609e3..a9090e8 100644
--- a/src/symbolic_async_graph/_impl_symbolic_async_graph_operators.rs
+++ b/src/symbolic_async_graph/_impl_symbolic_async_graph_operators.rs
@@ -44,7 +44,7 @@ impl SymbolicAsyncGraph {
         let symbolic_var = self.symbolic_context.state_variables[variable.0];
         let output = Bdd::fused_binary_flip_op(
             (&initial.bdd, None),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
             biodivine_lib_bdd::op_function::and,
         );
@@ -66,7 +66,7 @@ impl SymbolicAsyncGraph {
         let symbolic_var = self.symbolic_context.state_variables[variable.0];
         let output = Bdd::fused_binary_flip_op(
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             None,
             biodivine_lib_bdd::op_function::and,
         );
@@ -88,20 +88,11 @@ impl SymbolicAsyncGraph {
         // flip(set & !flip(set) & can_apply_function)
         let symbolic_var = self.symbolic_context.state_variables[variable.0];
         let output = Bdd::fused_ternary_flip_op(
-            (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&initial.bdd, None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
-            |a, b, c| {
-                // a & !b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(true), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(false), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            not_a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -123,18 +114,9 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             None,
-            |a, b, c| {
-                // !a & b & c
-                match (a, b, c) {
-                    (Some(true), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(false), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            not_a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -156,18 +138,9 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
-            |a, b, c| {
-                // a & b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -189,18 +162,9 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             None,
-            |a, b, c| {
-                // a & b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -218,7 +182,7 @@ impl SymbolicAsyncGraph {
     ) -> GraphColoredVertices {
         // set & can_apply_function
         GraphColoredVertices::new(
-            initial.bdd.and(&self.update_functions[variable.0]),
+            initial.bdd.and(&self.fn_transition[variable.0]),
             &self.symbolic_context,
         )
     }
@@ -238,7 +202,7 @@ impl SymbolicAsyncGraph {
         let symbolic_var = self.symbolic_context.state_variables[variable.0];
         let output = Bdd::fused_binary_flip_op(
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
             biodivine_lib_bdd::op_function::and,
         );
@@ -260,20 +224,11 @@ impl SymbolicAsyncGraph {
         // set & !flip(set) & can_apply_function
         let symbolic_var = self.symbolic_context.state_variables[variable.0];
         let output = Bdd::fused_ternary_flip_op(
-            (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&initial.bdd, None),
+            (&self.fn_transition[variable.0], None),
             None,
-            |a, b, c| {
-                // a & !b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(true), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(false), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            not_a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -295,18 +250,9 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
-            |a, b, c| {
-                // !a & b & c
-                match (a, b, c) {
-                    (Some(true), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(false), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            not_a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -328,18 +274,9 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             None,
-            |a, b, c| {
-                // a & b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
@@ -361,23 +298,36 @@ impl SymbolicAsyncGraph {
         let output = Bdd::fused_ternary_flip_op(
             (&initial.bdd, None),
             (&initial.bdd, Some(symbolic_var)),
-            (&self.update_functions[variable.0], None),
+            (&self.fn_transition[variable.0], None),
             Some(symbolic_var),
-            |a, b, c| {
-                // a & b & c
-                match (a, b, c) {
-                    (Some(false), _, _) => Some(false),
-                    (_, Some(false), _) => Some(false),
-                    (_, _, Some(false)) => Some(false),
-                    (Some(true), Some(true), Some(true)) => Some(true),
-                    _ => None,
-                }
-            },
+            a_and_b_and_c,
         );
         GraphColoredVertices::new(output, &self.symbolic_context)
     }
 }
 
+pub(crate) fn a_and_b_and_c(a: Option<bool>, b: Option<bool>, c: Option<bool>) -> Option<bool> {
+    // a & b & c
+    match (a, b, c) {
+        (Some(false), _, _) => Some(false),
+        (_, Some(false), _) => Some(false),
+        (_, _, Some(false)) => Some(false),
+        (Some(true), Some(true), Some(true)) => Some(true),
+        _ => None,
+    }
+}
+
+pub(crate) fn not_a_and_b_and_c(a: Option<bool>, b: Option<bool>, c: Option<bool>) -> Option<bool> {
+    // !a & b & c
+    match (a, b, c) {
+        (Some(true), _, _) => Some(false),
+        (_, Some(false), _) => Some(false),
+        (_, _, Some(false)) => Some(false),
+        (Some(false), Some(true), Some(true)) => Some(true),
+        _ => None,
+    }
+}
+
 /// 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.
@@ -398,36 +348,32 @@ impl SymbolicAsyncGraph {
 impl SymbolicAsyncGraph {
     /// Compute the result of applying `post` with *all* update functions to the `initial` set.
     pub fn post(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_post(v, initial))
             })
     }
 
     /// Compute the result of applying `pre` with *all* update functions to the `initial` set.
     pub fn pre(&self, initial: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_pre(v, initial))
             })
     }
 
     /// Compute the subset of `set` that can perform *some* `post` operation.
     pub fn can_post(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_post(v, set))
             })
     }
 
     /// Compute the subset of `set` that can perform *some* `pre` operation.
     pub fn can_pre(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_pre(v, set))
             })
     }
@@ -435,9 +381,8 @@ impl SymbolicAsyncGraph {
     /// Compute the subset of `set` that can perform *some* `post` operation which leads
     /// to a state within `set`.
     pub fn can_post_within(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_post_within(v, set))
             })
     }
@@ -447,17 +392,15 @@ impl SymbolicAsyncGraph {
     ///
     /// Note that this also includes states which cannot perform any `post` operation.
     pub fn will_post_within(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
+        self.variables()
             .fold(set.clone(), |r, v| r.minus(&self.var_can_post_out(v, set)))
     }
 
     /// Compute the subset of `set` that can perform *some* `pre` operation which leads
     /// to a state within `set`.
     pub fn can_pre_within(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_pre_within(v, set))
             })
     }
@@ -467,17 +410,15 @@ impl SymbolicAsyncGraph {
     ///
     /// Note that this also includes states which cannot perform any `pre` operation.
     pub fn will_pre_within(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
+        self.variables()
             .fold(set.clone(), |r, v| r.minus(&self.var_can_pre_out(v, set)))
     }
 
     /// Compute the subset of `set` that can perform *some* `post` operation which leads
     /// to a state outside of `set`.
     pub fn can_post_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_post_out(v, set))
             })
     }
@@ -487,7 +428,7 @@ impl SymbolicAsyncGraph {
     ///
     /// Note that this also includes states which cannot perform any `post` operation.
     pub fn will_post_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network.variables().fold(set.clone(), |r, v| {
+        self.variables().fold(set.clone(), |r, v| {
             r.minus(&self.var_can_post_within(v, set))
         })
     }
@@ -495,9 +436,8 @@ impl SymbolicAsyncGraph {
     /// Compute the subset of `set` that can perform *some* `pre` operation which leads
     /// to a state outside of `set`.
     pub fn can_pre_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network
-            .variables()
-            .fold(self.mk_empty_vertices(), |r, v| {
+        self.variables()
+            .fold(self.mk_empty_colored_vertices(), |r, v| {
                 r.union(&self.var_can_pre_out(v, set))
             })
     }
@@ -507,7 +447,7 @@ impl SymbolicAsyncGraph {
     ///
     /// Note that this also includes states which cannot perform any `pre` operation.
     pub fn will_pre_out(&self, set: &GraphColoredVertices) -> GraphColoredVertices {
-        self.network.variables().fold(set.clone(), |r, v| {
+        self.variables().fold(set.clone(), |r, v| {
             r.minus(&self.var_can_pre_within(v, set))
         })
     }
@@ -535,8 +475,8 @@ mod tests {
         ",
         )
         .unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
-        let id_b = stg.as_network().as_graph().find_variable("B").unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
+        let id_b = bn.as_graph().find_variable("B").unwrap();
         let b_is_true = stg.fix_network_variable(id_b, true);
         let b_is_false = stg.fix_network_variable(id_b, false);
 
diff --git a/src/symbolic_async_graph/_impl_symbolic_context.rs b/src/symbolic_async_graph/_impl_symbolic_context.rs
index 892402e..4450251 100644
--- a/src/symbolic_async_graph/_impl_symbolic_context.rs
+++ b/src/symbolic_async_graph/_impl_symbolic_context.rs
@@ -196,6 +196,15 @@ impl SymbolicContext {
         self.state_variables[variable.0]
     }
 
+    /// Try to find a [VariableId] which corresponds to the given [BddVariable], assuming
+    /// the [BddVariable] is one of the [Self::state_variables].
+    pub fn find_state_variable(&self, symbolic_variable: BddVariable) -> Option<VariableId> {
+        self.state_variables
+            .iter()
+            .position(|it| *it == symbolic_variable)
+            .map(VariableId::from_index)
+    }
+
     /// Get the `BddVariable` extra symbolic variable associated with a particular BN variable
     /// and an offset (within the domain of said variable).
     pub fn get_extra_state_variable(&self, variable: VariableId, offset: usize) -> BddVariable {
@@ -385,6 +394,20 @@ impl SymbolicContext {
         }
     }
 
+    /// Build a DNF representation of an instantiated update function (given as [Bdd]).
+    pub fn mk_instantiated_fn_update(&self, valuation: &BddValuation, function: &Bdd) -> FnUpdate {
+        let parameter_valuation = self
+            .parameter_variables()
+            .iter()
+            .map(|it| (*it, valuation[*it]))
+            .collect::<Vec<_>>();
+
+        // This should fix all parameters to their respective values.
+        let restricted = function.restrict(&parameter_valuation);
+
+        FnUpdate::build_from_bdd(self, &restricted)
+    }
+
     /// **(internal)** Utility method for converting `FnUpdate` arguments to `Bdd` arguments.
     fn prepare_args(&self, args: &[FnUpdate]) -> Vec<Bdd> {
         return args.iter().map(|v| self.mk_fn_update_true(v)).collect();
@@ -446,7 +469,7 @@ mod tests {
     fn hmox_pathway() {
         let model = std::fs::read_to_string("aeon_models/hmox_pathway.aeon").unwrap();
         let network = BooleanNetwork::try_from(model.as_str()).unwrap();
-        let graph = SymbolicAsyncGraph::new(network).unwrap();
+        let graph = SymbolicAsyncGraph::new(&network).unwrap();
         assert!(!graph.unit_colored_vertices().is_empty());
     }
 
diff --git a/src/symbolic_async_graph/mod.rs b/src/symbolic_async_graph/mod.rs
index ae8f7ed..a53130e 100644
--- a/src/symbolic_async_graph/mod.rs
+++ b/src/symbolic_async_graph/mod.rs
@@ -116,17 +116,25 @@ pub struct GraphVertexIterator {
 /// Provides standard pre/post operations for exploring the graph symbolically.
 #[derive(Clone)]
 pub struct SymbolicAsyncGraph {
-    network: BooleanNetwork,
+    // If available, provides the original network that was used to create the graph.
+    // We should not rely on the network being available though, as the graph can be created
+    // in different ways as well.
+    network: Option<BooleanNetwork>,
     symbolic_context: SymbolicContext,
     // Empty and unit vertex set.
-    vertex_space: (GraphColoredVertices, GraphColoredVertices),
+    colored_vertex_space: (GraphColoredVertices, GraphColoredVertices),
+    // Empty and unit vertex set.
+    vertex_space: (GraphVertices, GraphVertices),
     // Empty and unit color set.
     color_space: (GraphColors, GraphColors),
     // General symbolic unit bdd.
     unit_bdd: Bdd,
+    // A `Bdd` which stores the exact asynchronous update function `f_i(x)` for
+    // each variable `x_i`.
+    fn_update: Vec<Bdd>,
     // For every update function, stores `x_i != f_i(x)` (used for pre/post).
-    // In other words, symbolically this is the set of states where a transition is enabled.
-    update_functions: Vec<Bdd>,
+    // In other words, this is the symbolic set of states where a transition is enabled.
+    fn_transition: Vec<Bdd>,
 }
 
 /// Symbolic context manages the mapping between entities of the Boolean network
@@ -234,7 +242,7 @@ mod tests {
         ",
         )
         .unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let components = scc(&stg);
         assert_eq!(7, components.len());
         assert_eq!(2.0, components[0].vertices().approx_cardinality());
diff --git a/src/symbolic_async_graph/projected_iteration.rs b/src/symbolic_async_graph/projected_iteration.rs
index 8375bb0..c61e6c9 100644
--- a/src/symbolic_async_graph/projected_iteration.rs
+++ b/src/symbolic_async_graph/projected_iteration.rs
@@ -353,49 +353,31 @@ fn instantiate_functions(
 ) -> Vec<(VariableId, FnUpdate)> {
     let mut data = Vec::new();
     for var in retained {
-        let symbolic_instance = if let Some(function) = context.network.get_update_function(*var) {
-            context
-                .symbolic_context()
-                .instantiate_fn_update(valuation, function)
-        } else {
-            let arguments = context.as_network().regulators(*var);
-            context
-                .symbolic_context()
-                .instantiate_implicit_function(valuation, *var, &arguments)
-        };
-        let fn_update = FnUpdate::build_from_bdd(context.symbolic_context(), &symbolic_instance);
+        let symbolic_function = &context.fn_update[var.to_index()];
+        let fn_update = context
+            .symbolic_context()
+            .mk_instantiated_fn_update(valuation, symbolic_function);
         data.push((*var, fn_update));
     }
     data
 }
 
-/// Collect the symbolic variables that are necessary to instantiate the `retained` update
-/// functions of the network from `context`.
+/// Collect the symbolic parameter variables that are necessary to instantiate the
+/// `retained` update functions of the network from `context`.
 fn collect_fn_update_parameters(
     context: &SymbolicAsyncGraph,
     retained: &[VariableId],
 ) -> HashSet<BddVariable> {
     let symbolic_context = context.symbolic_context();
     let mut retained_symbolic = HashSet::new();
+    // First, collect all variables that are relevant.
     for var in retained {
-        if let Some(fn_update) = context.as_network().get_update_function(*var) {
-            // Retain all symbolic variables of the function's parameters.
-            for param in fn_update.collect_parameters() {
-                for s_var in symbolic_context
-                    .get_explicit_function_table(param)
-                    .symbolic_variables()
-                {
-                    retained_symbolic.insert(*s_var);
-                }
-            }
-        } else {
-            for s_var in symbolic_context
-                .get_implicit_function_table(*var)
-                .symbolic_variables()
-            {
-                retained_symbolic.insert(*s_var);
-            }
-        }
+        let update = context.get_symbolic_fn_update(*var);
+        retained_symbolic.extend(update.support_set());
+    }
+    // Then remove state variables to only keep parameter variables.
+    for state_var in symbolic_context.state_variables() {
+        retained_symbolic.remove(state_var);
     }
     retained_symbolic
 }
@@ -422,7 +404,7 @@ mod tests {
         let b = v.next().unwrap();
         let c = v.next().unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let a0b0 = stg.mk_subspace(&[(a, false), (b, false)]);
         let b1c1 = stg.mk_subspace(&[(b, true), (c, true)]);
@@ -432,23 +414,20 @@ mod tests {
         let ab_projection = union.state_projection(&[a, b]).iter().collect::<Vec<_>>();
         let bc_projection = union.state_projection(&[b, c]).iter().collect::<Vec<_>>();
 
-        assert_eq!(
-            ab_projection,
-            vec![
-                vec![(a, false), (b, false)],
-                vec![(a, false), (b, true)],
-                vec![(a, true), (b, true)],
-            ]
-        );
+        let ab_expected = vec![
+            vec![(a, false), (b, false)],
+            vec![(a, false), (b, true)],
+            vec![(a, true), (b, true)],
+        ];
 
-        assert_eq!(
-            bc_projection,
-            vec![
-                vec![(b, false), (c, false)],
-                vec![(b, false), (c, true)],
-                vec![(b, true), (c, true)]
-            ]
-        );
+        let bc_expected = vec![
+            vec![(b, false), (c, false)],
+            vec![(b, false), (c, true)],
+            vec![(b, true), (c, true)],
+        ];
+
+        assert_eq!(ab_projection, ab_expected);
+        assert_eq!(bc_projection, bc_expected);
 
         // The same should be true for vertices only:
 
@@ -457,23 +436,8 @@ mod tests {
         let ab_projection = union.state_projection(&[a, b]).iter().collect::<Vec<_>>();
         let bc_projection = union.state_projection(&[b, c]).iter().collect::<Vec<_>>();
 
-        assert_eq!(
-            ab_projection,
-            vec![
-                vec![(a, false), (b, false)],
-                vec![(a, false), (b, true)],
-                vec![(a, true), (b, true)],
-            ]
-        );
-
-        assert_eq!(
-            bc_projection,
-            vec![
-                vec![(b, false), (c, false)],
-                vec![(b, false), (c, true)],
-                vec![(b, true), (c, true)]
-            ]
-        );
+        assert_eq!(ab_projection, ab_expected);
+        assert_eq!(bc_projection, bc_expected);
     }
 
     #[test]
@@ -493,7 +457,7 @@ mod tests {
         let b = v.next().unwrap();
         let c = v.next().unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let can_update_a = stg.var_can_post(a, stg.unit_colored_vertices());
         let can_update_b = stg.var_can_post(b, stg.unit_colored_vertices());
@@ -567,7 +531,7 @@ mod tests {
         let b = v.next().unwrap();
         let c = v.next().unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let can_update_a = stg.var_can_post(a, stg.unit_colored_vertices());
         let can_update_b = stg.var_can_post(b, stg.unit_colored_vertices());
diff --git a/src/trap_spaces/_impl_network_colored_spaces.rs b/src/trap_spaces/_impl_network_colored_spaces.rs
index 8a5a1d3..3353b99 100644
--- a/src/trap_spaces/_impl_network_colored_spaces.rs
+++ b/src/trap_spaces/_impl_network_colored_spaces.rs
@@ -216,7 +216,7 @@ mod tests {
     fn basic_colored_spaces_set_test() {
         let bn = BooleanNetwork::try_from_file("aeon_models/005.aeon").unwrap();
         let ctx = SymbolicSpaceContext::new(&bn);
-        let stg = SymbolicAsyncGraph::with_space_context(bn.clone(), &ctx).unwrap();
+        let stg = SymbolicAsyncGraph::with_space_context(&bn, &ctx).unwrap();
 
         let unit = ctx.mk_unit_colored_spaces(&stg);
         assert!(!unit.is_singleton());
diff --git a/src/trap_spaces/_impl_trap_spaces.rs b/src/trap_spaces/_impl_trap_spaces.rs
index acf2f55..73ec53b 100644
--- a/src/trap_spaces/_impl_trap_spaces.rs
+++ b/src/trap_spaces/_impl_trap_spaces.rs
@@ -219,7 +219,7 @@ mod tests {
     fn test_trap_spaces() {
         let network = BooleanNetwork::try_from_file("./aeon_models/005.aeon").unwrap();
         let ctx = SymbolicSpaceContext::new(&network);
-        let stg = SymbolicAsyncGraph::with_space_context(network.clone(), &ctx).unwrap();
+        let stg = SymbolicAsyncGraph::with_space_context(&network, &ctx).unwrap();
         let unit = ctx.mk_unit_colored_spaces(&stg);
 
         let essential_traps = TrapSpaces::essential_symbolic(&network, &ctx, &unit);
diff --git a/src/tutorial/p03_symbolic_async_graph.rs b/src/tutorial/p03_symbolic_async_graph.rs
index 2681f42..00239bc 100644
--- a/src/tutorial/p03_symbolic_async_graph.rs
+++ b/src/tutorial/p03_symbolic_async_graph.rs
@@ -44,7 +44,7 @@
 //! // At this point, the implementation checks if there is at least one parametrisation which
 //! // satisfies all the requirements imposed by the RegulatoryGraph. If no such parametrisation
 //! // exists, an error is returned, typically also with an explanation why.
-//! let stg = SymbolicAsyncGraph::new(bn)?;
+//! let stg = SymbolicAsyncGraph::new(&bn)?;
 //!
 //! // Once we have a `SymbolicAsyncGraph`, we can access the `GraphVertices`, `GraphColors`
 //! // and `GraphColoredVertices`. Basic methods return a reference, `mk_*` methods create
@@ -52,18 +52,20 @@
 //! assert_eq!(32.0, stg.unit_colored_vertices().approx_cardinality());
 //! assert_eq!(8.0, stg.unit_colored_vertices().vertices().approx_cardinality());
 //! assert_eq!(4.0, stg.unit_colored_vertices().colors().approx_cardinality());
-//! assert!(stg.empty_vertices().is_empty());
+//! assert!(stg.empty_colored_vertices().is_empty());
 //! assert!(stg.mk_empty_colors().is_empty());
 //! assert_eq!(stg.mk_unit_colors(), stg.unit_colored_vertices().colors());
 //! // WARNING: Remember that floating point numbers may not be exact for larger values.
 //! // In fact, for some very large models, the set size can be simply approximated to infinity.
 //!
 //! // You can still access the underlying network of the graph:
-//! assert_eq!(3, stg.as_network().num_vars());
+//! assert_eq!(3, stg.as_network().unwrap().num_vars());
+//! // Just note that in some advanced instances, the network may not exist, in which case
+//! // `as_network` returns `None`
 //!
 //! // You can also obtain a set where all vertices have a Boolean variable set
 //! // to the given value:
-//! let id_a = stg.as_network().as_graph().find_variable("A").unwrap();
+//! let id_a = bn.as_graph().find_variable("A").unwrap();
 //! let a_is_true: GraphColoredVertices = stg.fix_network_variable(id_a, true);
 //! // This can be used to (for example) construct a set of initial states specified by the user.
 //!
@@ -131,8 +133,8 @@
 //! #     A -| A
 //! #     $A: C | f(A, B)
 //! # ").unwrap();
-//! # let stg = SymbolicAsyncGraph::new(bn)?;
-//! let id_b = stg.as_network().as_graph().find_variable("B").unwrap();
+//! # let stg = SymbolicAsyncGraph::new(&bn)?;
+//! let id_b = bn.as_graph().find_variable("B").unwrap();
 //! let b_is_true = stg.fix_network_variable(id_b, true);
 //! let b_is_false = stg.fix_network_variable(id_b, false);
 //!
diff --git a/src/tutorial/p04_graph_algorithm_sample.rs b/src/tutorial/p04_graph_algorithm_sample.rs
index 52bd3d1..a73e5ee 100644
--- a/src/tutorial/p04_graph_algorithm_sample.rs
+++ b/src/tutorial/p04_graph_algorithm_sample.rs
@@ -94,7 +94,7 @@
 //!     A -| A
 //!     $A: C | f(A, B)
 //! ").unwrap();
-//! let stg = SymbolicAsyncGraph::new(bn).unwrap();
+//! let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 //!
 //! // Note that since the symbolic graph contains different transitions for different colors,
 //! // this will create SCCs that overlap for some colors but are completely different for others.