diff --git a/Cargo.toml b/Cargo.toml
index 2a3055f..03ee6a7 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -12,18 +12,20 @@ rustdoc-args = ["--html-in-header", "docs-head.html"]
 [profile.release]
 # This is important for profiling - otherwise we would get unreadable traces.
 #debug = true
-# This gives a marginally better runtime, but a much much longer compile times, so disabled by default.
+# This gives a marginally better runtime, but a much, much longer compile times, so disabled by default.
 #lto = true
 
 [dependencies]
-biodivine-lib-bdd = "0.4.0"
-biodivine-lib-param-bn = "0.3.0"
-rocket = "0.5.0-rc.1"
+biodivine-lib-bdd = "0.5.19"
+biodivine-lib-param-bn = "0.5.11"
+rocket = "0.5.1"
+rocket_cors = "0.6.0"
 json = "0.12.4"
-regex = "1.5.4"
-rand = "0.8.1"
-futures = "0.3.21"
-tokio = "1.18.1"
-fixed-map = "0.7.2"
+regex = "1.10.6"
+rand = "0.8.5"
+futures = "0.3.30"
+tokio = "1.40.0"
+fixed-map = "0.9.5"
+lazy_static = "1.5.0"
 
 [dev-dependencies]
\ No newline at end of file
diff --git a/src/_impl_graph_task_context.rs b/src/_impl_graph_task_context.rs
index 5f801d1..443fc23 100644
--- a/src/_impl_graph_task_context.rs
+++ b/src/_impl_graph_task_context.rs
@@ -29,7 +29,7 @@ impl GraphTaskContext {
         self.is_cancelled.load(Ordering::SeqCst)
     }
 
-    /// Set the status of this task to cancelled.
+    /// Set the status of this task to cancel.
     ///
     /// Return true if the computation was set to cancelled by this call, false if it was
     /// cancelled previously.
diff --git a/src/algorithms/asymptotic_behaviour.rs b/src/algorithms/asymptotic_behaviour.rs
index 20b6832..ef4852c 100644
--- a/src/algorithms/asymptotic_behaviour.rs
+++ b/src/algorithms/asymptotic_behaviour.rs
@@ -13,7 +13,7 @@ use std::sync::Arc;
 
 /// Describes a possible asymptotic behaviour of a discrete system.
 /// Intuitively:
-///     - `Stability` is when all of the system variables reach a fixed state.
+///     - `Stability` is when all the system variables reach a fixed state.
 ///     - `Oscillation` is when some system variables change predictably and the rest
 ///     has a fixed state.
 ///     - `Disorder` is when some system variables change in a non-deterministic, unpredictable
@@ -127,7 +127,7 @@ impl AsymptoticBehaviour {
     ///
     /// Note that it doesn't matter whether the variable update leaves the `set` or stays within.
     /// Both count as unstable. However, you can use `SymbolicAsyncGraph::restrict` to disregard
-    /// updates leading outside of the provided `set`.
+    /// updates leading outside the provided `set`.
     pub fn check_variable_stability(
         stg: &SymbolicAsyncGraph,
         set: &GraphColoredVertices,
@@ -147,8 +147,7 @@ impl AsymptoticBehaviour {
     /// This method should be slightly faster than computing `AsymptoticBehaviour::classify`
     /// in full.
     pub fn check_stability(stg: &SymbolicAsyncGraph, set: &GraphColoredVertices) -> GraphColors {
-        stg.as_network()
-            .variables()
+        stg.variables()
             .map(|var| Self::check_variable_stability(stg, set, var))
             .fold(set.colors(), |a, b| a.intersect(&b))
     }
@@ -199,10 +198,10 @@ impl AsymptoticBehaviour {
         // transitions are discovered. Any color that appears in `successor_zero` or
         // `successor_more` is guaranteed to not have only deterministic cycles.
         let mut successors_zero = set.clone();
-        let mut successors_one = stg.mk_empty_vertices();
-        let mut successors_more = stg.mk_empty_vertices();
+        let mut successors_one = stg.mk_empty_colored_vertices();
+        let mut successors_more = stg.mk_empty_colored_vertices();
 
-        for var in stg.as_network().variables() {
+        for var in stg.variables() {
             let can_change = stg.var_can_post(var, set);
 
             let move_to_one = successors_zero.intersect(&can_change);
@@ -242,7 +241,7 @@ impl AsymptoticBehaviour {
         set: Arc<GraphColoredVertices>,
     ) -> AsymptoticBehaviourMap {
         let all_colors = set.colors();
-        let variables = stg.as_network().variables().collect();
+        let variables = stg.variables().collect();
         let [zero, one, more] = Self::classify_recursive(stg.clone(), set.clone(), variables).await;
 
         let stability = zero.colors().minus(&one.colors()).minus(&more.colors());
@@ -261,14 +260,18 @@ impl AsymptoticBehaviour {
         set: Arc<GraphColoredVertices>,
         variables: Vec<VariableId>,
     ) -> BoxFuture<'static, [GraphColoredVertices; 3]> {
-        return if variables.len() == 1 {
+        if variables.len() == 1 {
             // If there is only one variable remaining, compute states that can perform transition
             // with this variable. These are marked as "one transition", remaining are
             // "zero transitions".
             let var = variables[0];
             Box::pin(async move {
                 let can_post = stg.var_can_post(var, &set);
-                [set.minus(&can_post), can_post, stg.mk_empty_vertices()]
+                [
+                    set.minus(&can_post),
+                    can_post,
+                    stg.mk_empty_colored_vertices(),
+                ]
             })
         } else {
             // If there are more variables, split into two branches and continue each
@@ -289,7 +292,7 @@ impl AsymptoticBehaviour {
                 let zero = l_zero.intersect(&r_zero);
                 [zero, one, more]
             })
-        };
+        }
     }
 }
 
@@ -322,7 +325,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let all_colors = stg.mk_unit_colors();
 
         let t_state = stg.vertex(&ArrayBitVector::from(vec![true, true]));
@@ -343,10 +346,7 @@ mod tests {
             );
         }
 
-        assert_symbolic_eq!(
-            sink_colors.as_bdd(),
-            classification.get(AsymptoticBehaviour::Stability).as_bdd()
-        );
+        assert_symbolic_eq!(sink_colors.as_bdd(), classification.get(Stability).as_bdd());
     }
 
     #[tokio::test]
@@ -361,7 +361,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let all_colors = stg.mk_unit_colors();
 
         let t_state = stg.vertex(&ArrayBitVector::from(vec![true, true]));
@@ -383,10 +383,7 @@ mod tests {
             );
         }
 
-        assert_symbolic_eq!(
-            sink_colors.as_bdd(),
-            classification.get(AsymptoticBehaviour::Stability).as_bdd()
-        );
+        assert_symbolic_eq!(sink_colors.as_bdd(), classification.get(Stability).as_bdd());
     }
 
     #[tokio::test]
@@ -402,7 +399,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let all_colors = stg.mk_unit_colors();
 
         let t_state = stg.vertex(&ArrayBitVector::from(vec![true, true]));
@@ -426,9 +423,7 @@ mod tests {
 
         assert_symbolic_eq!(
             oscillation_colors.as_bdd(),
-            classification
-                .get(AsymptoticBehaviour::Oscillation)
-                .as_bdd()
+            classification.get(Oscillation).as_bdd()
         );
     }
 
@@ -443,7 +438,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let all_states = stg.mk_unit_colored_vertices();
         let all_colors = stg.mk_unit_colors();
 
@@ -463,7 +458,7 @@ mod tests {
 
         assert_symbolic_eq!(
             disordered_colors.as_bdd(),
-            classification.get(AsymptoticBehaviour::Disorder).as_bdd()
+            classification.get(Disorder).as_bdd()
         );
     }
 
@@ -480,7 +475,7 @@ mod tests {
         )
         .unwrap();
 
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let all_states = stg.mk_unit_colored_vertices();
         let all_colors = stg.mk_unit_colors();
 
