From f5ce2b5445b2538e884cbdca42b4a9255dbd5637 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Mon, 18 Dec 2023 16:39:13 +0100 Subject: [PATCH] Upgrade to latest `lib-param-bn`. --- Cargo.toml | 4 +-- src/aeon/itgr/mod.rs | 4 +-- src/aeon/scc_computation.rs | 2 +- src/analysis.rs | 7 ++-- src/bin/convert_aeon_to_bnet.rs | 16 +++++---- src/evaluation/algorithm.rs | 2 +- src/evaluation/hctl_operators_evaluation.rs | 11 +++--- src/evaluation/low_level_operations.rs | 13 ++++--- src/evaluation/mark_duplicate_subform.rs | 13 ++++--- src/mc_utils.rs | 11 +++--- src/model_checking.rs | 13 ++++--- src/postprocessing/sanitizing.rs | 14 +++++--- src/preprocessing/parser.rs | 12 +++---- src/preprocessing/utils.rs | 38 ++++++++++++--------- src/result_print.rs | 5 +-- 15 files changed, 96 insertions(+), 69 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index af72590..7f0f94f 100644 --- a/Cargo.toml +++ b/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" diff --git a/src/aeon/itgr/mod.rs b/src/aeon/itgr/mod.rs index 7737844..b0e1fc8 100644 --- a/src/aeon/itgr/mod.rs +++ b/src/aeon/itgr/mod.rs @@ -24,9 +24,9 @@ pub fn interleaved_transition_guided_reduction( graph: &SymbolicAsyncGraph, initial: GraphColoredVertices, ) -> (GraphColoredVertices, Vec) { - let variables = graph.as_network().variables().collect::>(); + let variables = graph.variables().collect::>(); 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, diff --git a/src/aeon/scc_computation.rs b/src/aeon/scc_computation.rs index b738f91..6ef82c9 100644 --- a/src/aeon/scc_computation.rs +++ b/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(), ) } diff --git a/src/analysis.rs b/src/analysis.rs index 2eec38c..127f0d5 100644 --- a/src/analysis.rs +++ b/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, diff --git a/src/bin/convert_aeon_to_bnet.rs b/src/bin/convert_aeon_to_bnet.rs index e142dfc..21fb497 100644 --- a/src/bin/convert_aeon_to_bnet.rs +++ b/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::>(); let name = format!("{}_", network.get_variable_name(variable)); explode_function(network, ®ulators, 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, ®ulators[1..], format!("{name_prefix}1")); let false_branch = explode_function(network, ®ulators[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)) } } diff --git a/src/evaluation/algorithm.rs b/src/evaluation/algorithm.rs index 756da59..4e756a9 100644 --- a/src/evaluation/algorithm.rs +++ b/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 diff --git a/src/evaluation/hctl_operators_evaluation.rs b/src/evaluation/hctl_operators_evaluation.rs index 45bf170..eeb7470 100644 --- a/src/evaluation/hctl_operators_evaluation.rs +++ b/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(); diff --git a/src/evaluation/low_level_operations.rs b/src/evaluation/low_level_operations.rs index aa3e883..249375b 100644 --- a/src/evaluation/low_level_operations.rs +++ b/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 = 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()); } diff --git a/src/evaluation/mark_duplicate_subform.rs b/src/evaluation/mark_duplicate_subform.rs index 3d12f82..258d979 100644 --- a/src/evaluation/mark_duplicate_subform.rs +++ b/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); } diff --git a/src/mc_utils.rs b/src/mc_utils.rs index 110c259..b722559 100644 --- a/src/mc_utils.rs +++ b/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(); diff --git a/src/model_checking.rs b/src/model_checking.rs index 0aedf21..86a5da2 100644 --- a/src/model_checking.rs +++ b/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()); diff --git a/src/postprocessing/sanitizing.rs b/src/postprocessing/sanitizing.rs index 894cb25..5b32e1f 100644 --- a/src/postprocessing/sanitizing.rs +++ b/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); diff --git a/src/preprocessing/parser.rs b/src/preprocessing/parser.rs index 30e8d3a..86cb754 100644 --- a/src/preprocessing/parser.rs +++ b/src/preprocessing/parser.rs @@ -13,9 +13,7 @@ use crate::preprocessing::tokenizer::{ try_tokenize_extended_formula, try_tokenize_formula, HctlToken, }; use crate::preprocessing::utils::check_props_and_rename_vars; - -use biodivine_lib_param_bn::BooleanNetwork; - +use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use std::collections::HashMap; /// Parse an HCTL formula string representation into an actual formula tree. @@ -42,11 +40,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( - bn: &BooleanNetwork, + ctx: &SymbolicContext, formula: &str, ) -> Result { let tree = parse_hctl_formula(formula)?; - let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?; + let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), ctx)?; Ok(tree) } @@ -54,11 +52,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( - bn: &BooleanNetwork, + ctx: &SymbolicContext, formula: &str, ) -> Result { let tree = parse_extended_formula(formula)?; - let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?; + let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), ctx)?; Ok(tree) } diff --git a/src/preprocessing/utils.rs b/src/preprocessing/utils.rs index 419a386..9dc4bfd 100644 --- a/src/preprocessing/utils.rs +++ b/src/preprocessing/utils.rs @@ -2,9 +2,7 @@ use crate::preprocessing::node::*; use crate::preprocessing::operator_enums::{Atomic, HybridOp}; - -use biodivine_lib_param_bn::BooleanNetwork; - +use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use std::collections::HashMap; /// Checks that all vars in formula are quantified (exactly once) and props are valid BN variables. @@ -14,7 +12,7 @@ pub fn check_props_and_rename_vars( orig_node: HctlTreeNode, mut mapping_dict: HashMap, mut last_used_name: String, - bn: &BooleanNetwork, + ctx: &SymbolicContext, ) -> Result { // If we find hybrid node with binder or exist, we add new var-name to rename_dict and stack (x, xx, xxx...) // After we leave this binder/exist, we remove its var from rename_dict @@ -32,11 +30,11 @@ pub fn check_props_and_rename_vars( } Atomic::Prop(name) => { // check that proposition corresponds to valid BN variable - let network_variable = bn.as_graph().find_variable(name); - if network_variable.is_none() { - return Err(format!("There is no network variable named {name}.")); + if ctx.find_network_variable(name).is_none() { + Err(format!("There is no network variable named {name}.")) + } else { + Ok(orig_node) } - Ok(orig_node) } // constants or wild-card propositions are always considered fine _ => return Ok(orig_node), @@ -44,7 +42,7 @@ pub fn check_props_and_rename_vars( // just dive one level deeper for unary nodes, and rename string NodeType::UnaryNode(op, child) => { let node = - check_props_and_rename_vars(*child, mapping_dict, last_used_name.clone(), bn)?; + check_props_and_rename_vars(*child, mapping_dict, last_used_name.clone(), ctx)?; Ok(HctlTreeNode::mk_unary_node(node, op)) } // just dive deeper for binary nodes, and rename string @@ -53,9 +51,9 @@ pub fn check_props_and_rename_vars( *left, mapping_dict.clone(), last_used_name.clone(), - bn, + ctx, )?; - let node2 = check_props_and_rename_vars(*right, mapping_dict, last_used_name, bn)?; + let node2 = check_props_and_rename_vars(*right, mapping_dict, last_used_name, ctx)?; Ok(HctlTreeNode::mk_binary_node(node1, node2, op)) } // hybrid nodes are more complicated @@ -81,7 +79,7 @@ pub fn check_props_and_rename_vars( *child, mapping_dict.clone(), last_used_name.clone(), - bn, + ctx, )?; // rename the variable in the node @@ -98,6 +96,7 @@ mod tests { parse_extended_formula, parse_hctl_formula, }; use crate::preprocessing::utils::check_props_and_rename_vars; + use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use biodivine_lib_param_bn::BooleanNetwork; use std::collections::HashMap; @@ -106,9 +105,10 @@ mod tests { fn test_state_var_minimization(formula: &str, formula_minimized: &str) { // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + let ctx = SymbolicContext::new(&bn).unwrap(); // automatically modify the original formula via preprocessing step - let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); + let tree = parse_and_minimize_hctl_formula(&ctx, formula).unwrap(); // get expected tree using the (same) formula with already manually minimized vars let tree_minimized = parse_hctl_formula(formula_minimized).unwrap(); @@ -144,12 +144,13 @@ mod tests { fn test_state_var_minimization_with_wild_cards() { // define any 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%)"; // same formula with already minimized vars let formula_minimized = "!{x}: 3{xx}: (@{x}: ~{xx} & %subst%) & (@{xx}: %subst%)"; - let tree = parse_and_minimize_extended_formula(&bn, formula).unwrap(); + let tree = parse_and_minimize_extended_formula(&ctx, formula).unwrap(); // get expected tree using the (same) formula with already manually minimized vars let tree_minimized = parse_extended_formula(formula_minimized).unwrap(); assert_eq!(tree_minimized, tree); @@ -160,12 +161,13 @@ mod tests { fn test_check_vars_error_1() { // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + let ctx = SymbolicContext::new(&bn).unwrap(); // define and parse formula with free variable let formula = "AX {x}"; let tree = parse_hctl_formula(formula).unwrap(); - assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); + assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).is_err()); } #[test] @@ -173,12 +175,13 @@ mod tests { fn test_check_vars_error_2() { // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + let ctx = 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!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); + assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).is_err()); } #[test] @@ -186,11 +189,12 @@ mod tests { fn test_check_props_error_1() { // define a placeholder bn with only 1 prop v1 let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + let ctx = SymbolicContext::new(&bn).unwrap(); // define and parse formula with invalid proposition let formula = "AX invalid_proposition"; let tree = parse_hctl_formula(formula).unwrap(); - assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); + assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &ctx).is_err()); } } diff --git a/src/result_print.rs b/src/result_print.rs index 91f1210..e8b8f30 100644 --- a/src/result_print.rs +++ b/src/result_print.rs @@ -57,13 +57,10 @@ pub(crate) fn print_results_full( // first print general summarizing information summarize_results(formula, results, start_time); - let network = graph.as_network(); for valuation in results.vertices().materialize().iter() { // print either colored (green/red) variable literals in conjunction if show_names { - let variable_name_strings = network - .variables() - .map(|id| network.get_variable_name(id).to_string()); + let variable_name_strings = graph.variables().map(|id| graph.get_variable_name(id)); let mut stdout = StandardStream::stdout(ColorChoice::Always); for (i, var) in variable_name_strings.enumerate() {