Refactoring, with few potentially breaking changes.

src/_test_model_checking/_test_against_precomputed.rs

@@ -11,12 +11,12 @@ fn compare_mc_results_with_expected(test_tuples: Vec<(&str, f64, f64, f64)>, bn:
     let stg = get_extended_symbolic_graph(&bn, 3).unwrap();
 
     for (formula, num_total, num_colors, num_states) in test_tuples {
-        let result = model_check_formula(formula.to_string(), &stg).unwrap();
+        let result = model_check_formula(formula, &stg).unwrap();
         assert_eq!(num_total, result.approx_cardinality());
         assert_eq!(num_colors, result.colors().approx_cardinality());
         assert_eq!(num_states, result.vertices().approx_cardinality());
 
-        let result = model_check_formula_dirty(formula.to_string(), &stg).unwrap();
+        let result = model_check_formula_dirty(formula, &stg).unwrap();
         assert_eq!(num_total, result.approx_cardinality());
         assert_eq!(num_colors, result.colors().approx_cardinality());
         assert_eq!(num_states, result.vertices().approx_cardinality());

src/_test_model_checking/_test_extended_formulae.rs

@@ -15,9 +15,9 @@ fn model_check_extended_simple() {
     let stg = get_extended_symbolic_graph(&bn, 1).unwrap();
 
     // 1) first test, only proposition substituted
-    let formula_v1 = "PleC & EF PleC".to_string();
-    let sub_formula = "PleC".to_string();
-    let formula_v2 = "%s% & EF %s%".to_string();
+    let formula_v1 = "PleC & EF PleC";
+    let sub_formula = "PleC";
+    let formula_v2 = "%s% & EF %s%";
 
     let result_v1 = model_check_formula(formula_v1, &stg).unwrap();
     // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars)
@@ -27,9 +27,9 @@ fn model_check_extended_simple() {
     assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true());
 
     // 2) second test, disjunction substituted
-    let formula_v1 = "EX (PleC | DivK)".to_string();
-    let sub_formula = "PleC | DivK".to_string();
-    let formula_v2 = "EX %s%".to_string();
+    let formula_v1 = "EX (PleC | DivK)";
+    let sub_formula = "PleC | DivK";
+    let formula_v2 = "EX %s%";
 
     let result_v1 = model_check_formula(formula_v1, &stg).unwrap();
     // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars)
@@ -50,32 +50,28 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) {
     // first define and evaluate the two formulae normally in one step
     let formula1 = "!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))";
     let formula2 = "3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & (!{z}: AX {z})) & EF ({y} & (!{z}: AX {z})) & AX (EF ({x} & (!{z}: AX {z})) ^ EF ({y} & (!{z}: AX {z})))";
-    let result1 = model_check_formula(formula1.to_string(), &stg).unwrap();
-    let result2 = model_check_formula(formula2.to_string(), &stg).unwrap();
+    let result1 = model_check_formula(formula1, &stg).unwrap();
+    let result2 = model_check_formula(formula2, &stg).unwrap();
 
     // now precompute part of the formula, and then substitute it as `wild-card proposition`
     let substitution_formula = "(!{z}: AX {z})";
     // we must use 'dirty' version to avoid sanitation (BDDs must retain all symbolic vars)
-    let raw_set = model_check_formula_dirty(substitution_formula.to_string(), &stg).unwrap();
+    let raw_set = model_check_formula_dirty(substitution_formula, &stg).unwrap();
     let context_sets = HashMap::from([("subst".to_string(), raw_set)]);
 
     let formula1_v2 = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%)";
     let formula2_v2 = "3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & %subst%) & EF ({y} & %subst%) & AX (EF ({x} & %subst%) ^ EF ({y} & %subst%))";
-    let result1_v2 =
-        model_check_extended_formula(formula1_v2.to_string(), &stg, &context_sets).unwrap();
-    let result2_v2 =
-        model_check_extended_formula(formula2_v2.to_string(), &stg, &context_sets).unwrap();
+    let result1_v2 = model_check_extended_formula(formula1_v2, &stg, &context_sets).unwrap();
+    let result2_v2 = model_check_extended_formula(formula2_v2, &stg, &context_sets).unwrap();
 
     assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true());
     assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true());
 
     // also double check that running "extended" evaluation on the original formula (without
     // wild-card propositions) is the same as running the standard variant
     let empty_context = HashMap::new();
