From 0ddab2c896569c32125f531b54c78c8c6d16d473 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sat, 21 Oct 2023 10:41:25 +0200 Subject: [PATCH] Update classifier's source code to the newest version. --- classifier/src/classification.rs | 60 ++++++-------- classifier/src/load_inputs.rs | 71 ++++++++++++++-- classifier/src/main.rs | 14 ++-- classifier/src/write_output.rs | 138 ++++++++++++++++++++++--------- 4 files changed, 198 insertions(+), 85 deletions(-) diff --git a/classifier/src/classification.rs b/classifier/src/classification.rs index e6d17015..232ebb81 100644 --- a/classifier/src/classification.rs +++ b/classifier/src/classification.rs @@ -1,7 +1,7 @@ //! Main high-level functionality regarding the BN classification based on HCTL properties. use crate::load_inputs::*; -use crate::write_output::{write_class_report_and_dump_bdds, write_empty_report}; +use crate::write_output::{write_classifier_output, write_empty_report}; use biodivine_hctl_model_checker::mc_utils::{ collect_unique_hctl_vars, get_extended_symbolic_graph, @@ -44,24 +44,30 @@ fn get_universal_colors( /// of properties is satisfied (universally). /// /// Report and BDDs representing resulting classes are generated into `output_zip` archive. -pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { +pub fn classify(model_path: &str, output_zip: &str) -> Result<(), String> { // TODO: allow caching between model-checking assertions and properties somehow // load the model and two sets of formulae (from model annotations) - let Ok(aeon_str) = std::fs::read_to_string(input_path) else { - return Err(format!("Input file `{input_path}` is not accessible.")); + let Ok(aeon_str) = std::fs::read_to_string(model_path) else { + return Err(format!("Input file `{model_path}` is not accessible.")); }; let bn = BooleanNetwork::try_from(aeon_str.as_str())?; let annotations = ModelAnnotation::from_model_string(aeon_str.as_str()); let assertions = read_model_assertions(&annotations); let named_properties = read_model_properties(&annotations)?; - println!("Loaded all inputs."); + println!("Loaded model and properties out of `{model_path}`."); - println!("Parsing formulae and generating model representation..."); + println!("Parsing formulae and generating symbolic representation..."); // Combine all assertions into one formula and add it to the list of properties. let assertion = build_combined_assertion(&assertions); + // Adjust message depending on the number of properties (singular/multiple) + let assertion_message = if assertions.len() == 1 { + "property (assertion)" + } else { + "properties (assertions)" + }; println!( - "Successfully parsed {} assertions and {} properties.", + "Successfully parsed all {} required {assertion_message} and all {} classification properties.", assertions.len(), named_properties.len(), ); @@ -79,30 +85,30 @@ pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { // Instantiate extended STG with enough variables to evaluate all formulae. let Ok(graph) = get_extended_symbolic_graph(&bn, num_hctl_vars as u16) else { - return Err("Unable to generate STG for provided BN model.".to_string()); + return Err("Unable to generate STG for provided PSBN model.".to_string()); }; println!( - "Successfully generated model with {} vars and {} params.", + "Successfully encoded model with {} variables and {} parameters.", graph.symbolic_context().num_state_variables(), graph.symbolic_context().num_parameter_variables(), ); println!( - "Model admits {:.0} parametrisations.", + "Model admits {:.0} instances.", graph.mk_unit_colors().approx_cardinality(), ); - println!("Evaluating assertions..."); + println!("Evaluating required properties (this may take some time)..."); // Compute the colors (universally) satisfying the combined assertion formula. let assertion_result = model_check_tree_dirty(assertion_tree, &graph)?; let valid_colors = get_universal_colors(&graph, &assertion_result); - println!("Assertions evaluated."); + println!("Required properties successfully evaluated."); println!( - "{:.0} parametrisations satisfy all assertions.", + "{:.0} instances satisfy all required properties.", valid_colors.approx_cardinality(), ); if valid_colors.is_empty() { - println!("No color satisfies given assertions. Aborting."); + println!("No instance satisfies given required properties. Aborting."); return write_empty_report(&assertions, output_zip).map_err(|e| format!("{e:?}")); } @@ -113,13 +119,14 @@ pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { valid_colors.as_bdd().clone(), )?; - println!("Evaluating properties..."); + println!("Evaluating classification properties (this may take some time)..."); // Model check all properties on the restricted graph. let property_result = model_check_multiple_trees_dirty(property_trees, &graph)?; let property_colors: Vec = property_result .iter() .map(|result| get_universal_colors(&graph, result)) .collect(); + println!("Classification properties successfully evaluated."); // This is an important step where we ensure that the "model checking context" // does not "leak" outside of the BN classifier. In essence, this ensures that the @@ -133,17 +140,17 @@ pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { .collect(); // do the classification while printing the report and dumping resulting BDDs - println!("Classifying based on model-checking results..."); - write_class_report_and_dump_bdds( + println!("Generating classification mapping based on model-checking results..."); + write_classifier_output( &assertions, - valid_colors, + &valid_colors, &named_properties, &property_colors, output_zip, aeon_str.as_str(), ) .map_err(|e| format!("{e:?}"))?; - println!("Results saved to {output_zip}."); + println!("Results saved to `{output_zip}`."); Ok(()) } @@ -151,7 +158,7 @@ pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { #[cfg(test)] mod tests { use crate::classification::{ - build_combined_assertion, extract_properties, read_model_assertions, read_model_properties, + build_combined_assertion, read_model_assertions, read_model_properties, }; use biodivine_hctl_model_checker::mc_utils::collect_unique_hctl_vars; use biodivine_hctl_model_checker::preprocessing::parser::parse_and_minimize_hctl_formula; @@ -251,17 +258,4 @@ mod tests { "Found multiple properties named `p1`." ); } - - #[test] - /// Test extracting properties from name-property pairs. - fn test_extract_properties() { - let named_props = vec![ - ("p1".to_string(), "true".to_string()), - ("p2".to_string(), "false".to_string()), - ]; - assert_eq!( - extract_properties(&named_props), - vec!["true".to_string(), "false".to_string()] - ); - } } diff --git a/classifier/src/load_inputs.rs b/classifier/src/load_inputs.rs index 4ac29905..838b0e17 100644 --- a/classifier/src/load_inputs.rs +++ b/classifier/src/load_inputs.rs @@ -1,8 +1,13 @@ //! Loading of various input components of the model, mainly of various properties/assertions. -use biodivine_lib_param_bn::ModelAnnotation; +use biodivine_lib_param_bn::{BooleanNetwork, ModelAnnotation}; -type NamedFormulaeVec = Vec<(String, String)>; +use biodivine_lib_bdd::Bdd; +use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; +use std::collections::HashMap; +use std::fs::File; +use std::io::Read; +use zip::ZipArchive; /// Read the list of assertions from an `.aeon` model annotation object. /// @@ -19,7 +24,9 @@ pub fn read_model_assertions(annotations: &ModelAnnotation) -> Vec { /// /// The properties are expected to appear as `#!dynamic_property: NAME: FORMULA` model annotations. /// They are returned in alphabetic order w.r.t. the property name. -pub fn read_model_properties(annotations: &ModelAnnotation) -> Result { +pub fn read_model_properties( + annotations: &ModelAnnotation, +) -> Result, String> { let Some(property_node) = annotations.get_child(&["dynamic_property"]) else { return Ok(Vec::new()); }; @@ -57,7 +64,59 @@ pub fn build_combined_assertion(assertions: &[String]) -> String { } } -/// Extract properties from name-property pairs. -pub fn extract_properties(named_props: &NamedFormulaeVec) -> Vec { - named_props.iter().map(|(_, x)| x.clone()).collect() +/// Read the contents of a file from a zip archive into a string. +fn read_zip_file(reader: &mut ZipArchive, file_name: &str) -> String { + let mut contents = String::new(); + let mut file = reader.by_name(file_name).unwrap(); + file.read_to_string(&mut contents).unwrap(); + contents +} + +/// Load the archive containing results produced by the classifier. +/// This function can also be used to load any `classification archives` of the same format (e.g., +/// those produced by the `build_classification_archive` function). +/// +/// Return mapping `category name -> color set` and whole model string in aeon format. +/// Category names are simply taken from BDD-file names in the archive. +pub fn load_classification_archive( + archive_path: String, +) -> Result<(HashMap, String), String> { + // Open the zip archive with classification results. + let archive_file = File::open(archive_path).map_err(|e| format!("{e:?}"))?; + let mut archive = ZipArchive::new(archive_file).map_err(|e| format!("{e:?}"))?; + + // Load the BN model (from the archive) and generate the extended STG. + let aeon_str = read_zip_file(&mut archive, "model.aeon"); + let bn = BooleanNetwork::try_from(aeon_str.as_str())?; + let graph = SymbolicAsyncGraph::new(bn)?; + + // collect the classification outcomes (colored sets) from the individual BDD dumps + let mut categories = HashMap::new(); + + // Load all class BDDs from files in the archive. + let files = archive + .file_names() + .map(|it| it.to_string()) + .collect::>(); + + for file in files { + if !file.starts_with("bdd_dump_") { + // Only read BDD dumps. + continue; + } + + let bdd_string = read_zip_file(&mut archive, file.as_str()); + let bdd = Bdd::from_string(bdd_string.as_str()); + let color_set = GraphColors::new(bdd, graph.symbolic_context()); + + let category_id = file.strip_prefix("bdd_dump_").unwrap(); + let category_id = category_id.strip_suffix(".txt").unwrap(); + + // The insert should create a new item, otherwise the archive is malformed. + assert!(categories + .insert(category_id.to_string(), color_set) + .is_none()); + } + + Ok((categories, aeon_str)) } diff --git a/classifier/src/main.rs b/classifier/src/main.rs index 2bbcee21..a3efab6a 100644 --- a/classifier/src/main.rs +++ b/classifier/src/main.rs @@ -1,11 +1,12 @@ //! Tool for symbolic classification of BN models based on dynamic properties. //! -//! Takes a path to a model in `.aeon` format containing a partially defined BN model and -//! two sets of HCTL formulae: assertions that must be satisfied, and properties that are -//! used for classification. All formulae are given in a form of model annotations. +//! Takes a path to a model in `.aeon` format containing a partially specified BN model and +//! two sets of HCTL formulae: required properties (assertions) that must be satisfied, +//! and classification properties that are used for classification. All formulae are given +//! in a form of model annotations. //! //! First, conjunction of assertions is model-checked, and then the set of remaining colors is -//! decomposed into categories based on the properties they satisfy. +//! decomposed into categories based on the classification properties they satisfy. //! pub mod classification; @@ -21,7 +22,8 @@ use std::time::SystemTime; #[derive(Parser)] #[clap(about = "Symbolic classifier for BN models based on dynamic properties.")] struct Arguments { - /// Path to a file in annotated `aeon` format containing a BN model and 2 sets of HCTL formulae. + /// Path to a file in annotated `aeon` format containing a PSBN model and 2 sets + /// of HCTL formulae. input_path: String, /// Path to a zip archive to which a report and BDD results will be dumped. @@ -45,7 +47,7 @@ fn main() { return; } - let classification_res = classify(output_name.as_str(), input_path.as_str()); + let classification_res = classify(input_path.as_str(), output_name.as_str()); if classification_res.is_err() { println!( diff --git a/classifier/src/write_output.rs b/classifier/src/write_output.rs index 27460c08..c408c9a0 100644 --- a/classifier/src/write_output.rs +++ b/classifier/src/write_output.rs @@ -2,9 +2,10 @@ use biodivine_lib_param_bn::biodivine_std::traits::Set; use biodivine_lib_param_bn::symbolic_async_graph::GraphColors; +use std::collections::HashMap; use std::fs::File; -use std::io::Write; +use std::io::{ErrorKind, Write}; use std::path::Path; use zip::write::{FileOptions, ZipWriter}; @@ -35,40 +36,14 @@ fn bool_vec_to_string(bool_data: &[bool]) -> String { .collect() } -/// Write a short summary regarding each category of the color decomposition, and dump a BDD -/// encoding the colors, all into the `archive_name` zip. -/// -/// - `assertion_formulae`: list of assertion formulae -/// - `all_valid_colors`: represents a "unit color set", i.e. all colors satisfying the -/// assertion formulae. -/// - `named_property_formulae`: lists the property names with their HCTL formula strings. -/// - `property_results`: lists the symbolic color set results for each property. -/// - `archive_name`: name of the `.zip` archive with results. -/// - `original_model_str`: original model in the aeon format -/// -/// Each result category is given by a set of colors that satisfy exactly the same properties. -/// -pub fn write_class_report_and_dump_bdds( +/// Prepare the initial part of the report regarding results for assertion formulae and +/// results for individual property formulae. +fn prepare_report_intro( assertion_formulae: &[String], - all_valid_colors: GraphColors, + all_valid_colors: &GraphColors, named_property_formulae: &[(String, String)], property_results: &[GraphColors], - archive_name: &str, - original_model_str: &str, -) -> Result<(), std::io::Error> { - // TODO: - // We are ignoring the zip result errors, but for now I do not want to convert - // everything to the same type of error... - - let archive_path = Path::new(archive_name); - // If there are some non existing dirs in path, create them. - let prefix = archive_path.parent().unwrap(); - std::fs::create_dir_all(prefix)?; - - // Create a zip writer for the desired archive. - let archive = File::create(archive_path)?; - let mut zip_writer = ZipWriter::new(archive); - +) -> Result, std::io::Error> { // We will first write the report into an intermediate buffer, // because we want to write it into the zip archive at the end // once all results are computed. @@ -102,6 +77,50 @@ pub fn write_class_report_and_dump_bdds( writeln!(report, "### Classes")?; writeln!(report)?; + Ok(report) +} + +/// Write a short summary regarding each category of the color decomposition, and dump a BDD +/// encoding the colors, all into the `archive_name` zip. +/// +/// - `assertion_formulae`: list of assertion formulae +/// - `all_valid_colors`: represents a "unit color set", i.e. all colors satisfying the +/// assertion formulae. +/// - `named_property_formulae`: lists the property names with their HCTL formula strings. +/// - `property_results`: lists the symbolic color set results for each property. +/// - `archive_name`: name of the `.zip` archive with results. +/// - `original_model_str`: original model in the aeon format +/// +/// Each result category is given by a set of colors that satisfy exactly the same properties. +pub fn write_classifier_output( + assertion_formulae: &[String], + all_valid_colors: &GraphColors, + named_property_formulae: &[(String, String)], + property_results: &[GraphColors], + archive_name: &str, + original_model_str: &str, +) -> Result<(), std::io::Error> { + let archive_path = Path::new(archive_name); + // If there are some non existing dirs in path, create them. + let prefix = archive_path + .parent() + .ok_or(std::io::Error::new(ErrorKind::Other, "Invalid path."))?; + std::fs::create_dir_all(prefix)?; + + // Create a zip writer for the desired archive. + let archive = File::create(archive_path)?; + let mut zip_writer = ZipWriter::new(archive); + + // We will first write the report into an intermediate buffer, + // because we want to write it into the zip archive at the end + // once all results are computed. + let mut report = prepare_report_intro( + assertion_formulae, + all_valid_colors, + named_property_formulae, + property_results, + )?; + // If this is broken, the number of properties is too high // to enumerate the combinations explicitly. assert!(property_results.len() < 31); @@ -133,7 +152,7 @@ pub fn write_class_report_and_dump_bdds( let bdd_file_name = format!("bdd_dump_{}.txt", bool_vec_to_string(&validity)); zip_writer .start_file(&bdd_file_name, FileOptions::default()) - .unwrap(); + .map_err(std::io::Error::from)?; category_colors.as_bdd().write_as_string(&mut zip_writer)?; } @@ -142,20 +161,60 @@ pub fn write_class_report_and_dump_bdds( // Finally, we can write the report. zip_writer .start_file("report.txt", FileOptions::default()) - .unwrap(); + .map_err(std::io::Error::from)?; zip_writer.write_all(&report)?; // Include the original model in the result bundle (we need to load it later). zip_writer .start_file("model.aeon", FileOptions::default()) - .unwrap(); + .map_err(std::io::Error::from)?; write!(zip_writer, "{original_model_str}")?; - zip_writer.finish().unwrap(); + zip_writer.finish().map_err(std::io::Error::from)?; Ok(()) } -/// Write a short summary regarding the computation where the assertions were not satisfied +/// Create classification archive for an arbitrary "map" of `string -> color set`. +pub fn build_classification_archive( + categories: HashMap, + archive_name: &str, + original_model_str: &str, +) -> Result<(), std::io::Error> { + let archive_path = Path::new(archive_name); + // If there are some non existing dirs in path, create them. + let prefix = archive_path + .parent() + .ok_or(std::io::Error::new(ErrorKind::Other, "Invalid path."))?; + std::fs::create_dir_all(prefix)?; + + // Create a zip writer for the desired archive. + let archive = File::create(archive_path)?; + let mut zip_writer = ZipWriter::new(archive); + + for (category_name, category_colors) in categories.iter() { + if !category_colors.is_empty() { + // If the BDD is not empty, the results go directly into the zip archive. + let bdd_file_name = format!("bdd_dump_{}.txt", category_name); + zip_writer + .start_file(&bdd_file_name, FileOptions::default()) + .map_err(std::io::Error::from)?; + + category_colors.as_bdd().write_as_string(&mut zip_writer)?; + } + } + + // Include the original model in the result bundle (we need to load it later). + zip_writer + .start_file("model.aeon", FileOptions::default()) + .map_err(std::io::Error::from)?; + write!(zip_writer, "{original_model_str}")?; + + zip_writer.finish().map_err(std::io::Error::from)?; + Ok(()) +} + +/// Write a short summary regarding the classification computation where the assertions were +/// not satisfied. pub fn write_empty_report( assertion_formulae: &[String], archive_name: &str, @@ -167,7 +226,7 @@ pub fn write_empty_report( // Here, we can write the empty report directly because there is nothing else to compute. zip_writer .start_file("report.txt", FileOptions::default()) - .unwrap(); + .map_err(std::io::Error::from)?; writeln!(zip_writer, "### Assertion formulae")?; writeln!(zip_writer)?; @@ -177,8 +236,7 @@ pub fn write_empty_report( writeln!(zip_writer, "0 colors satisfy combination of all assertions")?; writeln!(zip_writer)?; - zip_writer.finish().unwrap(); - + zip_writer.finish().map_err(std::io::Error::from)?; Ok(()) }