Update classifier's source code to the newest version.

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<GraphColors> = 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,25 +140,25 @@ 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(())
 }
 
 #[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()]
-        );
-    }
 }

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<String> {
 ///
 /// 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<NamedFormulaeVec, String> {
+pub fn read_model_properties(
+    annotations: &ModelAnnotation,
+) -> Result<Vec<(String, String)>, 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<String> {
-    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>, 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, GraphColors>, 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::<Vec<_>>();
+
+    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))
 }

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!(