Upgrade to latest lib-param-bn.

Cargo.toml

@@ -26,8 +26,8 @@ name = "convert-aeon-to-bnet"
 path = "src/bin/convert_aeon_to_bnet.rs"
 
 [dependencies]
-biodivine-lib-bdd = ">=0.5.2, <1.0.0"
-biodivine-lib-param-bn = ">=0.4.7, <1.0.0"
+biodivine-lib-bdd = ">=0.5.7, <1.0.0"
+biodivine-lib-param-bn = ">=0.5.0, <1.0.0"
 clap = { version = "4.1.4", features = ["derive"] }
 rand = "0.8.5"
 termcolor = "1.1.2"

src/aeon/itgr/mod.rs

@@ -24,9 +24,9 @@ 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(initial, variables);
-    for variable in graph.as_network().variables() {
+    for variable in graph.variables() {
         scheduler.spawn(ReachableProcess::new(
             variable,
             graph,

src/aeon/scc_computation.rs

@@ -19,7 +19,7 @@ pub fn compute_attractor_states(
         graph,
         &universe,
         &active_variables,
-        graph.mk_empty_vertices(),
+        graph.mk_empty_colored_vertices(),
     )
 }
 

src/analysis.rs

@@ -9,6 +9,7 @@ use crate::result_print::*;
 
 use biodivine_lib_param_bn::BooleanNetwork;
 
+use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext;
 use std::collections::HashMap;
 use std::time::SystemTime;
 
@@ -33,6 +34,7 @@ pub fn analyse_formulae(
     print_if_allowed(format!("Read {} HCTL formulae.", formulae.len()), print_op);
     print_if_allowed("-----".to_string(), print_op);
 
+    let plain_context = SymbolicContext::new(bn).unwrap();
     for (i, formula) in formulae.iter().enumerate() {
         print_if_allowed(format!("Original formula n.{}: {formula}", i + 1), print_op);
         let tree = parse_hctl_formula(formula.as_str())?;
@@ -41,7 +43,8 @@ pub fn analyse_formulae(
             print_op,
         );
 
-        let modified_tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?;
+        let modified_tree =
+            check_props_and_rename_vars(tree, HashMap::new(), String::new(), &plain_context)?;
         let num_hctl_vars = collect_unique_hctl_vars(modified_tree.clone()).len();
         print_if_allowed(
             format!("Modified version:     {}", modified_tree.subform_str),
@@ -60,7 +63,7 @@ pub fn analyse_formulae(
     print_if_allowed(
         format!(
             "Loaded BN model with {} components and {} parameters.",
-            graph.as_network().num_vars(),
+            graph.num_vars(),
             graph.symbolic_context().num_parameter_variables()
         ),
         print_op,

src/bin/convert_aeon_to_bnet.rs

@@ -31,7 +31,11 @@ fn flatten_update_function(network: &mut BooleanNetwork, variable: VariableId) {
         let function = function.clone(); // Clone necessary for borrow checking.
         flatten_fn_update(network, &function)
     } else {
-        let regulators = network.regulators(variable);
+        let regulators = network
+            .regulators(variable)
+            .into_iter()
+            .map(FnUpdate::mk_var)
+            .collect::<Vec<_>>();
         let name = format!("{}_", network.get_variable_name(variable));
         explode_function(network, &regulators, name)
     };
@@ -59,7 +63,7 @@ fn flatten_fn_update(network: &mut BooleanNetwork, update: &FnUpdate) -> FnUpdat
 
 fn explode_function(
     network: &mut BooleanNetwork,
-    regulators: &[VariableId],
+    regulators: &[FnUpdate],
     name_prefix: String,
 ) -> FnUpdate {
     if regulators.is_empty() {
@@ -68,12 +72,12 @@ fn explode_function(
             parameter.unwrap_or_else(|| network.add_parameter(name_prefix.as_str(), 0).unwrap());
         FnUpdate::Param(parameter, Vec::new())
     } else {
-        let regulator = regulators[0];
+        let regulator = regulators[0].clone();
         let true_branch = explode_function(network, &regulators[1..], format!("{name_prefix}1"));
         let false_branch = explode_function(network, &regulators[1..], format!("{name_prefix}0"));
-        let var = FnUpdate::Var(regulator);
-        var.clone()
+        regulator
+            .clone()
             .implies(true_branch)
-            .and(var.negation().implies(false_branch))
+            .and(regulator.negation().implies(false_branch))
     }
 }

src/evaluation/algorithm.rs

@@ -86,7 +86,7 @@ pub fn eval_node(
     let result = match node.node_type {
         NodeType::TerminalNode(atom) => match atom {
             Atomic::True => graph.mk_unit_colored_vertices(),
-            Atomic::False => graph.mk_empty_vertices(),
+            Atomic::False => graph.mk_empty_colored_vertices(),
             Atomic::Var(name) => eval_hctl_var(graph, name.as_str()),
             Atomic::Prop(name) => eval_prop(graph, &name),
             // should not be reachable, as wild-card nodes are always evaluated earlier using cache

src/evaluation/hctl_operators_evaluation.rs

@@ -43,7 +43,10 @@ pub fn eval_xor(
 /// Note that validity of formula's propositions are checked beforehand.
 pub fn eval_prop(graph: &SymbolicAsyncGraph, name: &str) -> GraphColoredVertices {
     // propositions are checked during preproc, and must be valid network variables
-    let network_variable = graph.as_network().as_graph().find_variable(name).unwrap();
+    let network_variable = graph
+        .symbolic_context()
+        .find_network_variable(name)
+        .unwrap();
 
     GraphColoredVertices::new(
         graph
@@ -155,7 +158,7 @@ pub fn eval_eu_saturated(
     let mut done = false;
     while !done {
         done = true;
-        for var in graph.as_network().variables().rev() {
+        for var in graph.variables().rev() {
             let update = phi1.intersect(&graph.var_pre(var, &result)).minus(&result);
             if !update.is_empty() {
                 result = result.union(&update);
@@ -184,7 +187,7 @@ pub fn eval_eg(
     self_loop_states: &GraphColoredVertices,
 ) -> GraphColoredVertices {
     let mut old_set = phi.clone();
-    let mut new_set = graph.mk_empty_vertices();
+    let mut new_set = graph.mk_empty_colored_vertices();
 
     while old_set != new_set {
         new_set = old_set.clone();
@@ -230,7 +233,7 @@ pub fn eval_au(
     self_loop_states: &GraphColoredVertices,
 ) -> GraphColoredVertices {
     let mut old_set = phi2.clone();
-    let mut new_set = graph.mk_empty_vertices();
+    let mut new_set = graph.mk_empty_colored_vertices();
 
     while old_set != new_set {
         new_set = old_set.clone();

src/evaluation/low_level_operations.rs

@@ -14,7 +14,6 @@ fn create_comparator(
     other_hctl_var_name_opt: Option<&str>,
 ) -> GraphColoredVertices {
     // TODO: merge both branches to not repeat code
-    let reg_graph = graph.as_network().as_graph();
     let mut comparator = graph.mk_unit_colored_vertices().as_bdd().clone();
 
     // HCTL variables are named x, xx, xxx, ...
@@ -26,8 +25,8 @@ fn create_comparator(
         // HCTL variables are named x, xx, xxx, ...
         let other_hctl_var_id = other_hctl_var_name.len() - 1; // len of var codes its index
 
-        for network_var_id in reg_graph.variables() {
-            let network_var_name = reg_graph.get_variable_name(network_var_id);
+        for network_var_id in graph.variables() {
+            let network_var_name = graph.get_variable_name(network_var_id);
 
             // extra BDD vars are called "{network_variable}_extra_{i}"
             let hctl_var1_component_name = format!("{network_var_name}_extra_{hctl_var_id}");
@@ -46,13 +45,13 @@ fn create_comparator(
     } else {
         // do comparator between network vars and a HCTL variable
 
-        for network_var_id in reg_graph.variables() {
-            let network_var_name = reg_graph.get_variable_name(network_var_id);
+        for network_var_id in graph.variables() {
+            let network_var_name = graph.get_variable_name(network_var_id);
             let hctl_component_name = format!("{network_var_name}_extra_{hctl_var_id}");
             let bdd_network_var = graph
                 .symbolic_context()
                 .bdd_variable_set()
-                .mk_var_by_name(network_var_name);
+                .mk_var_by_name(network_var_name.as_str());
             let bdd_hctl_component = graph
                 .symbolic_context()
                 .bdd_variable_set()
@@ -97,7 +96,7 @@ pub fn project_out_hctl_var(
 
     // collect all BDD vars that encode the HCTL var
     let mut bdd_vars_to_project: Vec<BddVariable> = Vec::new();
-    for network_var in graph.as_network().as_graph().variables() {
+    for network_var in graph.variables() {
         let extra_vars = graph.symbolic_context().extra_state_variables(network_var);
         bdd_vars_to_project.push(*extra_vars.get(hctl_var_id).unwrap());
     }

src/evaluation/mark_duplicate_subform.rs

@@ -185,6 +185,7 @@ mod tests {
     use crate::preprocessing::parser::{
         parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula,
     };
+    use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext;
     use biodivine_lib_param_bn::BooleanNetwork;
     use std::collections::HashMap;
 
@@ -196,8 +197,9 @@ mod tests {
 
         // define any placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
-        let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap();
+        let tree = parse_and_minimize_hctl_formula(&ctx, formula).unwrap();
         let duplicates = mark_duplicates_canonized_single(&tree);
 
         assert_eq!(duplicates, expected_duplicates);
@@ -214,8 +216,9 @@ mod tests {
 
         // define any placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
-        let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap();
+        let tree = parse_and_minimize_hctl_formula(&ctx, formula).unwrap();
         let duplicates = mark_duplicates_canonized_single(&tree);
         assert_eq!(duplicates, expected_duplicates);
     }
@@ -236,10 +239,11 @@ mod tests {
 
         // define any placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
         let mut trees = Vec::new();
         for formula in formulae {
-            let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap();
+            let tree = parse_and_minimize_hctl_formula(&ctx, formula).unwrap();
             trees.push(tree);
         }
         let duplicates = mark_duplicates_canonized_multiple(&trees);
@@ -252,11 +256,12 @@ mod tests {
     fn test_duplicates_wild_cards() {
         // define a placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
         let formula = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%) & v1 & v1";
         let expected_duplicates = HashMap::from([("%subst%".to_string(), 1)]);
 
-        let tree = parse_and_minimize_extended_formula(&bn, formula).unwrap();
+        let tree = parse_and_minimize_extended_formula(&ctx, formula).unwrap();
         let duplicates = mark_duplicates_canonized_single(&tree);
         assert_eq!(duplicates, expected_duplicates);
     }

src/mc_utils.rs

@@ -21,7 +21,7 @@ pub fn get_extended_symbolic_graph(
     let context = SymbolicContext::with_extra_state_variables(bn, &map_num_vars)?;
     let unit = context.mk_constant(true);
 
-    SymbolicAsyncGraph::with_custom_context(bn.clone(), context, unit)
+    SymbolicAsyncGraph::with_custom_context(bn, context, unit)
 }
 
 /// Compute the set of all uniquely named HCTL variables in the formula tree.
@@ -113,7 +113,7 @@ fn collect_unique_wild_card_props_recursive(
 /// There must be `num_hctl_vars` extra symbolic BDD vars for each BN variable.
 pub fn check_hctl_var_support(stg: &SymbolicAsyncGraph, hctl_syntactic_tree: HctlTreeNode) -> bool {
     let num_hctl_vars = collect_unique_hctl_vars(hctl_syntactic_tree).len();
-    for bn_var in stg.as_network().variables() {
+    for bn_var in stg.variables() {
         if num_hctl_vars > stg.symbolic_context().extra_state_variables(bn_var).len() {
             return false;
         }
@@ -134,6 +134,7 @@ mod tests {
 
     use biodivine_lib_param_bn::BooleanNetwork;
 
+    use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext;
     use std::collections::{HashMap, HashSet};
 
     #[test]
@@ -156,10 +157,11 @@ mod tests {
 
         // define any placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
         // and for tree with minimized number of renamed state vars
         let modified_tree =
-            check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).unwrap();
+            check_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).unwrap();
         let expected_vars =
             HashSet::from_iter(vec!["x".to_string(), "xx".to_string(), "xxx".to_string()]);
         assert_eq!(collect_unique_hctl_vars(modified_tree), expected_vars);
@@ -181,10 +183,11 @@ mod tests {
     fn test_check_hctl_var_support() {
         // define any placeholder bn and stg with enough variables
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
+        let ctx = SymbolicContext::new(&bn).unwrap();
 
         // formula with 3 variables
         let formula = "!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))";
-        let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap();
+        let tree = parse_and_minimize_hctl_formula(&ctx, formula).unwrap();
 
         // the stg that supports the same amount variables as the formula (3)
         let stg = get_extended_symbolic_graph(&bn, 3).unwrap();

src/model_checking.rs

@@ -93,7 +93,7 @@ fn parse_hctl_and_validate(
     // parse all the formulae and check that graph supports enough HCTL vars
     let mut parsed_trees = Vec::new();
     for formula in formulae {
-        let tree = parse_and_minimize_hctl_formula(graph.as_network(), formula.as_str())?;
+        let tree = parse_and_minimize_hctl_formula(graph.symbolic_context(), formula.as_str())?;
         // check that given extended symbolic graph supports enough stated variables
         if !check_hctl_var_support(graph, tree.clone()) {
             return Err("Graph does not support enough HCTL state variables".to_string());
@@ -159,7 +159,7 @@ fn parse_extended_and_validate(
     // parse all the formulae and check that graph supports enough HCTL vars
     let mut parsed_trees = Vec::new();
     for formula in formulae {
-        let tree = parse_and_minimize_extended_formula(graph.as_network(), formula.as_str())?;
+        let tree = parse_and_minimize_extended_formula(graph.symbolic_context(), formula.as_str())?;
 
         // check that given extended symbolic graph supports enough stated variables
         if !check_hctl_var_support(graph, tree.clone()) {
@@ -248,7 +248,12 @@ pub fn model_check_formula_unsafe_ex(
 
     let mut eval_info = EvalContext::from_single_tree(&tree);
     // do not consider self-loops during EX computation (UNSAFE optimisation)
-    let result = eval_node(tree, graph, &mut eval_info, &graph.mk_empty_vertices());
+    let result = eval_node(
+        tree,
+        graph,
+        &mut eval_info,
+        &graph.mk_empty_colored_vertices(),
+    );
     Ok(result)
 }
 
@@ -655,7 +660,7 @@ $DivK: (!PleC & DivJ)
         let stg = get_extended_symbolic_graph(&bn, 1).unwrap();
 
         // test situation where one substitution is missing
-        let sub_context = HashMap::from([("s".to_string(), stg.mk_empty_vertices())]);
+        let sub_context = HashMap::from([("s".to_string(), stg.mk_empty_colored_vertices())]);
         let formula = "%s% & EF %t%".to_string();
         let res = parse_extended_and_validate(vec![formula], &stg, &sub_context);
         assert!(res.is_err());

src/postprocessing/sanitizing.rs

@@ -11,7 +11,9 @@ pub fn sanitize_colored_vertices(
     stg: &SymbolicAsyncGraph,
     colored_vertices: &GraphColoredVertices,
 ) -> GraphColoredVertices {
-    let canonical_bn = stg.as_network();
+    let canonical_bn = stg.as_network().unwrap_or_else(|| {
+        panic!("Cannot normalize STG with no associated network.");
+    });
     let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
     let sanitized_result_bdd = canonical_context
         .transfer_from(colored_vertices.as_bdd(), stg.symbolic_context())
@@ -23,7 +25,9 @@ pub fn sanitize_colored_vertices(
 /// that were used for representing HCTL state-variables. At the moment, we remove all symbolic
 /// variables.
 pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphColors {
-    let canonical_bn = stg.as_network();
+    let canonical_bn = stg.as_network().unwrap_or_else(|| {
+        panic!("Cannot normalize STG with no associated network.");
+    });
     let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
     let sanitized_result_bdd = canonical_context
         .transfer_from(colors.as_bdd(), stg.symbolic_context())
@@ -35,7 +39,9 @@ pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphC
 /// that were used for representing HCTL state-variables. At the moment, we remove all symbolic
 /// variables.
 pub fn sanitize_vertices(stg: &SymbolicAsyncGraph, vertices: &GraphVertices) -> GraphVertices {
-    let canonical_bn = stg.as_network();
+    let canonical_bn = stg.as_network().unwrap_or_else(|| {
+        panic!("Cannot normalize STG with no associated network.");
+    });
     let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
     let sanitized_result_bdd = canonical_context
         .transfer_from(vertices.as_bdd(), stg.symbolic_context())
@@ -63,7 +69,7 @@ mod tests {
     #[test]
     fn test_sanitize() {
         let bn = BooleanNetwork::try_from_bnet(MODEL).unwrap();
-        let canonical_stg = SymbolicAsyncGraph::new(bn.clone()).unwrap();
+        let canonical_stg = SymbolicAsyncGraph::new(&bn).unwrap();
         let extended_stg = get_extended_symbolic_graph(&bn, 1).unwrap();
 
         let fp_canonical = compute_steady_states(&canonical_stg);