diff --git a/classifier/Cargo.toml b/classifier/Cargo.toml index a794088a..806768bb 100644 --- a/classifier/Cargo.toml +++ b/classifier/Cargo.toml @@ -10,7 +10,7 @@ rust-version = "1.72" [dependencies] biodivine-lib-bdd = ">=0.5.1, <1.0.0" biodivine-lib-param-bn = ">=0.4.5, <1.0.0" -biodivine-hctl-model-checker = ">=0.1.7, <1.0.0" +biodivine-hctl-model-checker = "0.2.0" clap = { version = "4.1.1", features = ["derive"] } zip = "0.6.3" diff --git a/classifier/src/classification.rs b/classifier/src/classification.rs index 73d125f7..e6d17015 100644 --- a/classifier/src/classification.rs +++ b/classifier/src/classification.rs @@ -20,7 +20,6 @@ use biodivine_lib_param_bn::symbolic_async_graph::{ use biodivine_lib_param_bn::{BooleanNetwork, ModelAnnotation}; use std::cmp::max; -use std::collections::HashSet; /// Return the set of colors for which ALL system states are contained in the given color-vertex /// set (i.e., if the given relation is a result of model checking a property, get colors for which @@ -69,11 +68,11 @@ pub fn classify(output_zip: &str, input_path: &str) -> Result<(), String> { // Parse all formulae and count the max. number of HCTL variables across formulae. let assertion_tree = parse_and_minimize_hctl_formula(&bn, &assertion)?; - let mut num_hctl_vars = collect_unique_hctl_vars(assertion_tree.clone(), HashSet::new()).len(); + let mut num_hctl_vars = collect_unique_hctl_vars(assertion_tree.clone()).len(); let mut property_trees: Vec = Vec::new(); for (_name, formula) in &named_properties { let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str())?; - let tree_vars = collect_unique_hctl_vars(tree.clone(), HashSet::new()).len(); + let tree_vars = collect_unique_hctl_vars(tree.clone()).len(); num_hctl_vars = max(num_hctl_vars, tree_vars); property_trees.push(tree); } @@ -158,7 +157,6 @@ mod tests { use biodivine_hctl_model_checker::preprocessing::parser::parse_and_minimize_hctl_formula; use biodivine_lib_param_bn::{BooleanNetwork, ModelAnnotation}; use std::cmp::max; - use std::collections::HashSet; #[test] /// Test the formulae parsing and variable counting @@ -178,7 +176,7 @@ mod tests { let mut var_count = 0; for f in formulae { let tree = parse_and_minimize_hctl_formula(&bn, f.as_str()).unwrap(); - let c = collect_unique_hctl_vars(tree, HashSet::new()).len(); + let c = collect_unique_hctl_vars(tree).len(); var_count = max(c, var_count); } assert_eq!(var_count, 2); diff --git a/src-tauri/Cargo.toml b/src-tauri/Cargo.toml index 8cb50233..0d207107 100644 --- a/src-tauri/Cargo.toml +++ b/src-tauri/Cargo.toml @@ -15,7 +15,7 @@ tauri-build = { version = "1.2.1", features = [] } [dependencies] biodivine-lib-bdd = ">=0.5.1, <1.0.0" biodivine-lib-param-bn = ">=0.4.5, <1.0.0" -biodivine-hctl-model-checker = "0.1.7" +biodivine-hctl-model-checker = "0.2.0" rand = "0.8.5" clap = { version = "4.1.4", features = ["derive"] }