Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move sanitization to lib-param-bn #12

Merged
merged 1 commit into from
Dec 18, 2023
Merged

Move sanitization to lib-param-bn #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
101 changes: 9 additions & 92 deletions src/postprocessing/sanitizing.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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::<HashMap<_, _>>();
// 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<u8> = 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
Expand All @@ -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)
}

Expand All @@ -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)
}

Expand All @@ -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)
}

Expand Down