From 691eeb270e520a1f2dbe8ba0c6a209f3195b4af4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Fri, 2 Feb 2024 17:29:53 +0100 Subject: [PATCH] Merge arguments for raw sets for wild-card properties and variable domains --- .../_test_extended_formulae.rs | 86 ++++++++++----- .../_test_pattern_equivalences.rs | 8 +- .../_test_variable_domains.rs | 43 +++----- src/model_checking.rs | 102 +++++++----------- src/preprocessing/utils.rs | 36 +++---- 5 files changed, 126 insertions(+), 149 deletions(-) diff --git a/src/_test_model_checking/_test_extended_formulae.rs b/src/_test_model_checking/_test_extended_formulae.rs index 2860a36..09de330 100644 --- a/src/_test_model_checking/_test_extended_formulae.rs +++ b/src/_test_model_checking/_test_extended_formulae.rs @@ -1,7 +1,8 @@ use crate::_test_model_checking::{MODEL_CELL_CYCLE, MODEL_CELL_DIVISION, MODEL_YEAST}; use crate::mc_utils::get_extended_symbolic_graph; use crate::model_checking::{ - model_check_extended_formula, model_check_formula, model_check_formula_dirty, + model_check_extended_formula, model_check_extended_formula_dirty, model_check_formula, + model_check_formula_dirty, }; use biodivine_lib_param_bn::BooleanNetwork; use std::collections::HashMap; @@ -21,10 +22,8 @@ fn model_check_extended_simple() { let result_v1 = model_check_formula(formula_v1, &stg).unwrap(); // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars) let result_sub = model_check_formula_dirty(sub_formula, &stg).unwrap(); - let context_props = HashMap::from([("s".to_string(), result_sub)]); - let context_domains = HashMap::new(); - let result_v2 = - model_check_extended_formula(formula_v2, &stg, &context_props, &context_domains).unwrap(); + let context_sets = HashMap::from([("s".to_string(), result_sub)]); + let result_v2 = model_check_extended_formula(formula_v2, &stg, &context_sets).unwrap(); assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true()); // 2) second test, disjunction substituted @@ -35,10 +34,8 @@ fn model_check_extended_simple() { let result_v1 = model_check_formula(formula_v1, &stg).unwrap(); // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars) let result_sub = model_check_formula_dirty(sub_formula, &stg).unwrap(); - let context_props = HashMap::from([("s".to_string(), result_sub)]); - let context_domains = HashMap::new(); - let result_v2 = - model_check_extended_formula(formula_v2, &stg, &context_props, &context_domains).unwrap(); + let context_sets = HashMap::from([("s".to_string(), result_sub)]); + let result_v2 = model_check_extended_formula(formula_v2, &stg, &context_sets).unwrap(); assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true()); } @@ -60,25 +57,14 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) { 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 context_props = HashMap::from([("subst".to_string(), raw_set)]); - let context_domains = HashMap::new(); + 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_props, - &context_domains, - ) - .unwrap(); - let result2_v2 = model_check_extended_formula( - formula2_v2.to_string(), - &stg, - &context_props, - &context_domains, - ) - .unwrap(); + 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(); assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true()); assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true()); @@ -87,11 +73,9 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) { // 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, &empty_context) - .unwrap(); + model_check_extended_formula(formula1.to_string(), &stg, &empty_context).unwrap(); let result2_v2 = - model_check_extended_formula(formula2.to_string(), &stg, &empty_context, &empty_context) - .unwrap(); + model_check_extended_formula(formula2.to_string(), &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()); } @@ -108,3 +92,47 @@ fn model_check_extended_complex() { model_check_extended_complex_on_bn(bn2); model_check_extended_complex_on_bn(bn3); } + +/// 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 stg = get_extended_symbolic_graph(&bn, 1).unwrap(); + + // we must use 'dirty' version to avoid sanitation (BDDs must retain all symbolic vars) + let raw_set = model_check_formula_dirty(formula, &stg).unwrap(); + + let formulas = [ + "V{x} in %1%: @{x}: (%1% & %2%)", + "V{x} in %1%: @{x}: (%2% & %3%)", + "V{x} in %2%: @{x}: (%2% & %3%)", + ]; + + // context with three entries of the same set + let context = HashMap::from([ + ("1".to_string(), raw_set.clone()), + ("2".to_string(), raw_set.clone()), + ("3".to_string(), raw_set.clone()), + ]); + + for f in formulas { + let result = model_check_extended_formula_dirty(f.to_string(), &stg, &context).unwrap(); + assert!(result + .as_bdd() + .iff(stg.unit_colored_vertices().as_bdd()) + .is_true()); + } +} + +#[test] +/// Test checking tautology or contradiction formulae that contain both wild-card properties +/// and variable domains. Use all 3 pre-defined models. +fn model_check_extended_tautologies() { + let bn1 = BooleanNetwork::try_from(MODEL_CELL_DIVISION).unwrap(); + let bn2 = BooleanNetwork::try_from_bnet(MODEL_CELL_CYCLE).unwrap(); + let bn3 = BooleanNetwork::try_from_bnet(MODEL_YEAST).unwrap(); + + model_check_extended_tautologies_on_bn(bn1); + model_check_extended_tautologies_on_bn(bn2); + model_check_extended_tautologies_on_bn(bn3); +} diff --git a/src/_test_model_checking/_test_pattern_equivalences.rs b/src/_test_model_checking/_test_pattern_equivalences.rs index beb2c71..19688bc 100644 --- a/src/_test_model_checking/_test_pattern_equivalences.rs +++ b/src/_test_model_checking/_test_pattern_equivalences.rs @@ -11,7 +11,7 @@ use std::collections::HashMap; /// Test evaluation of pairs of equivalent pattern formulae on given BN model. /// The patterns (wild-card propositions) are evaluated to raw sets specified by `context`. -fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context: LabelToSetMap) { +fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context_sets: LabelToSetMap) { let equivalent_pattern_pairs = vec![ // AU equivalence ( @@ -29,10 +29,8 @@ fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context: La ]; for (f1, f2) in equivalent_pattern_pairs { - let result1 = - model_check_extended_formula(f1.to_string(), stg, &context, &HashMap::new()).unwrap(); - let result2 = - model_check_extended_formula(f2.to_string(), stg, &context, &HashMap::new()).unwrap(); + 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(); 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 6348fc8..a446f73 100644 --- a/src/_test_model_checking/_test_variable_domains.rs +++ b/src/_test_model_checking/_test_variable_domains.rs @@ -43,21 +43,14 @@ 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_props = HashMap::from([("s".to_string(), raw_set.clone())]); - let ctx_doms = HashMap::new(); - let res = model_check_extended_formula(f.to_string(), &stg, &ctx_props, &ctx_doms) - .unwrap(); + let ctx_sets = HashMap::from([("s".to_string(), raw_set.clone())]); + let res = model_check_extended_formula(f.to_string(), &stg, &ctx_sets).unwrap(); // eval the variant with a domain - let ctx_props = HashMap::new(); - let ctx_doms = HashMap::from([("s".to_string(), raw_set.clone())]); - let res_v2 = model_check_extended_formula( - f_with_domain.to_string(), - &stg, - &ctx_props, - &ctx_doms, - ) - .unwrap(); + 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(); assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true()); } } @@ -79,21 +72,14 @@ fn model_check_with_empty_domain() { ]; let empty_set = stg.mk_empty_colored_vertices(); - let context_domains = HashMap::from([("s".to_string(), empty_set)]); - let context_props = HashMap::new(); + let context = HashMap::from([("s".to_string(), empty_set)]); for (f, domain_f) in formulae_pairs { // eval the variant without domain first let res = model_check_formula(f.to_string(), &stg).unwrap(); // and now the variant with empty domain - let res_v2 = model_check_extended_formula( - domain_f.to_string(), - &stg, - &context_props, - &context_domains, - ) - .unwrap(); + let res_v2 = model_check_extended_formula(domain_f.to_string(), &stg, &context).unwrap(); assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true()); } @@ -151,23 +137,18 @@ fn model_check_with_domains_complex() { for (f1, f2) in formulae_pairs { // eval the variant with a domain - let ctx_props = HashMap::new(); - let ctx_doms = HashMap::from([ + let context = HashMap::from([ ("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, &ctx_props, &ctx_doms) - .unwrap(); + let res_v2 = model_check_extended_formula(f1.to_string(), &stg, &context).unwrap(); // eval the variant without domain (contains wild-card prop) - let ctx_props = HashMap::from([ + let context = HashMap::from([ ("s1".to_string(), raw_set_1.clone()), ("s2".to_string(), raw_set_2.clone()), ]); - let ctx_doms = HashMap::new(); - let res = model_check_extended_formula(f2.to_string(), &stg, &ctx_props, &ctx_doms) - .unwrap(); + let res = model_check_extended_formula(f2.to_string(), &stg, &context).unwrap(); assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true()); } diff --git a/src/model_checking.rs b/src/model_checking.rs index aec6445..6fca90c 100644 --- a/src/model_checking.rs +++ b/src/model_checking.rs @@ -14,9 +14,10 @@ use crate::preprocessing::hctl_tree::HctlTreeNode; use crate::preprocessing::parser::{ parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula, }; +use std::collections::HashMap; use crate::evaluation::LabelToSetMap; -use crate::preprocessing::utils::validate_wild_cards; +use crate::preprocessing::utils::validate_and_divide_wild_cards; use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; /// Perform the model checking for the list of HCTL formulae given by their syntax trees on a given transition `graph`. @@ -153,14 +154,17 @@ pub fn model_check_formula_dirty( /// Parse given extended 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). +/// +/// Returns a triplet - a syntactic tree, context mapping for wild-card props, and context mapping for domains. fn parse_and_validate_extended( formulae: Vec, graph: &SymbolicAsyncGraph, - subst_context_props: &LabelToSetMap, - subst_context_domains: &LabelToSetMap, -) -> Result, String> { + context_sets: &LabelToSetMap, +) -> Result<(Vec, LabelToSetMap, LabelToSetMap), String> { // parse all the formulae and check that graph supports enough HCTL vars let mut parsed_trees = Vec::new(); + 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())?; @@ -169,10 +173,14 @@ fn parse_and_validate_extended( return Err("Graph does not support enough HCTL state variables".to_string()); } - validate_wild_cards(&tree, subst_context_props, subst_context_domains)?; + let (tree_prop_context, tree_dom_context) = + validate_and_divide_wild_cards(&tree, context_sets)?; + + props_context.extend(tree_prop_context); + domains_context.extend(tree_dom_context); parsed_trees.push(tree); } - Ok(parsed_trees) + Ok((parsed_trees, props_context, domains_context)) } /// Perform the model checking for list of `extended` HCTL formulae on a given transition `graph`, @@ -180,25 +188,23 @@ fn parse_and_validate_extended( /// 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. /// -/// The `subst_context_props` is a mapping determining how `wild-card propositions` are evaluated. -/// The `subst_context_domains` is a mapping determining how `var domains` are evaluated. -/// Bdds of both must only depend on BN variables and colours, not on their symbolic variables. +/// 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, stg: &SymbolicAsyncGraph, - subst_context_props: &LabelToSetMap, - subst_context_domains: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result, String> { - // get the abstract syntactic trees and check compatibility with graph - let parsed_trees = - parse_and_validate_extended(formulae, stg, subst_context_props, subst_context_domains)?; + // get the abstract syntactic trees and divide context sets, plus check compatibility with graph + let (parsed_trees, context_props, context_domains) = + parse_and_validate_extended(formulae, stg, context_sets)?; // prepare the extended evaluation context // 1) find normal duplicate sub-formulae throughout all formulae + initiate caching structures let mut eval_info = EvalContext::from_multiple_trees(&parsed_trees); // 2) extended the cache with given substitution context for wild-card nodes - eval_info.extend_context_with_wild_cards(subst_context_props, subst_context_domains); + eval_info.extend_context_with_wild_cards(&context_props, &context_domains); // 3) pre-compute compute states with self-loops which will be needed during eval let self_loop_states = compute_steady_states(stg); @@ -219,21 +225,14 @@ pub fn model_check_multiple_extended_formulae_dirty( /// 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. /// -/// The `subst_context_props` is a mapping determining how `wild-card propositions` are evaluated. -/// The `subst_context_domains` is a mapping determining how `var domains` are evaluated. -/// Bdds of both must only depend on BN variables and colours, not on their symbolic variables. +/// 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, stg: &SymbolicAsyncGraph, - subst_context_props: &LabelToSetMap, - subst_context_domains: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result, String> { - let results = model_check_multiple_extended_formulae_dirty( - formulae, - stg, - subst_context_props, - subst_context_domains, - )?; + let results = model_check_multiple_extended_formulae_dirty(formulae, stg, context_sets)?; // sanitize the results' bdds - get rid of additional bdd vars used for HCTL vars let sanitized_results: Vec = results @@ -246,21 +245,14 @@ pub fn model_check_multiple_extended_formulae( /// Perform the model checking for a given `extended` HCTL formula on a given transition `graph`. /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. /// -/// The `subst_context_props` is a mapping determining how `wild-card propositions` are evaluated. -/// The `subst_context_domains` is a mapping determining how `var domains` are evaluated. -/// Bdds of both must only depend on BN variables and colours, not on their symbolic variables. +/// 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, stg: &SymbolicAsyncGraph, - subst_context_props: &LabelToSetMap, - subst_context_domains: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result { - let result = model_check_multiple_extended_formulae( - vec![formula], - stg, - subst_context_props, - subst_context_domains, - )?; + let result = model_check_multiple_extended_formulae(vec![formula], stg, context_sets)?; Ok(result[0].clone()) } @@ -268,21 +260,14 @@ pub fn model_check_extended_formula( /// but do not sanitize the results. /// The `graph` object MUST support enough sets of symbolic variables to represent all occurring HCTL vars. /// -/// The `subst_context_props` is a mapping determining how `wild-card propositions` are evaluated. -/// The `subst_context_domains` is a mapping determining how `var domains` are evaluated. -/// Bdds of both must only depend on BN variables and colours, not on their symbolic variables. +/// 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, stg: &SymbolicAsyncGraph, - subst_context_props: &LabelToSetMap, - subst_context_domains: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result { - let result = model_check_multiple_extended_formulae_dirty( - vec![formula], - stg, - subst_context_props, - subst_context_domains, - )?; + let result = model_check_multiple_extended_formulae_dirty(vec![formula], stg, context_sets)?; Ok(result[0].clone()) } @@ -378,15 +363,9 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); // test situation where one substitution is missing - let sub_context_props = HashMap::from([("s".to_string(), stg.mk_empty_colored_vertices())]); - let sub_context_domains = HashMap::new(); + let context_sets = HashMap::from([("s".to_string(), stg.mk_empty_colored_vertices())]); let formula = "%s% & EF %t%".to_string(); - let res = parse_and_validate_extended( - vec![formula], - &stg, - &sub_context_props, - &sub_context_domains, - ); + let res = parse_and_validate_extended(vec![formula], &stg, &context_sets); assert!(res.is_err()); assert_eq!( res.err().unwrap(), @@ -394,16 +373,9 @@ mod tests { ); // test situation where one domain is missing - let sub_context_props = HashMap::new(); - let sub_context_domains = - HashMap::from([("a".to_string(), stg.mk_empty_colored_vertices())]); + 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 res = parse_and_validate_extended( - vec![formula], - &stg, - &sub_context_props, - &sub_context_domains, - ); + let res = parse_and_validate_extended(vec![formula], &stg, &context_sets); assert!(res.is_err()); assert_eq!( res.err().unwrap(), diff --git a/src/preprocessing/utils.rs b/src/preprocessing/utils.rs index abb6262..231f144 100644 --- a/src/preprocessing/utils.rs +++ b/src/preprocessing/utils.rs @@ -104,16 +104,15 @@ pub fn validate_props_and_rename_vars( } /// Check that all wild-card propositions and variable domains in the formula's syntactic tree have -/// their corresponding "raw set" (context) in `context_props` or `context_domains`, respectively. +/// their corresponding "raw set" (context) in `context_sets`. pub fn validate_wild_cards( tree: &HctlTreeNode, - context_props: &LabelToSetMap, - context_domains: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result<(), String> { let (wild_card_props, var_domains) = collect_unique_wild_cards(tree.clone()); // check that all occurring wild-card props are present in `context_props` for wild_card in wild_card_props { - if !context_props.contains_key(wild_card.as_str()) { + if !context_sets.contains_key(wild_card.as_str()) { return Err(format!( "Wild-card prop `{}` lacks evaluation context.", wild_card @@ -122,7 +121,7 @@ pub fn validate_wild_cards( } // check that all occurring wild-card props are present in `context_domains` for var_domain in var_domains { - if !context_domains.contains_key(var_domain.as_str()) { + if !context_sets.contains_key(var_domain.as_str()) { return Err(format!( "Var domain `{}` lacks evaluation context.", var_domain @@ -138,7 +137,7 @@ pub fn validate_wild_cards( /// Returns two individual context subsets, one for wild-card propositions, and the other for variable domains. pub fn validate_and_divide_wild_cards( tree: &HctlTreeNode, - substitution_context: &LabelToSetMap, + context_sets: &LabelToSetMap, ) -> Result<(LabelToSetMap, LabelToSetMap), String> { let mut context_domains = HashMap::new(); let mut context_props = HashMap::new(); @@ -146,7 +145,7 @@ pub fn validate_and_divide_wild_cards( let (wild_card_props, var_domains) = collect_unique_wild_cards(tree.clone()); // check that all occurring wild-card props are present in `substitution_context` for wild_card in wild_card_props { - if !substitution_context.contains_key(wild_card.as_str()) { + if !context_sets.contains_key(wild_card.as_str()) { return Err(format!( "Wild-card prop `{}` lacks evaluation context.", wild_card @@ -154,13 +153,13 @@ pub fn validate_and_divide_wild_cards( } else { context_props.insert( wild_card.clone(), - substitution_context.get(&wild_card).unwrap().clone(), + context_sets.get(&wild_card).unwrap().clone(), ); } } // check that all occurring wild-card props are present in `substitution_context` for var_domain in var_domains { - if !substitution_context.contains_key(var_domain.as_str()) { + if !context_sets.contains_key(var_domain.as_str()) { return Err(format!( "Var domain `{}` lacks evaluation context.", var_domain @@ -168,7 +167,7 @@ pub fn validate_and_divide_wild_cards( } else { context_domains.insert( var_domain.clone(), - substitution_context.get(&var_domain).unwrap().clone(), + context_sets.get(&var_domain).unwrap().clone(), ); } } @@ -254,20 +253,19 @@ mod tests { let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); // test simple validation - let context_props = HashMap::from([("p".to_string(), stg.mk_empty_colored_vertices())]); - let context_domains = HashMap::from([("d".to_string(), stg.mk_empty_colored_vertices())]); + let context_sets = HashMap::from([ + ("p".to_string(), stg.mk_empty_colored_vertices()), + ("d".to_string(), stg.mk_empty_colored_vertices()), + ]); let formula = "!{x} in %d%: EF %p%"; let tree = parse_and_minimize_extended_formula(stg.symbolic_context(), formula).unwrap(); - let res = validate_wild_cards(&tree, &context_props, &context_domains); + let res = validate_wild_cards(&tree, &context_sets); assert!(res.is_ok()); // test validation combined with dividing set of wild-cards into propositions and domains - let context_combined = HashMap::from([ - ("p".to_string(), stg.mk_empty_colored_vertices()), - ("d".to_string(), stg.mk_empty_colored_vertices()), - ]); - let (context1, context2) = - validate_and_divide_wild_cards(&tree, &context_combined).unwrap(); + let context_props = HashMap::from([("p".to_string(), stg.mk_empty_colored_vertices())]); + let context_domains = HashMap::from([("d".to_string(), stg.mk_empty_colored_vertices())]); + let (context1, context2) = validate_and_divide_wild_cards(&tree, &context_sets).unwrap(); assert_eq!(context1, context_props); assert_eq!(context2, context_domains); }