diff --git a/src/algorithms/asymptotic_behaviour_classifier.rs b/src/algorithms/asymptotic_behaviour_classifier.rs
index 11c45fc..7497e89 100644
--- a/src/algorithms/asymptotic_behaviour_classifier.rs
+++ b/src/algorithms/asymptotic_behaviour_classifier.rs
@@ -15,7 +15,7 @@ pub struct Class(Set<AsymptoticBehaviour>);
 
 impl Feature for Class {
     fn extend(&self, other: &Self) -> Self {
-        let mut set = self.0.clone();
+        let mut set = self.0;
         for value in other.0.iter() {
             set.insert(value);
         }
@@ -99,6 +99,10 @@ impl AsymptoticBehaviourClassifier {
         self.classifier.len()
     }
 
+    pub fn is_empty(&self) -> bool {
+        self.classifier.is_empty()
+    }
+
     /// Extend this classifier using a full behaviour classification map.
     pub fn add_classification(&mut self, classification: &AsymptoticBehaviourMap) {
         for (behaviour, colors) in classification.clone().to_vec() {
@@ -142,7 +146,7 @@ mod tests {
         // works as expected.
 
         let a = bn.as_graph().find_variable("a").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let a_true = stg.fix_network_variable(a, true);
         let a_false = stg.fix_network_variable(a, false);
diff --git a/src/algorithms/asymptotic_behaviour_counter.rs b/src/algorithms/asymptotic_behaviour_counter.rs
index 01ffab4..a0eee36 100644
--- a/src/algorithms/asymptotic_behaviour_counter.rs
+++ b/src/algorithms/asymptotic_behaviour_counter.rs
@@ -15,7 +15,7 @@ pub struct Count(Map<AsymptoticBehaviour, usize>);
 
 impl Feature for Count {
     fn extend(&self, other: &Self) -> Self {
-        let mut map = self.0.clone();
+        let mut map = self.0;
         for (key, value) in other.0.iter() {
             if let Some(current) = map.get(key) {
                 let new_count = *value + *current;
@@ -103,6 +103,10 @@ impl AsymptoticBehaviourCounter {
         self.counter.len()
     }
 
+    pub fn is_empty(&self) -> bool {
+        self.counter.is_empty()
+    }
+
     /// Extend this classifier using a full behaviour classification map.
     pub fn add_classification(&mut self, classification: &AsymptoticBehaviourMap) {
         for (behaviour, colors) in classification.clone().to_vec() {
@@ -146,7 +150,7 @@ mod tests {
         // works as expected.
 
         let a = bn.as_graph().find_variable("a").unwrap();
-        let stg = SymbolicAsyncGraph::new(bn).unwrap();
+        let stg = SymbolicAsyncGraph::new(&bn).unwrap();
 
         let a_true = stg.fix_network_variable(a, true);
         let a_false = stg.fix_network_variable(a, false);
diff --git a/src/algorithms/attractors/itgr/itgr_process.rs b/src/algorithms/attractors/itgr/itgr_process.rs
index f31e2c0..45d9f70 100644
--- a/src/algorithms/attractors/itgr/itgr_process.rs
+++ b/src/algorithms/attractors/itgr/itgr_process.rs
@@ -1,8 +1,8 @@
+use crate::algorithms::attractors::itgr::itgr_process::ProcessState::*;
+use crate::algorithms::attractors::itgr::reachability_process::{BwdProcess, FwdProcess};
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
-use crate::algorithms::attractors::itgr::itgr_process::ProcessState::*;
-use crate::algorithms::attractors::itgr::reachability_process::{BwdProcess, FwdProcess};
 
 pub struct ItgrProcess {
     last_timestamp: usize,
@@ -12,33 +12,32 @@ pub struct ItgrProcess {
 }
 
 enum ProcessState {
-    FwdPhase {
+    Fwd {
         fwd: FwdProcess,
     },
-    FwdBasinPhase {
+    FwdBasin {
         fwd: GraphColoredVertices,
         fwd_basin: BwdProcess,
     },
-    CmpPhase {
+    Cmp {
         fwd: GraphColoredVertices,
         cmp: BwdProcess,
     },
-    TrapPhase {
+    Trap {
         cmp: GraphColoredVertices,
         trap: GraphColoredVertices,
         trap_basin: BwdProcess,
-    }
+    },
 }
 
 impl ItgrProcess {
-
     pub fn new(stg: &SymbolicAsyncGraph, variable: VariableId) -> ItgrProcess {
         let pivots = stg.var_can_post(variable, stg.unit_colored_vertices());
         ItgrProcess {
             variable,
             root_stg: stg.clone(),
-            state: FwdPhase {
-                fwd: FwdProcess::new(stg.clone(), pivots)
+            state: Fwd {
+                fwd: FwdProcess::new(stg.clone(), pivots),
             },
             last_timestamp: 0,
         }
@@ -52,16 +51,20 @@ impl ItgrProcess {
         self.last_timestamp = timestamp;
         self.root_stg = self.root_stg.restrict(universe);
         match &mut self.state {
-            FwdPhase { fwd } => fwd.restrict(universe),
-            FwdBasinPhase { fwd, fwd_basin } => {
+            Fwd { fwd } => fwd.restrict(universe),
+            FwdBasin { fwd, fwd_basin } => {
                 *fwd = fwd.intersect(universe);
                 fwd_basin.restrict(universe);
-            },
-            CmpPhase { fwd, cmp } => {
+            }
+            Cmp { fwd, cmp } => {
                 *fwd = fwd.intersect(universe);
                 cmp.restrict(universe);
-            },
-            TrapPhase { cmp, trap, trap_basin } => {
+            }
+            Trap {
+                cmp,
+                trap,
+                trap_basin,
+            } => {
                 *cmp = cmp.intersect(universe);
                 *trap = trap.intersect(universe);
                 trap_basin.restrict(universe);
@@ -71,17 +74,17 @@ impl ItgrProcess {
 
     pub async fn step(&mut self) -> (bool, Option<GraphColoredVertices>) {
         match &mut self.state {
-            FwdPhase { fwd } => {
+            Fwd { fwd } => {
                 if fwd.step().await {
                     let fwd = fwd.finish();
-                    self.state = FwdBasinPhase {
+                    self.state = FwdBasin {
                         fwd: fwd.clone(),
                         fwd_basin: BwdProcess::new(self.root_stg.clone(), fwd),
                     }
                 }
                 (false, None)
-            },
-            FwdBasinPhase { fwd, fwd_basin} => {
+            }
+            FwdBasin { fwd, fwd_basin } => {
                 /*if fwd_basin.step().await {
                     let fwd_basin = fwd_basin.finish();
                     let to_remove = fwd_basin.minus(&fwd);
@@ -94,28 +97,31 @@ impl ItgrProcess {
                 } else {
                     (false, None)
                 }*/
-                while !fwd_basin.step().await { }
+                while !fwd_basin.step().await {}
                 let fwd_basin = fwd_basin.finish();
-                let to_remove = fwd_basin.minus(&fwd);
+                let to_remove = fwd_basin.minus(fwd);
                 let pivots = self.root_stg.var_can_post(self.variable, fwd);
-                self.state = CmpPhase {
+                self.state = Cmp {
                     fwd: fwd.clone(),
-                    cmp: BwdProcess::new(self.root_stg.restrict(&fwd), pivots),
+                    cmp: BwdProcess::new(self.root_stg.restrict(fwd), pivots),
                 };
                 (false, Some(to_remove))
-            },
-            CmpPhase { fwd, cmp } => {
+            }
+            Cmp { fwd, cmp } => {
                 if cmp.step().await {
                     let cmp = cmp.finish();
                     let trap = fwd.minus(&cmp);
-                    self.state = TrapPhase {
+                    self.state = Trap {
                         trap_basin: BwdProcess::new(self.root_stg.clone(), trap.clone()),
-                        cmp, trap,
+                        cmp,
+                        trap,
                     }
                 }
                 (false, None)
             }
-            TrapPhase { trap, trap_basin, .. } => {
+            Trap {
+                trap, trap_basin, ..
+            } => {
                 /*if trap_basin.step().await {
                     let trap_basin = trap_basin.finish();
                     let to_remove = trap_basin.minus(trap);
@@ -123,7 +129,7 @@ impl ItgrProcess {
                 } else {
                     (false, None)
                 }*/
-                while !trap_basin.step().await { }
+                while !trap_basin.step().await {}
                 let trap_basin = trap_basin.finish();
                 let to_remove = trap_basin.minus(trap);
                 (true, Some(to_remove))
@@ -133,11 +139,10 @@ impl ItgrProcess {
 
     pub fn weight(&self) -> usize {
         match &self.state {
-            FwdPhase { fwd } => fwd.weight(),
-            FwdBasinPhase { fwd_basin, .. } => fwd_basin.weight(),
-            CmpPhase { cmp, .. } => cmp.weight(),
-            TrapPhase { trap_basin, .. } => trap_basin.weight(),
+            Fwd { fwd } => fwd.weight(),
+            FwdBasin { fwd_basin, .. } => fwd_basin.weight(),
+            Cmp { cmp, .. } => cmp.weight(),
+            Trap { trap_basin, .. } => trap_basin.weight(),
         }
     }
-
-}
\ No newline at end of file
+}
diff --git a/src/algorithms/attractors/itgr/mod.rs b/src/algorithms/attractors/itgr/mod.rs
index 761616a..7e52a2c 100644
--- a/src/algorithms/attractors/itgr/mod.rs
+++ b/src/algorithms/attractors/itgr/mod.rs
@@ -1,18 +1,19 @@
-use std::time::{Duration, SystemTime};
+use crate::algorithms::attractors::itgr::itgr_process::ItgrProcess;
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use futures::stream::FuturesUnordered;
 use futures::StreamExt;
-use crate::algorithms::attractors::itgr::itgr_process::ItgrProcess;
+use std::time::{Duration, SystemTime};
 
-mod reachability_process;
 mod itgr_process;
+mod reachability_process;
 
 pub async fn schedule_reductions(
     stg: SymbolicAsyncGraph,
     fork_limit: usize,
 ) -> GraphColoredVertices {
-    let mut processes = stg.as_network().variables()
+    let mut processes = stg
+        .variables()
         .map(|var| ItgrProcess::new(&stg, var))
         .collect::<Vec<_>>();
 
@@ -24,7 +25,7 @@ pub async fn schedule_reductions(
         // Put processes with the smallest weight at the end of the vector.
         processes.sort_by_cached_key(|p| -(p.weight() as isize));
 
-        while futures.len() < fork_limit && processes.len() > 0 {
+        while futures.len() < fork_limit && !processes.is_empty() {
             let mut process = processes.pop().unwrap();
 
             // Before queueing up the process, check if it has all the latest updates.
@@ -38,9 +39,12 @@ pub async fn schedule_reductions(
                 loop {
                     iter += 1;
                     let (done, to_remove) = process.step().await;
-                    if done || to_remove.is_some() || start.elapsed().unwrap() > Duration::from_secs(30) {
+                    if done
+                        || to_remove.is_some()
+                        || start.elapsed().unwrap() > Duration::from_secs(30)
+                    {
                         println!("Task completed {} iterations.", iter);
-                        return (done, to_remove, process)
+                        return (done, to_remove, process);
                     }
                 }
             }));
@@ -51,7 +55,7 @@ pub async fn schedule_reductions(
 
         if let Some(to_remove) = to_remove {
             universe.0 = universe.0.minus(&to_remove);
-            universe.1 = universe.1 + 1;
+            universe.1 += 1;
         }
 
         if !done {
@@ -61,7 +65,6 @@ pub async fn schedule_reductions(
         println!("Remaining: {} + {}", processes.len(), futures.len());
     }
 
-
     universe.0
     /*let mut futures = Vec::new();
 
@@ -101,4 +104,4 @@ pub async fn schedule_reductions(
     }
 
     universe.0*/
-}
\ No newline at end of file
+}
diff --git a/src/algorithms/attractors/itgr/reachability_process.rs b/src/algorithms/attractors/itgr/reachability_process.rs
index 8273622..a30a342 100644
--- a/src/algorithms/attractors/itgr/reachability_process.rs
+++ b/src/algorithms/attractors/itgr/reachability_process.rs
@@ -1,8 +1,8 @@
+use crate::algorithms::non_constant_variables;
+use crate::algorithms::reachability::{bwd_step, fwd_step};
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
-use crate::algorithms::non_constant_variables;
-use crate::algorithms::reachability::{bwd_step, fwd_step};
 
 /// A simplified "process" object that computes the forward reachable states from an initial set.
 pub struct FwdProcess {
@@ -19,12 +19,11 @@ pub struct BwdProcess {
 }
 
 impl FwdProcess {
-
     pub fn new(stg: SymbolicAsyncGraph, set: GraphColoredVertices) -> FwdProcess {
         FwdProcess {
             variables: non_constant_variables(&stg),
             stg,
-            set
+            set,
         }
     }
 
@@ -50,16 +49,14 @@ impl FwdProcess {
     pub fn weight(&self) -> usize {
         self.set.symbolic_size()
     }
-
 }
 
 impl BwdProcess {
-
     pub fn new(stg: SymbolicAsyncGraph, set: GraphColoredVertices) -> BwdProcess {
         BwdProcess {
             variables: non_constant_variables(&stg),
             stg,
-            set
+            set,
         }
     }
 
@@ -85,5 +82,4 @@ impl BwdProcess {
     pub fn weight(&self) -> usize {
         self.set.symbolic_size()
     }
-
 }
diff --git a/src/algorithms/attractors/mod.rs b/src/algorithms/attractors/mod.rs
index aba01f7..4f35e3f 100644
--- a/src/algorithms/attractors/mod.rs
+++ b/src/algorithms/attractors/mod.rs
@@ -1,7 +1,7 @@
-use biodivine_lib_param_bn::biodivine_std::traits::Set;
-use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use crate::algorithms::non_constant_variables;
 use crate::algorithms::reachability::{bwd, fwd_step};
+use biodivine_lib_param_bn::biodivine_std::traits::Set;
+use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 
 /// **(internal)** Implements interleaved transition guided reduction. This procedure attempts
 /// to eliminate a large portion of non-attractor states quickly. The module itself is private,
@@ -17,7 +17,7 @@ mod itgr;
 
 pub async fn transition_guided_reduction(
     stg: &SymbolicAsyncGraph,
-    fork_limit: usize
+    fork_limit: usize,
 ) -> GraphColoredVertices {
     itgr::schedule_reductions(stg.clone(), fork_limit).await
 }
@@ -25,14 +25,14 @@ pub async fn transition_guided_reduction(
 /// Forward-backward symbolic SCC detection algorithm modified to detect attractors (bottom SCCs).
 ///
 /// The algorithm can be parametrised by two callbacks:
-///  - First is called when an attractors is found. The argument represents the attractor set.
+///  - First is called when an attractor is found. The argument represents the attractor set.
 ///  - Second callback is called when a set of states is eliminated. This set may or may not
 ///    contain an attractor (however, if it does, the attractor is already reported).
 pub async fn attractors<OnAttractor, OnEliminated>(
     stg: &SymbolicAsyncGraph,
     set: &GraphColoredVertices,
     on_attractor: OnAttractor,
-    on_eliminated: OnEliminated
+    on_eliminated: OnEliminated,
 ) where
     OnAttractor: Fn(GraphColoredVertices) + Send + Sync,
     OnEliminated: Fn(GraphColoredVertices) + Send + Sync,
@@ -51,7 +51,9 @@ pub async fn attractors<OnAttractor, OnEliminated>(
 
         // Compute the rest of the pivot's SCC, stopping if it is not terminal.
         let mut pivot_component = pivot.clone();
-        while let Some(successors) = fwd_step(&active_stg, &pivot_component, &active_variables).await {
+        while let Some(successors) =
+            fwd_step(&active_stg, &pivot_component, &active_variables).await
+        {
             let non_terminal = successors.minus(&pivot_basin);
             if !non_terminal.is_empty() {
                 pivot_component = pivot_component.minus_colors(&non_terminal.colors());
diff --git a/src/algorithms/incremental_classifier.rs b/src/algorithms/incremental_classifier.rs
index 83397e1..aa3e3ce 100644
--- a/src/algorithms/incremental_classifier.rs
+++ b/src/algorithms/incremental_classifier.rs
@@ -28,6 +28,10 @@ impl<F: Feature, S: Set> IncrementalClassifier<F, S> {
         self.items.len()
     }
 
+    pub fn is_empty(&self) -> bool {
+        self.items.is_empty()
+    }
+
     /// Get the underlying list of features tracked by  this `IncrementalClassifier`.
     ///
     /// Note that the features may be ordered arbitrarily.
@@ -61,7 +65,7 @@ impl<F: Feature, S: Set> IncrementalClassifier<F, S> {
         for (f, s) in self.items.iter() {
             add(&mut new_items, (f.clone(), s.minus(&remaining)));
             add(&mut new_items, (f.extend(feature), s.intersect(&remaining)));
-            remaining = remaining.minus(&s);
+            remaining = remaining.minus(s);
         }
 
         assert!(remaining.is_empty());
diff --git a/src/algorithms/mod.rs b/src/algorithms/mod.rs
index bc9a843..3f35b84 100644
--- a/src/algorithms/mod.rs
+++ b/src/algorithms/mod.rs
@@ -9,7 +9,7 @@ pub mod asymptotic_behaviour;
 
 /// Reachability provides the main building blocks for more complex graph algorithms. The methods
 /// here are specifically designed to fit well into other processes in AEON. For basic tasks,
-/// you may be better of with some of the simpler algorithms provided by `SymbolicAsyncGraph`
+/// you may be better off with some of the simpler algorithms provided by `SymbolicAsyncGraph`
 /// directly.
 pub mod reachability;
 
@@ -34,18 +34,19 @@ mod asymptotic_behaviour_classifier;
 
 // Re-export stuff from private modules to public scope as part of `algorithms` module:
 
+pub use asymptotic_behaviour_classifier::AsymptoticBehaviourClassifier;
+pub use asymptotic_behaviour_counter::AsymptoticBehaviourCounter;
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
 use biodivine_lib_param_bn::VariableId;
-pub use asymptotic_behaviour_classifier::AsymptoticBehaviourClassifier;
-pub use asymptotic_behaviour_counter::AsymptoticBehaviourCounter;
 pub use symbolic_counter::SymbolicCounter;
 
 /// Identify the `VariableId` objects for which the given `stg` can perform *some* transition.
 pub fn non_constant_variables(stg: &SymbolicAsyncGraph) -> Vec<VariableId> {
-    stg.as_network().variables()
+    stg.variables()
         .filter(|var| {
-            !stg.var_can_post(*var, stg.unit_colored_vertices()).is_empty()
+            !stg.var_can_post(*var, stg.unit_colored_vertices())
+                .is_empty()
         })
         .collect()
-}
\ No newline at end of file
+}
diff --git a/src/algorithms/reachability.rs b/src/algorithms/reachability.rs
index 26e680f..5bad9a3 100644
--- a/src/algorithms/reachability.rs
+++ b/src/algorithms/reachability.rs
@@ -2,7 +2,6 @@ use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
 
-
 /// Try to compute direct successors of the provided `set` with respect to the given `stg`.
 /// The successors are also limited to the given selection of `variables`.
 ///
@@ -66,11 +65,11 @@ pub async fn fwd(
 pub async fn bwd(
     stg: &SymbolicAsyncGraph,
     set: &GraphColoredVertices,
-    variables: &[VariableId]
+    variables: &[VariableId],
 ) -> GraphColoredVertices {
     let mut result = set.clone();
     while let Some(predecessors) = bwd_step(stg, &result, variables).await {
         result = result.union(&predecessors);
     }
     result
-}
\ No newline at end of file
+}
diff --git a/src/algorithms/symbolic_counter.rs b/src/algorithms/symbolic_counter.rs
index 025fff6..6d5c5b2 100644
--- a/src/algorithms/symbolic_counter.rs
+++ b/src/algorithms/symbolic_counter.rs
@@ -3,7 +3,7 @@ use crate::util::functional::Functional;
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 
 /// Basic `SymbolicCounter` object that uses `IncrementalClassifier` to count how many times
-/// a a particular set member has been observed.
+/// a particular set member has been observed.
 #[derive(Clone)]
 pub struct SymbolicCounter<S: Set> {
     counter: IncrementalClassifier<Count, S>,
diff --git a/src/bdt/_attributes_for_network.rs b/src/bdt/_attributes_for_network.rs
index fecb1a9..023843f 100644
--- a/src/bdt/_attributes_for_network.rs
+++ b/src/bdt/_attributes_for_network.rs
@@ -3,17 +3,21 @@ use crate::util::functional::Functional;
 use biodivine_lib_bdd::Bdd;
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
-use biodivine_lib_param_bn::{FnUpdate, VariableId};
+use biodivine_lib_param_bn::{BooleanNetwork, FnUpdate, VariableId};
 
 impl Bdt {
-    pub fn new_from_graph(classes: BifurcationFunction, graph: &SymbolicAsyncGraph) -> Bdt {
+    pub fn new_from_graph(
+        classes: BifurcationFunction,
+        graph: &SymbolicAsyncGraph,
+        network: &BooleanNetwork,
+    ) -> Bdt {
         let mut attributes = Vec::new();
-        attributes_for_network_inputs(graph, &mut attributes);
-        attributes_for_constant_parameters(graph, &mut attributes);
-        attributes_for_missing_constraints(graph, &mut attributes);
-        attributes_for_implicit_function_tables(graph, &mut attributes);
-        attributes_for_explicit_function_tables(graph, &mut attributes);
-        attributes_for_conditional_observability(graph, &mut attributes);
+        attributes_for_network_inputs(network, graph, &mut attributes);
+        attributes_for_constant_parameters(network, graph, &mut attributes);
+        attributes_for_missing_constraints(network, graph, &mut attributes);
+        attributes_for_implicit_function_tables(network, graph, &mut attributes);
+        attributes_for_explicit_function_tables(network, graph, &mut attributes);
+        attributes_for_conditional_observability(network, graph, &mut attributes);
         let attributes = attributes
             .into_iter()
             .filter(|a| {
@@ -30,17 +34,21 @@ impl Bdt {
 }
 
 /// **(internal)** Construct basic attributes for all input variables.
-fn attributes_for_network_inputs(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for v in graph.as_network().variables() {
+fn attributes_for_network_inputs(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
+    for v in network.variables() {
         // v is input if it has no update function and no regulators
-        let is_input = graph.as_network().regulators(v).is_empty();
-        let is_input = is_input && graph.as_network().get_update_function(v).is_none();
+        let is_input = network.regulators(v).is_empty();
+        let is_input = is_input && network.get_update_function(v).is_none();
         if is_input {
             let bdd = graph
                 .symbolic_context()
                 .mk_implicit_function_is_true(v, &[]);
             out.push(Attribute {
-                name: graph.as_network().get_variable_name(v).clone(),
+                name: network.get_variable_name(v).clone(),
                 negative: graph.empty_colors().copy(bdd.not()),
                 positive: graph.empty_colors().copy(bdd),
                 context: None,
@@ -50,15 +58,19 @@ fn attributes_for_network_inputs(graph: &SymbolicAsyncGraph, out: &mut Vec<Attri
 }
 
 /// **(internal)** Construct basic attributes for all constant parameters of the network.
-fn attributes_for_constant_parameters(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for p in graph.as_network().parameters() {
-        if graph.as_network()[p].get_arity() == 0 {
+fn attributes_for_constant_parameters(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
+    for p in network.parameters() {
+        if network[p].get_arity() == 0 {
             // Parameter is a constant
             let bdd = graph
                 .symbolic_context()
                 .mk_uninterpreted_function_is_true(p, &[]);
             out.push(Attribute {
-                name: graph.as_network()[p].get_name().clone(),
+                name: network[p].get_name().clone(),
                 negative: graph.empty_colors().copy(bdd.not()),
                 positive: graph.empty_colors().copy(bdd),
                 context: None,
@@ -69,10 +81,13 @@ fn attributes_for_constant_parameters(graph: &SymbolicAsyncGraph, out: &mut Vec<
 
 /// **(internal)** If some regulation has a missing static constraint, try to build it
 /// and add it as an attribute.
-fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    let network = graph.as_network();
+fn attributes_for_missing_constraints(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
     let context = graph.symbolic_context();
-    for reg in graph.as_network().as_graph().regulations() {
+    for reg in network.as_graph().regulations() {
         // This is straight up copied from static constraint analysis in lib-param-bn.
         // For more context, go there.
         let target = reg.get_target();
@@ -89,11 +104,11 @@ fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<
         let regulator_is_false = context.mk_state_variable_is_true(reg.get_regulator()).not();
 
         if !reg.is_observable() {
-            let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_project(regulator);
-            let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_project(regulator);
+            let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_exists(regulator);
+            let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_exists(regulator);
             let observability = fn_x1_to_1
                 .xor(&fn_x0_to_1)
-                .project(context.state_variables());
+                .exists(context.state_variables());
 
             out.push(Attribute {
                 name: format!(
@@ -112,17 +127,17 @@ fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<
         }
 
         if reg.get_monotonicity().is_none() {
-            let fn_x1_to_0 = fn_is_false.and(&regulator_is_true).var_project(regulator);
-            let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_project(regulator);
+            let fn_x1_to_0 = fn_is_false.and(&regulator_is_true).var_exists(regulator);
+            let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_exists(regulator);
             let non_activation = fn_x0_to_1
                 .and(&fn_x1_to_0)
-                .project(context.state_variables());
+                .exists(context.state_variables());
 
-            let fn_x0_to_0 = fn_is_false.and(&regulator_is_false).var_project(regulator);
-            let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_project(regulator);
+            let fn_x0_to_0 = fn_is_false.and(&regulator_is_false).var_exists(regulator);
+            let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_exists(regulator);
             let non_inhibition = fn_x0_to_0
                 .and(&fn_x1_to_1)
-                .project(context.state_variables());
+                .exists(context.state_variables());
 
             out.push(Attribute {
                 name: format!(
@@ -159,27 +174,33 @@ fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<
 
 /// **(internal)** Make an explicit attributes (like `f[1,0,1] = 1`) for every implicit update
 /// function row in the network.
-fn attributes_for_implicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for v in graph.as_network().variables() {
-        let is_implicit_function = graph.as_network().get_update_function(v).is_none();
-        let is_implicit_function =
-            is_implicit_function && !graph.as_network().regulators(v).is_empty();
+fn attributes_for_implicit_function_tables(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
+    for v in network.variables() {
+        let is_implicit_function = network.get_update_function(v).is_none();
+        let is_implicit_function = is_implicit_function && !network.regulators(v).is_empty();
         if is_implicit_function {
-            let table = graph.symbolic_context().get_implicit_function_table(v);
+            let table = graph
+                .symbolic_context()
+                .get_implicit_function_table(v)
+                .unwrap();
             for (ctx, var) in table {
                 let bdd = graph.symbolic_context().bdd_variable_set().mk_var(var);
                 let ctx: Vec<String> = ctx
                     .into_iter()
-                    .zip(graph.as_network().regulators(v))
+                    .zip(network.regulators(v))
                     .map(|(b, r)| {
                         format!(
                             "{}{}",
                             if b { "" } else { "¬" },
-                            graph.as_network().get_variable_name(r)
+                            network.get_variable_name(r)
                         )
                     })
                     .collect();
-                let name = format!("{}{:?}", graph.as_network().get_variable_name(v), ctx);
+                let name = format!("{}{:?}", network.get_variable_name(v), ctx);
                 out.push(Attribute {
                     name: name.replace("\"", ""),
                     negative: graph.mk_empty_colors().copy(bdd.not()),
@@ -192,9 +213,13 @@ fn attributes_for_implicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut
 }
 
 /// **(internal)** Make an explicit argument for every explicit parameter function row in the network.
-fn attributes_for_explicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for p in graph.as_network().parameters() {
-        let parameter = graph.as_network().get_parameter(p);
+fn attributes_for_explicit_function_tables(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
+    for p in network.parameters() {
+        let parameter = network.get_parameter(p);
         if parameter.get_arity() > 0 {
             let table = graph.symbolic_context().get_explicit_function_table(p);
             let arg_names = (0..parameter.get_arity())
@@ -220,11 +245,14 @@ fn attributes_for_explicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut
 }
 
 /// Create "conditional observability" attributes for both implicit and explicit update functions.
-fn attributes_for_conditional_observability(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
+fn attributes_for_conditional_observability(
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+    out: &mut Vec<Attribute>,
+) {
     let context = graph.symbolic_context();
-    let network = graph.as_network();
-    for v in graph.as_network().variables() {
-        let regulators = graph.as_network().regulators(v);
+    for v in network.variables() {
+        let regulators = network.regulators(v);
 
         // Bdd that is true when update function for this variable is true
         let fn_is_true = if let Some(function) = network.get_update_function(v) {
@@ -268,11 +296,11 @@ fn attributes_for_conditional_observability(graph: &SymbolicAsyncGraph, out: &mu
                 for (condition_name, condition_list, condition_bdd) in contexts {
                     // Restrict to values that satisfy conditions
                     let fn_is_true = fn_is_true.and(&condition_bdd);
-                    let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_project(r_var);
-                    let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_project(r_var);
+                    let fn_x1_to_1 = fn_is_true.and(&regulator_is_true).var_exists(r_var);
+                    let fn_x0_to_1 = fn_is_true.and(&regulator_is_false).var_exists(r_var);
                     let observability = fn_x1_to_1
                         .xor(&fn_x0_to_1)
-                        .project(context.state_variables());
+                        .exists(context.state_variables());
 
                     out.push(Attribute {
                         name: format!(
@@ -301,7 +329,17 @@ fn variable_contexts(function: &FnUpdate) -> Vec<Vec<VariableId>> {
     match function {
         FnUpdate::Const(_) => vec![],
         FnUpdate::Var(_) => vec![],
-        FnUpdate::Param(_, args) => vec![args.clone()],
+        FnUpdate::Param(_, args) => {
+            let mut arg_ids = Vec::new();
+            for arg in args {
+                if let FnUpdate::Var(id) = arg {
+                    arg_ids.push(*id);
+                } else {
+                    panic!("Arguments must be variables, not complex expressions.")
+                }
+            }
+            vec![arg_ids]
+        }
         FnUpdate::Not(inner) => variable_contexts(inner),
         FnUpdate::Binary(_, l, r) => variable_contexts(l)
             .apply(|list| variable_contexts(r).into_iter().for_each(|c| list.push(c))),
@@ -316,7 +354,7 @@ fn variable_contexts(function: &FnUpdate) -> Vec<Vec<VariableId>> {
 /// XYZ
 ///
 /// This should also automatically filter out empty results, so you can
-/// include A and !A in the conditions without problems.
+/// include `A` and `!A` in the conditions without problems.
 fn make_contexts(conditions: &[(String, Bdd)]) -> Vec<(String, Vec<String>, Bdd)> {
     fn recursion(
         conditions: &[(String, Bdd)],
diff --git a/src/bdt/_impl_indexing.rs b/src/bdt/_impl_indexing.rs
index 9d073b9..b9fde80 100644
--- a/src/bdt/_impl_indexing.rs
+++ b/src/bdt/_impl_indexing.rs
@@ -11,6 +11,11 @@ impl BdtNodeId {
     pub fn try_from(index: usize, collection: &Bdt) -> Option<Self> {
         BdtNodeId(index).take_if(|i| collection.storage.contains_key(&i.0))
     }
+
+    pub fn try_from_str(string: &str, collection: &Bdt) -> Option<Self> {
+        let index = string.parse::<usize>().ok()?;
+        Self::try_from(index, collection)
+    }
 }
 
 impl AttributeId {
@@ -21,6 +26,11 @@ impl AttributeId {
     pub fn try_from(index: usize, collection: &Bdt) -> Option<Self> {
         AttributeId(index).take_if(|i| i.0 < collection.attributes.len())
     }
+
+    pub fn try_from_str(string: &str, collection: &Bdt) -> Option<Self> {
+        let index = string.parse::<usize>().ok()?;
+        AttributeId::try_from(index, collection)
+    }
 }
 
 impl Index<BdtNodeId> for Bdt {
diff --git a/src/bdt/mod.rs b/src/bdt/mod.rs
index 561f395..632922a 100644
--- a/src/bdt/mod.rs
+++ b/src/bdt/mod.rs
@@ -25,7 +25,7 @@ mod _impl_indexing;
 type BifurcationFunction = HashMap<Class, GraphColors>;
 
 /// Encodes one node of a bifurcation decision tree. A node can be either a leaf (fully classified
-/// set of parametrisations), a decision node with a fixed attribute, or an unprocessed node
+/// parametrization set), a decision node with a fixed attribute, or an unprocessed node
 /// with a remaining bifurcation function.
 #[derive(Clone)]
 pub enum BdtNode {
@@ -71,7 +71,7 @@ pub struct Bdt {
     storage: HashMap<usize, BdtNode>,
     attributes: Vec<Attribute>,
     next_id: usize,
-    // Represents a hundreds of a percent threshold (So 9350 means 95.30%) at which a mixed node
+    // Represents a hundred of a percent threshold (So 9350 means 95.30%) at which a mixed node
     // is assumed to be a leaf, or `None` is the tree is exact. We assume that this number is
     // always >50% to make sure the decision is unique.
     precision: Option<u32>,
diff --git a/src/bin/experiment.rs b/src/bin/experiment.rs
index 5f55417..a884ebe 100644
--- a/src/bin/experiment.rs
+++ b/src/bin/experiment.rs
@@ -25,11 +25,11 @@ fn main() {
     println!("Model loaded...");
     println!("{} variables: {:?}", model.num_vars(), names);
 
-    let graph = SymbolicAsyncGraph::new(model).unwrap();
+    let graph = SymbolicAsyncGraph::new(&model).unwrap();
 
     println!("Asynchronous graph ready...");
     println!(
-        "Admissible parametrisations: {}",
+        "Admissible parametrization set: {}",
         graph.unit_colors().approx_cardinality()
     );
     println!(
diff --git a/src/bin/experiment_new.rs b/src/bin/experiment_new.rs
index 781810d..81bfb10 100644
--- a/src/bin/experiment_new.rs
+++ b/src/bin/experiment_new.rs
@@ -1,13 +1,8 @@
-use biodivine_aeon_server::scc::algo_interleaved_transition_guided_reduction::interleaved_transition_guided_reduction;
-use biodivine_aeon_server::scc::algo_xie_beerel::xie_beerel_attractors;
-use biodivine_aeon_server::scc::Classifier;
-use biodivine_aeon_server::GraphTaskContext;
+use biodivine_aeon_server::algorithms::attractors::transition_guided_reduction;
 use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
 use biodivine_lib_param_bn::BooleanNetwork;
 use std::convert::TryFrom;
 use std::io::Read;
-use std::time::{SystemTime, UNIX_EPOCH};
-use biodivine_aeon_server::algorithms::attractors::transition_guided_reduction;
 
 #[tokio::main]
 async fn main() {
@@ -22,11 +17,11 @@ async fn main() {
     println!("Model loaded...");
     println!("{} variables: {:?}", model.num_vars(), names);
 
-    let graph = SymbolicAsyncGraph::new(model).unwrap();
+    let graph = SymbolicAsyncGraph::new(&model).unwrap();
 
     println!("Asynchronous graph ready...");
     println!(
-        "Admissible parametrisations: {}",
+        "Admissible parametrization set: {}",
         graph.unit_colors().approx_cardinality()
     );
     println!(
diff --git a/src/bin/sink_state_enumerator.rs b/src/bin/sink_state_enumerator.rs
index 0633f64..149eb71 100644
--- a/src/bin/sink_state_enumerator.rs
+++ b/src/bin/sink_state_enumerator.rs
@@ -24,11 +24,11 @@ fn main() {
     println!("Model loaded...");
     println!("{} variables: {:?}", model.num_vars(), names);
 
-    let graph = SymbolicAsyncGraph::new(model.clone()).unwrap();
+    let graph = SymbolicAsyncGraph::new(&model).unwrap();
 
     println!("Asynchronous graph ready...");
     println!(
-        "Admissible parametrisations: {}",
+        "Admissible parametrization set: {}",
         graph.unit_colors().approx_cardinality()
     );
     println!(
@@ -75,7 +75,7 @@ fn main() {
     );
     println!("Elapsed time: {}s", start.elapsed().unwrap().as_secs());
 
-    let mut all_sinks = graph.mk_empty_vertices();
+    let mut all_sinks = graph.mk_empty_colored_vertices();
     for (attractor, behaviours) in classifier.export_components() {
         if let Some(sink_colors) = behaviours.get(&Behaviour::Stability) {
             all_sinks = all_sinks.union(&attractor.intersect_colors(sink_colors));
diff --git a/src/main.rs b/src/main.rs
index 0d3b5be..17ac201 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,11 +1,9 @@
-#![feature(proc_macro_hygiene, decl_macro)]
 #[macro_use]
 extern crate rocket;
 
 #[macro_use]
 extern crate json;
 
-use rocket::http::hyper::header::AccessControlAllowOrigin;
 use rocket::http::{ContentType, Header};
 use rocket::request::Request;
 use rocket::response::{self, Responder, Response};
@@ -22,20 +20,23 @@ use biodivine_aeon_server::scc::algo_stability_analysis::{
 };
 use biodivine_aeon_server::scc::algo_xie_beerel::xie_beerel_attractors;
 use biodivine_aeon_server::util::functional::Functional;
-use biodivine_aeon_server::util::index_type::IndexType;
 use biodivine_aeon_server::GraphTaskContext;
 use biodivine_lib_param_bn::biodivine_std::bitvector::{ArrayBitVector, BitVector};
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph};
 use json::JsonValue;
-use rocket::config::Environment;
+use lazy_static::lazy_static;
+use rocket::data::ByteUnit;
 use rocket::{Config, Data};
+use rocket_cors::{AllowedOrigins, CorsOptions};
 use std::cmp::max;
 use std::collections::{HashMap, HashSet};
-use std::io::Read;
+use std::net::IpAddr;
+use std::str::FromStr;
 use std::sync::{Arc, RwLock};
 use std::thread::JoinHandle;
 use std::time::{Duration, SystemTime, UNIX_EPOCH};
+use tokio::io::AsyncReadExt;
 
 /// Computation keeps all information
 struct Computation {
@@ -81,7 +82,7 @@ lazy_static! {
 ///    node. (This can take a while for large models) Returns an array of attribute objects.
 ///    - /apply_attribute/<node_id>/<attribute_id>: Apply an attribute to an unprocessed node,
 ///    replacing it with a decision and adding two new child nodes. Returns an array of tree nodes
-///    that have changed (i.e. the unprocessed node is now a decision node and it has two children
+///    that have changed (i.e. the unprocessed node is now a decision node, and it has two children
 ///    now)
 ///    - /revert_decision/<node_id>: Turn a decision node back into unprocessed node. This is done
 ///    recursively, so any children are deleted as well. Returns a
@@ -187,10 +188,10 @@ fn get_stability_data(node_id: String, behaviour_str: String) -> BackendResponse
 
             let stability_data = compute_stability(graph, &components);
             let mut response = JsonValue::new_array();
-            for variable in graph.as_network().variables() {
+            for variable in graph.variables() {
                 response
                     .push(object! {
-                        "variable": graph.as_network().get_variable_name(variable).clone(),
+                        "variable": graph.get_variable_name(variable).clone(),
                         "data": stability_data[&variable].to_json(),
                     })
                     .unwrap();
@@ -208,7 +209,7 @@ fn get_stability_data(node_id: String, behaviour_str: String) -> BackendResponse
 fn apply_attribute(node_id: String, attribute_id: String) -> BackendResponse {
     let tree = TREE.clone();
     let mut tree = tree.write().unwrap();
-    return if let Some(tree) = tree.as_mut() {
+    if let Some(tree) = tree.as_mut() {
         let node = BdtNodeId::try_from_str(&node_id, tree);
         let node = if let Some(node) = node {
             node
@@ -233,7 +234,7 @@ fn apply_attribute(node_id: String, attribute_id: String) -> BackendResponse {
         }
     } else {
         BackendResponse::err("No tree present. Run computation first.")
-    };
+    }
 }
 
 #[post("/revert_decision/<node_id>")]
@@ -333,10 +334,10 @@ fn max_parameter_cardinality(function: &FnUpdate) -> usize {
 /// Return cardinality of such model (i.e. the number of instantiations of this update function)
 /// or error if the update function (or model) is invalid.
 #[post("/check_update_function", format = "plain", data = "<data>")]
-fn check_update_function(data: Data) -> BackendResponse {
-    let mut stream = data.open().take(10_000_000); // limit model size to 10MB
+async fn check_update_function(data: Data<'_>) -> BackendResponse {
+    let mut stream = data.open(ByteUnit::Megabyte(10)); // limit model size to 10MB
     let mut model_string = String::new();
-    return match stream.read_to_string(&mut model_string) {
+    match stream.read_to_string(&mut model_string).await {
         Ok(_) => {
             let lock = CHECK_UPDATE_FUNCTION_LOCK.clone();
             let mut lock = lock.write().unwrap();
@@ -357,7 +358,7 @@ fn check_update_function(data: Data) -> BackendResponse {
                             model.num_vars(),
                             max_size
                         );
-                        SymbolicAsyncGraph::new(model)
+                        SymbolicAsyncGraph::new(&model)
                     } else {
                         Err("Function too large for on-the-fly analysis.".to_string())
                     }
@@ -368,7 +369,7 @@ fn check_update_function(data: Data) -> BackendResponse {
                 start.elapsed().unwrap().as_millis(),
                 graph
             );
-            (*lock) = !(*lock);
+            *lock = !(*lock);
             match graph {
                 Ok(cardinality) => {
                     BackendResponse::ok(&format!("{{\"cardinality\":\"{}\"}}", cardinality))
@@ -377,7 +378,7 @@ fn check_update_function(data: Data) -> BackendResponse {
             }
         }
         Err(error) => BackendResponse::err(&format!("{}", error)),
-    };
+    }
 }
 
 const VERSION: &str = env!("CARGO_PKG_VERSION");
@@ -466,7 +467,7 @@ fn get_results() -> BackendResponse {
                     )
                 } else {
                     return BackendResponse::err(
-                        &"Classification running. Cannot export components right now.".to_string(),
+                        "Classification running. Cannot export components right now.",
                     );
                 }
             } else {
@@ -489,7 +490,7 @@ fn get_results() -> BackendResponse {
 
     println!("Result {:?}", lines);
 
-    let elapsed = if let Some(e) = elapsed { e } else { 0 };
+    let elapsed = elapsed.unwrap_or_default();
 
     let mut json = String::new();
     for line in lines.iter().take(lines.len() - 1) {
@@ -587,9 +588,8 @@ fn get_stability_witness(
         };
         if let Some(graph) = &cmp.graph {
             let variable = graph
-                .as_network()
-                .as_graph()
-                .find_variable(variable_str.as_str());
+                .symbolic_context()
+                .find_network_variable(variable_str.as_str());
             let variable = if let Some(variable) = variable {
                 variable
             } else {
@@ -613,9 +613,9 @@ fn get_stability_witness(
             if let Some(colors) = &variable_stability[vector] {
                 get_witness_network(colors)
             } else {
-                return BackendResponse::err(
+                BackendResponse::err(
                     format!("No witness available for vector `{}`.", vector_str).as_str(),
-                );
+                )
             }
         } else {
             BackendResponse::err("No attractor data found.")
@@ -651,8 +651,7 @@ fn get_witness(class_str: String) -> BackendResponse {
                     }
                 } else {
                     BackendResponse::err(
-                        &"Classification in progress. Cannot extract witness right now."
-                            .to_string(),
+                        "Classification in progress. Cannot extract witness right now.",
                     )
                 }
             } else {
@@ -773,9 +772,8 @@ fn get_stability_attractors(
         };
         if let Some(graph) = &cmp.graph {
             let variable = graph
-                .as_network()
-                .as_graph()
-                .find_variable(variable_str.as_str());
+                .symbolic_context()
+                .find_network_variable(variable_str.as_str());
             let variable = if let Some(variable) = variable {
                 variable
             } else {
@@ -799,9 +797,9 @@ fn get_stability_attractors(
             if let Some(colors) = &variable_stability[vector] {
                 get_witness_attractors(colors)
             } else {
-                return BackendResponse::err(
+                BackendResponse::err(
                     format!("No witness available for vector `{}`.", vector_str).as_str(),
-                );
+                )
             }
         } else {
             BackendResponse::err("No attractor data found.")
@@ -839,8 +837,7 @@ fn get_attractors(class_str: String) -> BackendResponse {
                     }
                 } else {
                     BackendResponse::err(
-                        &"Classification still in progress. Cannot explore attractors now."
-                            .to_string(),
+                        "Classification still in progress. Cannot explore attractors now.",
                     )
                 }
             } else {
@@ -862,7 +859,7 @@ fn get_witness_attractors(f_colors: &GraphColors) -> BackendResponse {
                 if let Some(graph) = &cmp.graph {
                     let f_witness_colour = f_colors.pick_singleton();
                     let witness_network: BooleanNetwork = graph.pick_witness(&f_witness_colour);
-                    let witness_graph = SymbolicAsyncGraph::new(witness_network.clone()).unwrap();
+                    let witness_graph = SymbolicAsyncGraph::new(&witness_network).unwrap();
                     let witness_str = witness_network.to_string();
                     let f_witness_attractors = f_classifier.attractors(&f_witness_colour);
                     let variable_name_strings = witness_network
@@ -897,11 +894,9 @@ fn get_witness_attractors(f_colors: &GraphColors) -> BackendResponse {
                         } else if f_attractor.approx_cardinality() >= 500.0 {
                             has_large_attractors = true;
                             // For large attractors, only show fixed values.
-                            let mut state_0 =
-                                ArrayBitVector::from(vec![false; graph.as_network().num_vars()]);
-                            let mut state_1 =
-                                ArrayBitVector::from(vec![true; graph.as_network().num_vars()]);
-                            for var in graph.as_network().variables() {
+                            let mut state_0 = ArrayBitVector::from(vec![false; graph.num_vars()]);
+                            let mut state_1 = ArrayBitVector::from(vec![true; graph.num_vars()]);
+                            for var in graph.variables() {
                                 let f_var_true = graph.fix_network_variable(var, true).vertices();
                                 let f_var_false = graph.fix_network_variable(var, false).vertices();
                                 let f_always_one = f_attractor.intersect(&f_var_false).is_empty();
@@ -919,8 +914,8 @@ fn get_witness_attractors(f_colors: &GraphColors) -> BackendResponse {
                         } else {
                             for source in f_attractor.materialize().iter() {
                                 let source_set = witness_graph.vertex(&source);
-                                let mut target_set = witness_graph.mk_empty_vertices();
-                                for v in witness_graph.as_network().variables() {
+                                let mut target_set = witness_graph.mk_empty_colored_vertices();
+                                for v in witness_graph.variables() {
                                     let post = witness_graph.var_post(v, &source_set);
                                     if !post.is_empty() {
                                         not_fixed_vars.insert(v.into());
@@ -998,10 +993,10 @@ fn get_witness_attractors(f_colors: &GraphColors) -> BackendResponse {
 
 /// Accept an Aeon model, parse it and start a new computation (if there is no computation running).
 #[post("/start_computation", format = "plain", data = "<data>")]
-fn start_computation(data: Data) -> BackendResponse {
-    let mut stream = data.open().take(10_000_000); // limit model to 10MB
+async fn start_computation(data: Data<'_>) -> BackendResponse {
+    let mut stream = data.open(ByteUnit::Megabyte(10)); // limit model to 10MB
     let mut aeon_string = String::new();
-    return match stream.read_to_string(&mut aeon_string) {
+    return match stream.read_to_string(&mut aeon_string).await {
         Ok(_) => {
             // First, try to parse the network so that the user can at least verify it is correct...
             match BooleanNetwork::try_from(aeon_string.as_str()) {
@@ -1041,7 +1036,7 @@ fn start_computation(data: Data) -> BackendResponse {
                         // stuff.
                         let cmp_thread = std::thread::spawn(move || {
                             let cmp: Arc<RwLock<Option<Computation>>> = COMPUTATION.clone();
-                            match SymbolicAsyncGraph::new(network) {
+                            match SymbolicAsyncGraph::new(&network) {
                                 Ok(graph) => {
                                     // Now that we have graph, we can create classifier and progress
                                     // and save them into the computation.
@@ -1104,7 +1099,7 @@ fn start_computation(data: Data) -> BackendResponse {
                                         let result = classifier.export_result();
                                         let tree = TREE.clone();
                                         let mut tree = tree.write().unwrap();
-                                        *tree = Some(Bdt::new_from_graph(result, &graph));
+                                        *tree = Some(Bdt::new_from_graph(result, &graph, &network));
                                         println!("Saved decision tree");
                                     }
 
@@ -1169,7 +1164,7 @@ fn cancel_computation() -> BackendResponse {
             return BackendResponse::err("Nothing to cancel. Computation already done.");
         }
         if cmp.task.cancel() {
-            BackendResponse::ok(&"\"ok\"".to_string())
+            BackendResponse::ok("\"ok\"")
         } else {
             BackendResponse::err("Computation already cancelled.")
         }
@@ -1182,10 +1177,10 @@ fn cancel_computation() -> BackendResponse {
 /// If everything goes well, return a standard result object with a parsed model, or
 /// error if something fails.
 #[post("/sbml_to_aeon", format = "plain", data = "<data>")]
-fn sbml_to_aeon(data: Data) -> BackendResponse {
-    let mut stream = data.open().take(10_000_000); // limit model to 10MB
+async fn sbml_to_aeon(data: Data<'_>) -> BackendResponse {
+    let mut stream = data.open(ByteUnit::Megabyte(10)); // limit model to 10MB
     let mut sbml_string = String::new();
-    match stream.read_to_string(&mut sbml_string) {
+    match stream.read_to_string(&mut sbml_string).await {
         Ok(_) => {
             match BooleanNetwork::try_from_sbml(&sbml_string) {
                 Ok((model, layout)) => {
@@ -1240,10 +1235,10 @@ fn read_metadata(aeon_string: &str) -> (Option<String>, Option<String>) {
 /// which will then be translated into SBML (XML) representation.
 /// Preserve layout metadata.
 #[post("/aeon_to_sbml", format = "plain", data = "<data>")]
-fn aeon_to_sbml(data: Data) -> BackendResponse {
-    let mut stream = data.open().take(10_000_000); // limit model to 10MB
+async fn aeon_to_sbml(data: Data<'_>) -> BackendResponse {
+    let mut stream = data.open(ByteUnit::Megabyte(10)); // limit model to 10MB
     let mut aeon_string = String::new();
-    match stream.read_to_string(&mut aeon_string) {
+    match stream.read_to_string(&mut aeon_string).await {
         Ok(_) => match BooleanNetwork::try_from(aeon_string.as_str()) {
             Ok(network) => {
                 let layout = read_layout(&aeon_string);
@@ -1260,12 +1255,14 @@ fn aeon_to_sbml(data: Data) -> BackendResponse {
 /// Note that this can take quite a while for large models since we have to actually build
 /// the unit BDD right now (in the future, we might opt to use a SAT solver which might be faster).
 #[post("/aeon_to_sbml_instantiated", format = "plain", data = "<data>")]
-fn aeon_to_sbml_instantiated(data: Data) -> BackendResponse {
-    let mut stream = data.open().take(10_000_000); // limit model to 10MB
+async fn aeon_to_sbml_instantiated(data: Data<'_>) -> BackendResponse {
+    let mut stream = data.open(ByteUnit::Megabyte(10)); // limit model to 10MB
     let mut aeon_string = String::new();
-    return match stream.read_to_string(&mut aeon_string) {
+    match stream.read_to_string(&mut aeon_string).await {
         Ok(_) => {
-            match BooleanNetwork::try_from(aeon_string.as_str()).and_then(SymbolicAsyncGraph::new) {
+            match BooleanNetwork::try_from(aeon_string.as_str())
+                .and_then(|it| SymbolicAsyncGraph::new(&it))
+            {
                 Ok(graph) => {
                     let witness = graph.pick_witness(graph.unit_colors());
                     let layout = read_layout(&aeon_string);
@@ -1277,12 +1274,20 @@ fn aeon_to_sbml_instantiated(data: Data) -> BackendResponse {
             }
         }
         Err(error) => BackendResponse::err(&format!("{}", error)),
-    };
+    }
 }
 
-fn main() {
+// An empty endpoint that will respond to all OPTIONS requests positively,
+// since we accept all requests.
+#[options("/<_path..>")]
+fn all_options(_path: std::path::PathBuf) -> &'static str {
+    "" // Respond to all OPTIONS requests with an empty 200 response
+}
+
+#[launch]
+fn rocket() -> _ {
     //test_main::run();
-    let address = std::env::var("AEON_ADDR").unwrap_or_else(|_| "localhost".to_string());
+    let address = std::env::var("AEON_ADDR").unwrap_or_else(|_| "127.0.0.1".to_string());
     let port_from_args = {
         let mut args = std::env::args();
         args.next(); // Skip binary path
@@ -1292,12 +1297,17 @@ fn main() {
         .ok()
         .and_then(|s| s.parse::<u16>().ok());
     let port: u16 = port_from_args.or(port_from_env).unwrap_or(8000);
-    let config = Config::build(Environment::Production)
-        .address(address)
-        .port(port)
-        .finalize();
 
-    rocket::custom(config.unwrap())
+    let config = Config {
+        address: IpAddr::from_str(address.as_str()).unwrap(),
+        port,
+        ..Default::default()
+    };
+
+    let cors = CorsOptions::default().allowed_origins(AllowedOrigins::all());
+
+    rocket::custom(config)
+        .attach(cors.to_cors().unwrap())
         .mount(
             "/",
             routes![
@@ -1323,9 +1333,9 @@ fn main() {
                 apply_tree_precision,
                 get_tree_precision,
                 auto_expand,
+                all_options,
             ],
         )
-        .launch();
 }
 
 struct BackendResponse {
@@ -1350,19 +1360,17 @@ impl BackendResponse {
     }
 }
 
-impl<'r> Responder<'r> for BackendResponse {
-    fn respond_to(self, _: &Request) -> response::Result<'r> {
+impl<'r, 's: 'r> Responder<'r, 's> for BackendResponse {
+    fn respond_to(self, _request: &'r Request<'_>) -> response::Result<'s> {
         use std::io::Cursor;
 
-        let cursor = Cursor::new(self.message);
         Response::build()
             .header(ContentType::Plain)
-            .header(AccessControlAllowOrigin::Any)
-            // This magic set of headers might fix some CROS issues, but we are not sure yet...
+            // This magic set of headers might fix some CORS issues, but we are not sure yet...
             .header(Header::new("Allow", "GET, POST, OPTIONS, PUT, DELETE"))
             .header(Header::new("Access-Control-Allow-Methods", "GET, POST, OPTIONS, PUT, DELETE"))
             .header(Header::new("Access-Control-Allow-Headers", "X-API-KEY, Origin, X-Requested-With, Content-Type, Accept, Access-Control-Request-Method"))
-            .sized_body(cursor)
+            .sized_body(self.message.len(), Cursor::new(self.message))
             .ok()
     }
 }
diff --git a/src/scc/_impl_classifier.rs b/src/scc/_impl_classifier.rs
index 9c1e1f4..f011bc5 100644
--- a/src/scc/_impl_classifier.rs
+++ b/src/scc/_impl_classifier.rs
@@ -128,9 +128,9 @@ impl Classifier {
         }
         if !not_sink_params.is_empty() {
             let mut disorder = graph.mk_empty_colors();
-            for variable in graph.as_network().variables() {
+            for variable in graph.variables() {
                 let found_first_successor = &graph.var_can_post(variable, &without_sinks);
-                for next_variable in graph.as_network().variables() {
+                for next_variable in graph.variables() {
                     if next_variable == variable {
                         continue;
                     }
@@ -200,8 +200,8 @@ impl Classifier {
         component: GraphColoredVertices,
         graph: &SymbolicAsyncGraph,
     ) -> GraphColoredVertices {
-        let mut is_not_sink = graph.empty_vertices().clone();
-        for variable in graph.as_network().variables() {
+        let mut is_not_sink = graph.empty_colored_vertices().clone();
+        for variable in graph.variables() {
             let has_successor = &graph.var_can_post(variable, &component);
             if !has_successor.is_empty() {
                 is_not_sink = is_not_sink.union(has_successor);
diff --git a/src/scc/algo_interleaved_transition_guided_reduction/mod.rs b/src/scc/algo_interleaved_transition_guided_reduction/mod.rs
index 25e6dac..20dcad5 100644
--- a/src/scc/algo_interleaved_transition_guided_reduction/mod.rs
+++ b/src/scc/algo_interleaved_transition_guided_reduction/mod.rs
@@ -27,16 +27,16 @@ pub fn interleaved_transition_guided_reduction(
     graph: &SymbolicAsyncGraph,
     initial: GraphColoredVertices,
 ) -> (GraphColoredVertices, Vec<VariableId>) {
-    let variables = graph.as_network().variables().collect::<Vec<_>>();
+    let variables = graph.variables().collect::<Vec<_>>();
     let mut scheduler = Scheduler::new(ctx, initial, variables);
-    for variable in graph.as_network().variables() {
+    for variable in graph.variables() {
         scheduler.spawn(ReachableProcess::new(
             variable,
             graph,
             scheduler.get_universe().clone(),
         ));
     }
-    let process_count = u32::try_from(graph.as_network().num_vars() * 2).unwrap();
+    let process_count = u32::try_from(graph.num_vars() * 2).unwrap();
     ctx.progress.set_process_count(process_count); // * 2 because each will spawn one extra.
 
     while !scheduler.is_done() {
diff --git a/src/scc/algo_stability_analysis/mod.rs b/src/scc/algo_stability_analysis/mod.rs
index 9140dcf..70f7c8b 100644
--- a/src/scc/algo_stability_analysis/mod.rs
+++ b/src/scc/algo_stability_analysis/mod.rs
@@ -58,7 +58,6 @@ pub fn compute_stability(
     components: &[GraphColoredVertices],
 ) -> StabilityData {
     graph
-        .as_network()
         .variables()
         .map(|id| (id, VariableStability::for_attractors(graph, components, id)))
         .collect()
diff --git a/src/scc/algo_xie_beerel/mod.rs b/src/scc/algo_xie_beerel/mod.rs
index 1b0ebe2..69da259 100644
--- a/src/scc/algo_xie_beerel/mod.rs
+++ b/src/scc/algo_xie_beerel/mod.rs
@@ -31,7 +31,7 @@ pub fn xie_beerel_attractors<F>(
         let mut pivot_component = pivots.clone();
 
         // Iteratively compute the pivot component. If some color leaves `pivot_basin`, it is
-        // removed from `pivot_component`, as it does not have to be processed any more.
+        // removed from `pivot_component`, as it does not have to be processed anymore.
         //
         // At the end of the loop, `pivot_component` contains only colors for which the component
         // is an attractor (other colors will leave the `pivot_basin` at some point).
diff --git a/src/util/functional.rs b/src/util/functional.rs
index 2f1a698..b7b96fb 100644
--- a/src/util/functional.rs
+++ b/src/util/functional.rs
@@ -3,7 +3,7 @@ pub trait Functional: Sized {
     ///
     /// It takes ownership of the given value and returns it back once the action
     /// has been applied. Note that it cannot change the output type (output of
-    /// `action` is ignored.
+    /// `action` is ignored).
     fn apply<F, R>(mut self, action: F) -> Self
     where
         F: FnOnce(&mut Self) -> R,
@@ -23,7 +23,7 @@ pub trait Functional: Sized {
         action(self)
     }
 
-    /// Run an non-modifying action with the given value. The return value
+    /// Run a non-modifying action with the given value. The return value
     /// is dropped.
     fn also<F, R>(self, action: F) -> Self
     where
@@ -36,7 +36,7 @@ pub trait Functional: Sized {
     /// Conditionally wrap item in `Some`.
     ///
     /// Note that this always evaluates the value in question and shouldn't be thus
-    /// used when side-effects are important or items are large.
+    /// used when side effects are important or items are large.
     fn take_if<F>(self, test: F) -> Option<Self>
     where
         F: FnOnce(&Self) -> bool,