diff --git a/Cargo.toml b/Cargo.toml index c45b5d9..af72590 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.1, <1.0.0" -biodivine-lib-param-bn = ">=0.4.5, <1.0.0" +biodivine-lib-bdd = ">=0.5.2, <1.0.0" +biodivine-lib-param-bn = ">=0.4.7, <1.0.0" clap = { version = "4.1.4", features = ["derive"] } rand = "0.8.5" termcolor = "1.1.2" diff --git a/src/postprocessing/sanitizing.rs b/src/postprocessing/sanitizing.rs index 903962e..894cb25 100644 --- a/src/postprocessing/sanitizing.rs +++ b/src/postprocessing/sanitizing.rs @@ -1,88 +1,8 @@ //! Contains operations to sanitize bdds of their additional symbolic variables, //! making them compatible with remaining biodivine libraries. - -use biodivine_lib_bdd::Bdd; use biodivine_lib_param_bn::symbolic_async_graph::{ GraphColoredVertices, GraphColors, GraphVertices, SymbolicAsyncGraph, SymbolicContext, }; -use std::collections::HashMap; -use std::io::Write; - -/// Turns a BDD that is a valid representation of coloured state set in the -/// `model_checking_context` into a BDD of the equivalent set in the `canonical_context`. -/// -/// The method assumes that variables and parameters are ordered equivalently, they are just -/// augmented with extra model checking variables that are unused in the original BDD. -pub fn sanitize_bdd( - model_checking_context: &SymbolicContext, - canonical_context: &SymbolicContext, - bdd: &Bdd, -) -> Bdd { - // First, build a map that translates a "model checking" symbolic variable - // into an equivalent "canonical" variable. - let mut variable_map = HashMap::new(); - let mc_state_variables = model_checking_context.state_variables().iter(); - let mc_param_variables = model_checking_context.parameter_variables().iter(); - for mc_var in mc_state_variables.chain(mc_param_variables) { - let var_name = model_checking_context.bdd_variable_set().name_of(*mc_var); - let c_var = canonical_context - .bdd_variable_set() - .var_by_name(&var_name) - .expect("Mismatch in model variables."); - variable_map.insert(*mc_var, c_var); - } - - // Then verify that the ordering of these variables is the same across both contexts. - let mut mc_variables_sorted = Vec::from_iter(variable_map.keys().cloned()); - mc_variables_sorted.sort(); - let mut c_variables_sorted = Vec::from_iter(variable_map.values().cloned()); - c_variables_sorted.sort(); - for (mc, c) in mc_variables_sorted.iter().zip(c_variables_sorted.iter()) { - assert_eq!( - variable_map.get(mc), - Some(c), - "Mismatch in variable ordering." - ); - } - - // Now we know it is actually safe to translate the BDD. - - // Now we have to do a very dumb thing to translate a BDD variable to its actual "raw index". - // Sadly there isn't a nicer way to do this in lib-bdd right now. - let mut variable_map = variable_map - .into_iter() - .map(|(a, b)| (format!("{a}"), format!("{b}"))) - .collect::>(); - // BDD terminal nodes contain information about the number of variables instead of a variable id. - // We have to map this information too in the new BDD. - variable_map.insert( - format!("{}", model_checking_context.bdd_variable_set().num_vars()), - format!("{}", canonical_context.bdd_variable_set().num_vars()), - ); - - let mc_string = bdd.to_string(); - let mut c_string: Vec = Vec::new(); - write!(c_string, "|").unwrap(); - - for mc_node in mc_string.split('|') { - if mc_node.is_empty() { - // First and last item will be empty because there is an additional separator - // at the beginning/end of the string. - continue; - } - let mut node_data = mc_node.split(','); - // Low/high links remain the same, but the variable ID is translated. - let node_var = node_data.next().unwrap(); - let node_low = node_data.next().unwrap(); - let node_high = node_data.next().unwrap(); - let new_node_var = variable_map - .get(node_var) - .expect("Model checking BDD is using unexpected variables."); - write!(c_string, "{new_node_var},{node_low},{node_high}|").unwrap(); - } - - Bdd::from_string(&String::from_utf8(c_string).unwrap()) -} /// Sanitize underlying BDD of a given coloured state set by removing the symbolic variables /// that were used for representing HCTL state-variables. At the moment, we remove all symbolic @@ -93,11 +13,9 @@ pub fn sanitize_colored_vertices( ) -> GraphColoredVertices { let canonical_bn = stg.as_network(); let canonical_context = SymbolicContext::new(canonical_bn).unwrap(); - let sanitized_result_bdd = sanitize_bdd( - stg.symbolic_context(), - &canonical_context, - colored_vertices.as_bdd(), - ); + let sanitized_result_bdd = canonical_context + .transfer_from(colored_vertices.as_bdd(), stg.symbolic_context()) + .unwrap(); GraphColoredVertices::new(sanitized_result_bdd, &canonical_context) } @@ -107,8 +25,9 @@ pub fn sanitize_colored_vertices( pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphColors { let canonical_bn = stg.as_network(); let canonical_context = SymbolicContext::new(canonical_bn).unwrap(); - let sanitized_result_bdd = - sanitize_bdd(stg.symbolic_context(), &canonical_context, colors.as_bdd()); + let sanitized_result_bdd = canonical_context + .transfer_from(colors.as_bdd(), stg.symbolic_context()) + .unwrap(); GraphColors::new(sanitized_result_bdd, &canonical_context) } @@ -118,11 +37,9 @@ pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphC pub fn sanitize_vertices(stg: &SymbolicAsyncGraph, vertices: &GraphVertices) -> GraphVertices { let canonical_bn = stg.as_network(); let canonical_context = SymbolicContext::new(canonical_bn).unwrap(); - let sanitized_result_bdd = sanitize_bdd( - stg.symbolic_context(), - &canonical_context, - vertices.as_bdd(), - ); + let sanitized_result_bdd = canonical_context + .transfer_from(vertices.as_bdd(), stg.symbolic_context()) + .unwrap(); GraphVertices::new(sanitized_result_bdd, &canonical_context) }