From 1e893faaf2573cb1b478d227c915a16e6c8de2db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Fri, 2 Feb 2024 18:15:21 +0100 Subject: [PATCH] Refactoring, with few potentially breaking changes. --- .../_test_against_precomputed.rs | 4 +- .../_test_extended_formulae.rs | 34 ++++++++--------- .../_test_formula_equivalences.rs | 8 ++-- .../_test_pattern_equivalences.rs | 4 +- .../_test_unsafe_optimization.rs | 10 ++--- .../_test_variable_domains.rs | 14 +++---- src/analysis.rs | 3 +- src/mc_utils.rs | 7 ++-- src/model_checking.rs | 38 +++++++++---------- src/preprocessing/parser.rs | 9 ++--- src/preprocessing/utils.rs | 33 ++++++++++------ 11 files changed, 82 insertions(+), 82 deletions(-) diff --git a/src/_test_model_checking/_test_against_precomputed.rs b/src/_test_model_checking/_test_against_precomputed.rs index 00ee59e..0465115 100644 --- a/src/_test_model_checking/_test_against_precomputed.rs +++ b/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()); diff --git a/src/_test_model_checking/_test_extended_formulae.rs b/src/_test_model_checking/_test_extended_formulae.rs index 09de330..9c87466 100644 --- a/src/_test_model_checking/_test_extended_formulae.rs +++ b/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,21 +50,19 @@ 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()); @@ -72,10 +70,8 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) { // 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()) diff --git a/src/_test_model_checking/_test_formula_equivalences.rs b/src/_test_model_checking/_test_formula_equivalences.rs index 3d59f45..0448004 100644 --- a/src/_test_model_checking/_test_formula_equivalences.rs +++ b/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()); } } diff --git a/src/_test_model_checking/_test_pattern_equivalences.rs b/src/_test_model_checking/_test_pattern_equivalences.rs index 19688bc..87516bb 100644 --- a/src/_test_model_checking/_test_pattern_equivalences.rs +++ b/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()); } } diff --git a/src/_test_model_checking/_test_unsafe_optimization.rs b/src/_test_model_checking/_test_unsafe_optimization.rs index a8a14c4..a02ccd6 100644 --- a/src/_test_model_checking/_test_unsafe_optimization.rs +++ b/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()); } } diff --git a/src/_test_model_checking/_test_variable_domains.rs b/src/_test_model_checking/_test_variable_domains.rs index a446f73..c33f1c8 100644 --- a/src/_test_model_checking/_test_variable_domains.rs +++ b/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()); } diff --git a/src/analysis.rs b/src/analysis.rs index 0c0d79a..0397927 100644 --- a/src/analysis.rs +++ b/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); diff --git a/src/mc_utils.rs b/src/mc_utils.rs index 36d2a00..84b859e 100644 --- a/src/mc_utils.rs +++ b/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); diff --git a/src/model_checking.rs b/src/model_checking.rs index 6fca90c..1ca2cb7 100644 --- a/src/model_checking.rs +++ b/src/model_checking.rs @@ -90,13 +90,13 @@ pub fn model_check_tree( /// Parse given HCTL formulae into syntactic trees and perform compatibility check with /// the provided `graph` (i.e., check if `graph` object supports enough sets of symbolic variables). fn parse_and_validate( - formulae: Vec, + formulae: Vec<&str>, graph: &SymbolicAsyncGraph, ) -> Result, String> { // 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.symbolic_context(), formula.as_str())?; + let tree = parse_and_minimize_hctl_formula(graph.symbolic_context(), formula)?; // 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()); @@ -110,7 +110,7 @@ fn parse_and_validate( /// Return the resulting sets of colored vertices (in the same order as input formulae). /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. pub fn model_check_multiple_formulae( - formulae: Vec, + formulae: Vec<&str>, graph: &SymbolicAsyncGraph, ) -> Result, String> { // get the abstract syntactic trees @@ -122,7 +122,7 @@ pub fn model_check_multiple_formulae( /// Perform the model checking for the list of formulae, but do not sanitize the results. /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. pub fn model_check_multiple_formulae_dirty( - formulae: Vec, + formulae: Vec<&str>, graph: &SymbolicAsyncGraph, ) -> Result, String> { // get the abstract syntactic trees @@ -135,7 +135,7 @@ pub fn model_check_multiple_formulae_dirty( /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. /// Return the resulting set of colored vertices. pub fn model_check_formula( - formula: String, + formula: &str, graph: &SymbolicAsyncGraph, ) -> Result { let result = model_check_multiple_formulae(vec![formula], graph)?; @@ -145,7 +145,7 @@ pub fn model_check_formula( /// Perform the model checking for given formula, but do not sanitize the result. /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. pub fn model_check_formula_dirty( - formula: String, + formula: &str, graph: &SymbolicAsyncGraph, ) -> Result { let result = model_check_multiple_formulae_dirty(vec![formula], graph)?; @@ -157,7 +157,7 @@ pub fn model_check_formula_dirty( /// /// Returns a triplet - a syntactic tree, context mapping for wild-card props, and context mapping for domains. fn parse_and_validate_extended( - formulae: Vec, + formulae: Vec<&str>, graph: &SymbolicAsyncGraph, context_sets: &LabelToSetMap, ) -> Result<(Vec, LabelToSetMap, LabelToSetMap), String> { @@ -166,7 +166,7 @@ fn parse_and_validate_extended( let mut props_context = HashMap::new(); let mut domains_context = HashMap::new(); for formula in formulae { - let tree = parse_and_minimize_extended_formula(graph.symbolic_context(), formula.as_str())?; + let tree = parse_and_minimize_extended_formula(graph.symbolic_context(), formula)?; // check that given extended symbolic graph supports enough stated variables if !check_hctl_var_support(graph, tree.clone()) { @@ -191,7 +191,7 @@ fn parse_and_validate_extended( /// The `context_props` is a mapping determining how `wild-card propositions` and `variable domains` are evaluated. /// These BDDs must only depend on BN variables and parameters, not on any other symbolic variables. pub fn model_check_multiple_extended_formulae_dirty( - formulae: Vec, + formulae: Vec<&str>, stg: &SymbolicAsyncGraph, context_sets: &LabelToSetMap, ) -> Result, String> { @@ -228,7 +228,7 @@ pub fn model_check_multiple_extended_formulae_dirty( /// The `context_props` is a mapping determining how `wild-card propositions` and `variable domains` are evaluated. /// These BDDs must only depend on BN variables and parameters, not on any other symbolic variables. pub fn model_check_multiple_extended_formulae( - formulae: Vec, + formulae: Vec<&str>, stg: &SymbolicAsyncGraph, context_sets: &LabelToSetMap, ) -> Result, String> { @@ -248,7 +248,7 @@ pub fn model_check_multiple_extended_formulae( /// The `context_props` is a mapping determining how `wild-card propositions` and `variable domains` are evaluated. /// These BDDs must only depend on BN variables and parameters, not on any other symbolic variables. pub fn model_check_extended_formula( - formula: String, + formula: &str, stg: &SymbolicAsyncGraph, context_sets: &LabelToSetMap, ) -> Result { @@ -263,7 +263,7 @@ pub fn model_check_extended_formula( /// The `context_props` is a mapping determining how `wild-card propositions` and `variable domains` are evaluated. /// These BDDs must only depend on BN variables and parameters, not on any other symbolic variables. pub fn model_check_extended_formula_dirty( - formula: String, + formula: &str, stg: &SymbolicAsyncGraph, context_sets: &LabelToSetMap, ) -> Result { @@ -279,7 +279,7 @@ pub fn model_check_extended_formula_dirty( /// /// Also, this does not sanitize results. pub fn model_check_formula_unsafe_ex( - formula: String, + formula: &str, graph: &SymbolicAsyncGraph, ) -> Result { let tree = parse_and_validate(vec![formula], graph)?[0].clone(); @@ -314,7 +314,7 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 1).unwrap(); // define formula with two variables - let formula = "!{x}: !{y}: (AX {x} & AX {y})".to_string(); + let formula = "!{x}: !{y}: (AX {x} & AX {y})"; assert!(model_check_formula(formula, &stg).is_err()); } @@ -326,7 +326,7 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); // define formula that contains free variable - let formula = "AX {x}".to_string(); + let formula = "AX {x}"; assert!(model_check_formula(formula, &stg).is_err()); } @@ -338,7 +338,7 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); // define formula with several times quantified var - let formula = "!{x}: !{x}: AX {x}".to_string(); + let formula = "!{x}: !{x}: AX {x}"; assert!(model_check_formula(formula, &stg).is_err()); } @@ -350,7 +350,7 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); // define formula with an invalid proposition - let formula = "AX invalid_proposition".to_string(); + let formula = "AX invalid_proposition"; assert!(model_check_formula(formula, &stg).is_err()); } @@ -364,7 +364,7 @@ mod tests { // test situation where one substitution is missing let context_sets = HashMap::from([("s".to_string(), stg.mk_empty_colored_vertices())]); - let formula = "%s% & EF %t%".to_string(); + let formula = "%s% & EF %t%"; let res = parse_and_validate_extended(vec![formula], &stg, &context_sets); assert!(res.is_err()); assert_eq!( @@ -374,7 +374,7 @@ mod tests { // test situation where one domain is missing let context_sets = HashMap::from([("a".to_string(), stg.mk_empty_colored_vertices())]); - let formula = "!{x} in %a%: !{y} in %b%: AX {x}".to_string(); + let formula = "!{x} in %a%: !{y} in %b%: AX {x}"; let res = parse_and_validate_extended(vec![formula], &stg, &context_sets); assert!(res.is_err()); assert_eq!( diff --git a/src/preprocessing/parser.rs b/src/preprocessing/parser.rs index 06ab95b..c79fe07 100644 --- a/src/preprocessing/parser.rs +++ b/src/preprocessing/parser.rs @@ -14,7 +14,6 @@ use crate::preprocessing::tokenizer::{ }; use crate::preprocessing::utils::validate_props_and_rename_vars; use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; -use std::collections::HashMap; /// Parse an HCTL formula string representation into an actual formula tree. /// Basically a wrapper for tokenize+parse (used often for testing/debug purposes). @@ -40,11 +39,11 @@ pub fn parse_extended_formula(formula: &str) -> Result { /// set of variables. /// Basically a wrapper for the whole preprocessing step (tokenize + parse + rename vars). pub fn parse_and_minimize_hctl_formula( - ctx: &SymbolicContext, + symbolic_context: &SymbolicContext, formula: &str, ) -> Result { let tree = parse_hctl_formula(formula)?; - let tree = validate_props_and_rename_vars(tree, HashMap::new(), String::new(), ctx)?; + let tree = validate_props_and_rename_vars(tree, symbolic_context)?; Ok(tree) } @@ -52,11 +51,11 @@ pub fn parse_and_minimize_hctl_formula( /// with renamed (minimized) set of variables. /// Extended formulae can include `wild-card propositions` in form "%proposition%". pub fn parse_and_minimize_extended_formula( - ctx: &SymbolicContext, + symbolic_context: &SymbolicContext, formula: &str, ) -> Result { let tree = parse_extended_formula(formula)?; - let tree = validate_props_and_rename_vars(tree, HashMap::new(), String::new(), ctx)?; + let tree = validate_props_and_rename_vars(tree, symbolic_context)?; Ok(tree) } diff --git a/src/preprocessing/utils.rs b/src/preprocessing/utils.rs index 231f144..4ff844f 100644 --- a/src/preprocessing/utils.rs +++ b/src/preprocessing/utils.rs @@ -13,6 +13,17 @@ use std::collections::HashMap; /// Then renames all HCTL vars in the formula's tree to a pseudo-canonical form - "x", "xx", ... /// It renames as many variables as possible to identical names, without affecting the semantics. pub fn validate_props_and_rename_vars( + orig_tree: HctlTreeNode, + symbolic_context: &SymbolicContext, +) -> Result { + validate_and_rename_recursive(orig_tree, HashMap::new(), String::new(), symbolic_context) +} + +/// Checks that all HCTL variables in the formula's syntactic tree are quantified (exactly once) and that +/// its propositions are valid BN variables. +/// Then renames all HCTL vars in the formula's tree to a pseudo-canonical form - "x", "xx", ... +/// It renames as many variables as possible to identical names, without affecting the semantics. +fn validate_and_rename_recursive( orig_tree: HctlTreeNode, mut renaming_map: HashMap, mut last_used_name: String, @@ -46,18 +57,18 @@ pub fn validate_props_and_rename_vars( // just dive one level deeper for unary nodes, and rename string NodeType::Unary(op, child) => { let node = - validate_props_and_rename_vars(*child, renaming_map, last_used_name.clone(), ctx)?; + validate_and_rename_recursive(*child, renaming_map, last_used_name.clone(), ctx)?; Ok(HctlTreeNode::mk_unary(node, op)) } // just dive deeper for binary nodes, and rename string NodeType::Binary(op, left, right) => { - let node1 = validate_props_and_rename_vars( + let node1 = validate_and_rename_recursive( *left, renaming_map.clone(), last_used_name.clone(), ctx, )?; - let node2 = validate_props_and_rename_vars(*right, renaming_map, last_used_name, ctx)?; + let node2 = validate_and_rename_recursive(*right, renaming_map, last_used_name, ctx)?; Ok(HctlTreeNode::mk_binary(node1, node2, op)) } // hybrid nodes are more complicated @@ -79,7 +90,7 @@ pub fn validate_props_and_rename_vars( } // dive deeper - let node = validate_props_and_rename_vars( + let node = validate_and_rename_recursive( *child, renaming_map.clone(), last_used_name.clone(), @@ -275,19 +286,19 @@ mod tests { fn validation_error_free_vars() { // 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(); // define and parse formula with free variable let formula = "AX {x}"; let tree = parse_hctl_formula(formula).unwrap(); - let result = validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx); + let result = validate_props_and_rename_vars(tree, &symbolic_context); assert!(result.is_err()); assert_eq!(result.err().unwrap(), "Variable x is free.".to_string()); // define and parse formula with free variable in jump operator let formula = "@{x}: v1"; let tree = parse_hctl_formula(formula).unwrap(); - let result = validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx); + let result = validate_props_and_rename_vars(tree, &symbolic_context); assert!(result.is_err()); assert_eq!( result.err().unwrap(), @@ -300,13 +311,13 @@ mod tests { fn validation_error_invalid_quantification() { // 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(); // define and parse formula with two variables let formula = "!{x}: !{x}: AX {x}"; let tree = parse_hctl_formula(formula).unwrap(); - assert!(validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).is_err()); + assert!(validate_props_and_rename_vars(tree, &symbolic_context).is_err()); } #[test] @@ -314,12 +325,12 @@ mod tests { fn validation_error_invalid_propositions() { // define a placeholder bn with only 1 prop v1 let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); - let ctx = SymbolicContext::new(&bn).unwrap(); + let symbolic_context = SymbolicContext::new(&bn).unwrap(); // define and parse formula with invalid proposition let formula = "AX invalid_proposition"; let tree = parse_hctl_formula(formula).unwrap(); - assert!(validate_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).is_err()); + assert!(validate_props_and_rename_vars(tree, &symbolic_context).is_err()); } }