-    let result1_v2 =
-        model_check_extended_formula(formula1.to_string(), &stg, &empty_context).unwrap();
-    let result2_v2 =
-        model_check_extended_formula(formula2.to_string(), &stg, &empty_context).unwrap();
+    let result1_v2 = model_check_extended_formula(formula1, &stg, &empty_context).unwrap();
+    let result2_v2 = model_check_extended_formula(formula2, &stg, &empty_context).unwrap();
     assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true());
     assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true());
 }
@@ -96,7 +92,7 @@ fn model_check_extended_complex() {
 /// Test checking tautology or contradiction formulae that contain both wild-card properties
 /// and variable domains.
 fn model_check_extended_tautologies_on_bn(bn: BooleanNetwork) {
-    let formula = "!{x}: AG EF {x}".to_string();
+    let formula = "!{x}: AG EF {x}";
     let stg = get_extended_symbolic_graph(&bn, 1).unwrap();
 
     // we must use 'dirty' version to avoid sanitation (BDDs must retain all symbolic vars)
@@ -116,7 +112,7 @@ fn model_check_extended_tautologies_on_bn(bn: BooleanNetwork) {
     ]);
 
     for f in formulas {
-        let result = model_check_extended_formula_dirty(f.to_string(), &stg, &context).unwrap();
+        let result = model_check_extended_formula_dirty(f, &stg, &context).unwrap();
         assert!(result
             .as_bdd()
             .iff(stg.unit_colored_vertices().as_bdd())

src/_test_model_checking/_test_formula_equivalences.rs

@@ -64,12 +64,12 @@ fn evaluate_equivalent_formulae(bn: BooleanNetwork) {
     // check that the results for the two formulae are equivalent in both sanitized and
     // non-sanitized version of model checking
     for (formula1, formula2) in equivalent_formulae_pairs {
-        let result1 = model_check_formula(formula1.to_string(), &stg).unwrap();
-        let result2 = model_check_formula(formula2.to_string(), &stg).unwrap();
+        let result1 = model_check_formula(formula1, &stg).unwrap();
+        let result2 = model_check_formula(formula2, &stg).unwrap();
         assert!(result1.as_bdd().iff(result2.as_bdd()).is_true());
 
-        let result1 = model_check_formula_dirty(formula1.to_string(), &stg).unwrap();
-        let result2 = model_check_formula_dirty(formula2.to_string(), &stg).unwrap();
+        let result1 = model_check_formula_dirty(formula1, &stg).unwrap();
+        let result2 = model_check_formula_dirty(formula2, &stg).unwrap();
         assert!(result1.as_bdd().iff(result2.as_bdd()).is_true());
     }
 }

src/_test_model_checking/_test_pattern_equivalences.rs

@@ -29,8 +29,8 @@ fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context_set
     ];
 
     for (f1, f2) in equivalent_pattern_pairs {
-        let result1 = model_check_extended_formula(f1.to_string(), stg, &context_sets).unwrap();
-        let result2 = model_check_extended_formula(f2.to_string(), stg, &context_sets).unwrap();
+        let result1 = model_check_extended_formula(f1, stg, &context_sets).unwrap();
+        let result2 = model_check_extended_formula(f2, stg, &context_sets).unwrap();
         assert!(result1.as_bdd().iff(result2.as_bdd()).is_true());
     }
 }

src/_test_model_checking/_test_unsafe_optimization.rs

@@ -16,13 +16,11 @@ fn test_unsafe_optimization() {
     for bn in bns {
         let stg = get_extended_symbolic_graph(&bn, 3).unwrap();
         // use formula for attractors that won't be recognized as the "attractor pattern"
-        let formula = "!{x}: AG EF ({x} & {x})".to_string();
-        let result1 = model_check_formula(formula.clone(), &stg).unwrap();
+        let formula = "!{x}: AG EF ({x} & {x})";
+        let result1 = model_check_formula(formula, &stg).unwrap();
         // result of the unsafe eval must be sanitized
-        let result2 = sanitize_colored_vertices(
-            &stg,
-            &model_check_formula_unsafe_ex(formula.clone(), &stg).unwrap(),
-        );
+        let result2 =
+            sanitize_colored_vertices(&stg, &model_check_formula_unsafe_ex(formula, &stg).unwrap());
         assert!(result1.as_bdd().iff(result2.as_bdd()).is_true());
     }
 }

src/_test_model_checking/_test_variable_domains.rs

@@ -44,13 +44,11 @@ fn model_check_with_domains() {
             for (f, f_with_domain) in formulae_pairs {
                 // eval the variant without domain first (contains wild-card prop)
                 let ctx_sets = HashMap::from([("s".to_string(), raw_set.clone())]);
-                let res = model_check_extended_formula(f.to_string(), &stg, &ctx_sets).unwrap();
+                let res = model_check_extended_formula(f, &stg, &ctx_sets).unwrap();
 
                 // eval the variant with a domain
                 let ctx_sets = HashMap::from([("s".to_string(), raw_set.clone())]);
-                let res_v2 =
-                    model_check_extended_formula(f_with_domain.to_string(), &stg, &ctx_sets)
-                        .unwrap();
+                let res_v2 = model_check_extended_formula(f_with_domain, &stg, &ctx_sets).unwrap();
                 assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
             }
         }
@@ -76,10 +74,10 @@ fn model_check_with_empty_domain() {
 
     for (f, domain_f) in formulae_pairs {
         // eval the variant without domain first
-        let res = model_check_formula(f.to_string(), &stg).unwrap();
+        let res = model_check_formula(f, &stg).unwrap();
 
         // and now the variant with empty domain
-        let res_v2 = model_check_extended_formula(domain_f.to_string(), &stg, &context).unwrap();
+        let res_v2 = model_check_extended_formula(domain_f, &stg, &context).unwrap();
 
         assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
     }
@@ -141,14 +139,14 @@ fn model_check_with_domains_complex() {
                     ("s1".to_string(), raw_set_1.clone()),
                     ("s2".to_string(), raw_set_2.clone()),
                 ]);
-                let res_v2 = model_check_extended_formula(f1.to_string(), &stg, &context).unwrap();
+                let res_v2 = model_check_extended_formula(f1, &stg, &context).unwrap();
 
                 // eval the variant without domain (contains wild-card prop)
                 let context = HashMap::from([
                     ("s1".to_string(), raw_set_1.clone()),
                     ("s2".to_string(), raw_set_2.clone()),
                 ]);
-                let res = model_check_extended_formula(f2.to_string(), &stg, &context).unwrap();
+                let res = model_check_extended_formula(f2, &stg, &context).unwrap();
 
                 assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
             }

src/analysis.rs

@@ -59,8 +59,7 @@ pub fn analyse_formulae(
         print_if_allowed(format!("Parsed version:       {tree}"), print_opt);
 
         // validate propositions and modify variable names in the formula
-        let modified_tree =
-            validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &plain_context)?;
+        let modified_tree = validate_props_and_rename_vars(tree, &plain_context)?;
         print_if_allowed(format!("Modified version:     {modified_tree}"), print_opt);
         print_if_allowed("-----".to_string(), print_opt);
 

src/mc_utils.rs

@@ -137,7 +137,7 @@ mod tests {
     use biodivine_lib_param_bn::BooleanNetwork;
 
     use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext;
-    use std::collections::{HashMap, HashSet};
+    use std::collections::HashSet;
 
     #[test]
     /// Test collecting state vars from HCTL formulae.
@@ -159,11 +159,10 @@ mod tests {
 
         // define any placeholder bn
         let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
-        let ctx = SymbolicContext::new(&bn).unwrap();
+        let symbolic_context = SymbolicContext::new(&bn).unwrap();
 
         // and for tree with minimized number of renamed state vars
-        let modified_tree =
-            validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).unwrap();
+        let modified_tree = validate_props_and_rename_vars(tree, &symbolic_context).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);