diff --git a/.githooks/README.txt b/.githooks/README.txt deleted file mode 100644 index de6b467..0000000 --- a/.githooks/README.txt +++ /dev/null @@ -1,3 +0,0 @@ -To globally enable githooks, run: - -git config core.hooksPath .githooks diff --git a/.githooks/pre-commit b/.githooks/pre-commit deleted file mode 100644 index 0aa2bb4..0000000 --- a/.githooks/pre-commit +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash - -# Runs automatic formatting and tests - -exec cargo fmt -- --check -exec cargo build --all-features -exec cargo test --all-features diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 553457d..57d0345 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -89,7 +89,7 @@ jobs: - name: Setup cargo-tarpaulin. run: cargo install cargo-tarpaulin - name: Run tarpaulin to compute coverage. - run: cargo tarpaulin --verbose --lib --examples --all-features --out Xml + run: cargo tarpaulin --verbose --lib --examples --all-features --out xml - name: Upload to codecov.io uses: codecov/codecov-action@v1.0.2 with: diff --git a/Cargo.toml b/Cargo.toml index a030b93..c45b5d9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "biodivine-hctl-model-checker" -version = "0.1.7" +version = "0.2.0" authors = ["OndÅ™ej Huvar ", "Samuel Pastva "] edition = "2021" description = "Library for symbolic HCTL model checking on partially defined Boolean networks." diff --git a/README.md b/README.md index ced2bbf..71128d6 100644 --- a/README.md +++ b/README.md @@ -18,6 +18,8 @@ This includes properties like stability, bi-stability, attractors, or oscillator To run the model checker, you will need the Rust compiler. We recommend following the instructions on [rustlang.org](https://www.rust-lang.org/learn/get-started). +If you are not familiar with Rust, there are also Python bindings for most of the important functionality in [AEON.py](https://github.com/sybila/biodivine-aeon-py). + ## Functionality This repository encompasses the CLI model-checking tool, and the model-checking library. @@ -85,3 +87,10 @@ The operator precedence is following (the lower, the stronger): * hybrid operators: 8 However, it is strongly recommended to use parentheses wherever possible to prevent any parsing issues. + +#### Wild-card properties + +The library also provides functions to model check extended formulae that contain so called "wild-card propositions". +These special propositions are evaluated as an arbitrary (coloured) set given by the user. +This allows the re-use of already pre-computed results in subsequent computations. +In formulae, the syntax of these propositions is `%property_name%`. \ No newline at end of file diff --git a/src/analysis.rs b/src/analysis.rs index 37463a4..2eec38c 100644 --- a/src/analysis.rs +++ b/src/analysis.rs @@ -1,7 +1,7 @@ //! Model-checking analysis from start to finish, with progress output and result prints. use crate::evaluation::algorithm::{compute_steady_states, eval_node}; -use crate::evaluation::eval_info::EvalInfo; +use crate::evaluation::eval_context::EvalContext; use crate::mc_utils::{collect_unique_hctl_vars, get_extended_symbolic_graph}; use crate::preprocessing::parser::parse_hctl_formula; use crate::preprocessing::utils::check_props_and_rename_vars; @@ -9,7 +9,7 @@ use crate::result_print::*; use biodivine_lib_param_bn::BooleanNetwork; -use std::collections::{HashMap, HashSet}; +use std::collections::HashMap; use std::time::SystemTime; /// Perform the whole model checking analysis regarding several (individual) formulae. This @@ -42,7 +42,7 @@ pub fn analyse_formulae( ); let modified_tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?; - let num_hctl_vars = collect_unique_hctl_vars(modified_tree.clone(), HashSet::new()).len(); + let num_hctl_vars = collect_unique_hctl_vars(modified_tree.clone()).len(); print_if_allowed( format!("Modified version: {}", modified_tree.subform_str), print_op, @@ -86,7 +86,7 @@ pub fn analyse_formulae( print_if_allowed("-----".to_string(), print_op); // find duplicate sub-formulae throughout all formulae + initiate caching structures - let mut eval_info = EvalInfo::from_multiple_trees(&parsed_trees); + let mut eval_info = EvalContext::from_multiple_trees(&parsed_trees); print_if_allowed( format!( "Found following duplicate sub-formulae (canonized): {:?}", @@ -153,14 +153,13 @@ pub fn analyse_formula( #[cfg(test)] mod tests { - use crate::analysis::analyse_formulae; + use crate::analysis::{analyse_formula, analyse_formulae}; use crate::result_print::PrintOptions; use biodivine_lib_param_bn::BooleanNetwork; #[test] /// Simple test to check whether the whole analysis runs without an error. fn test_analysis_run() { - let formulae = vec!["!{x}: AG EF {x}".to_string(), "!{x}: AF {x}".to_string()]; let model = r" $frs2:(!erk & fgfr) fgfr -> frs2 @@ -176,6 +175,10 @@ mod tests { "; let bn = BooleanNetwork::try_from(model).unwrap(); + let formulae = vec!["!{x}: AG EF {x}".to_string(), "!{x}: AF {x}".to_string()]; assert!(analyse_formulae(&bn, formulae, PrintOptions::WithProgress).is_ok()); + + let formula = "erk & fgfr & frs2 & ~shc".to_string(); // simple to avoid long prints + assert!(analyse_formula(&bn, formula, PrintOptions::Exhaustive).is_ok()); } } diff --git a/src/evaluation/algorithm.rs b/src/evaluation/algorithm.rs index fb9534b..756da59 100644 --- a/src/evaluation/algorithm.rs +++ b/src/evaluation/algorithm.rs @@ -2,7 +2,7 @@ use crate::aeon::scc_computation::compute_attractor_states; use crate::evaluation::canonization::get_canonical_and_mapping; -use crate::evaluation::eval_info::EvalInfo; +use crate::evaluation::eval_context::EvalContext; use crate::evaluation::hctl_operators_evaluation::*; use crate::evaluation::low_level_operations::substitute_hctl_var; use crate::preprocessing::node::{HctlTreeNode, NodeType}; @@ -20,7 +20,7 @@ use std::collections::HashMap; pub fn eval_node( node: HctlTreeNode, graph: &SymbolicAsyncGraph, - eval_info: &mut EvalInfo, + eval_info: &mut EvalContext, steady_states: &GraphColoredVertices, ) -> GraphColoredVertices { // first check whether this node does not belong in the duplicates @@ -89,6 +89,8 @@ pub fn eval_node( Atomic::False => graph.mk_empty_vertices(), Atomic::Var(name) => eval_hctl_var(graph, name.as_str()), Atomic::Prop(name) => eval_prop(graph, &name), + // should not be reachable, as wild-card nodes are always evaluated earlier using cache + Atomic::WildCardProp(_) => unreachable!(), }, NodeType::UnaryNode(op, child) => match op { UnaryOp::Not => eval_neg(graph, &eval_node(*child, graph, eval_info, steady_states)), @@ -269,8 +271,8 @@ mod tests { #[test] /// Test recognition of fixed-point pattern. fn test_fixed_point_pattern() { - let tree = create_hybrid( - create_unary(create_var_node("x".to_string()), UnaryOp::Ax), + let tree = HctlTreeNode::mk_hybrid_node( + HctlTreeNode::mk_unary_node(HctlTreeNode::mk_var_node("x".to_string()), UnaryOp::Ax), "x".to_string(), HybridOp::Bind, ); @@ -280,9 +282,12 @@ mod tests { #[test] /// Test recognition of attractor pattern. fn test_attractor_pattern() { - let tree = create_hybrid( - create_unary( - create_unary(create_var_node("x".to_string()), UnaryOp::Ef), + let tree = HctlTreeNode::mk_hybrid_node( + HctlTreeNode::mk_unary_node( + HctlTreeNode::mk_unary_node( + HctlTreeNode::mk_var_node("x".to_string()), + UnaryOp::Ef, + ), UnaryOp::Ag, ), "x".to_string(), diff --git a/src/evaluation/eval_context.rs b/src/evaluation/eval_context.rs new file mode 100644 index 0000000..6662c52 --- /dev/null +++ b/src/evaluation/eval_context.rs @@ -0,0 +1,141 @@ +//! Contains the structure to hold useful data to speed-up the computation. + +use crate::evaluation::mark_duplicate_subform::{ + mark_duplicates_canonized_multiple, mark_duplicates_canonized_single, +}; +use crate::preprocessing::node::HctlTreeNode; + +use biodivine_lib_param_bn::symbolic_async_graph::GraphColoredVertices; + +use std::collections::HashMap; + +/// Struct holding information for efficient caching during the main computation. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct EvalContext { + /// Duplicate sub-formulae and their counter + pub duplicates: HashMap, + /// Cached sub-formulae and their result + corresponding mapping of variable renaming + pub cache: HashMap)>, +} + +impl EvalContext { + /// Instantiate the struct with precomputed duplicates and empty cache. + pub fn new(duplicates: HashMap) -> EvalContext { + EvalContext { + duplicates, + cache: HashMap::new(), + } + } + + /// Instantiate the struct with precomputed duplicates and empty cache. + pub fn from_single_tree(tree: &HctlTreeNode) -> EvalContext { + EvalContext { + duplicates: mark_duplicates_canonized_single(tree), + cache: HashMap::new(), + } + } + + /// Instantiate the struct with precomputed duplicates and empty cache. + pub fn from_multiple_trees(trees: &Vec) -> EvalContext { + EvalContext { + duplicates: mark_duplicates_canonized_multiple(trees), + cache: HashMap::new(), + } + } + + /// Get the duplicates field containing the sub-formulae and their counter. + pub fn get_duplicates(&self) -> HashMap { + self.duplicates.clone() + } + + /// Get the cache field containing the cached sub-formulae, their result and var renaming. + pub fn get_cache(&self) -> HashMap)> { + self.cache.clone() + } + + /// Extend the standard evaluation context with "pre-computed cache" regarding wild-card nodes. + pub fn extend_context_with_wild_cards( + &mut self, + substitution_context: HashMap, + ) { + // For each `wild-card proposition` in `substitution_context`, increment its duplicate + // counter. That way, the first occurrence will also be treated as duplicate and taken from + // cache directly. + for (prop_name, raw_set) in substitution_context.into_iter() { + // we dont have to compute canonical sub-formula, because there are no HCTL variables + let sub_formula = format!("%{}%", prop_name); + if self.duplicates.contains_key(sub_formula.as_str()) { + self.duplicates.insert( + sub_formula.clone(), + self.duplicates[sub_formula.as_str()] + 1, + ); + } else { + self.duplicates.insert(sub_formula.clone(), 1); + } + + // Add the raw sets directly to the cache to be used during evaluation. + // The mapping for var renaming is empty, because there are no HCTL vars. + self.cache.insert(sub_formula, (raw_set, HashMap::new())); + } + } +} + +#[cfg(test)] +mod tests { + use crate::evaluation::eval_context::EvalContext; + use crate::mc_utils::get_extended_symbolic_graph; + use crate::preprocessing::parser::{parse_extended_formula, parse_hctl_formula}; + + use biodivine_lib_param_bn::BooleanNetwork; + + use std::collections::HashMap; + + #[test] + /// Test equivalent ways to generate EvalContext object. + fn test_eval_context_creation() { + let formula = "!{x}: (AX {x} & AX {x})"; + let syntax_tree = parse_hctl_formula(formula).unwrap(); + + let expected_duplicates = HashMap::from([("(Ax {var0})".to_string(), 1)]); + let eval_info = EvalContext::new(expected_duplicates.clone()); + + assert_eq!(eval_info, EvalContext::from_single_tree(&syntax_tree)); + assert_eq!( + eval_info, + EvalContext::from_multiple_trees(&vec![syntax_tree]) + ); + assert_eq!(eval_info.get_duplicates(), expected_duplicates); + + // check that cache is always initially empty + assert!(eval_info.get_cache().is_empty()); + } + + #[test] + /// Test extension of the EvalContext with "pre-computed cache" regarding wild-card nodes. + fn test_eval_context_extension() { + // prepare placeholder BN and STG + let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + let stg = get_extended_symbolic_graph(&bn, 2).unwrap(); + + let formula = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%)"; + let syntax_tree = parse_extended_formula(formula).unwrap(); + let mut eval_info = EvalContext::from_single_tree(&syntax_tree); + + assert_eq!( + eval_info.get_duplicates(), + HashMap::from([("%subst%".to_string(), 1)]) + ); + assert_eq!(eval_info.get_cache(), HashMap::new()); + + let raw_set = stg.mk_unit_colored_vertices(); + let substitution_context = HashMap::from([("subst".to_string(), raw_set.clone())]); + eval_info.extend_context_with_wild_cards(substitution_context); + let expected_cache = HashMap::from([("%subst%".to_string(), (raw_set, HashMap::new()))]); + + assert_eq!( + eval_info.get_duplicates(), + HashMap::from([("%subst%".to_string(), 2)]) + ); + assert_eq!(eval_info.get_cache(), expected_cache); + } +} diff --git a/src/evaluation/eval_info.rs b/src/evaluation/eval_info.rs deleted file mode 100644 index dc2328a..0000000 --- a/src/evaluation/eval_info.rs +++ /dev/null @@ -1,70 +0,0 @@ -//! Contains the structure to hold useful data to speed-up the computation. - -use crate::evaluation::mark_duplicate_subform::{ - mark_duplicates_canonized_multiple, mark_duplicates_canonized_single, -}; -use crate::preprocessing::node::HctlTreeNode; - -use biodivine_lib_param_bn::symbolic_async_graph::GraphColoredVertices; - -use std::collections::HashMap; - -/// Struct holding information for efficient caching during the main computation. -#[derive(Clone, Debug, PartialEq, Eq)] -pub struct EvalInfo { - /// Duplicate sub-formulae and their counter - pub duplicates: HashMap, - /// Cached sub-formulae and their result + variable renaming mapping - pub cache: HashMap)>, -} - -impl EvalInfo { - /// Instantiate the struct with precomputed duplicates and empty cache. - pub fn new(duplicates: HashMap) -> EvalInfo { - EvalInfo { - duplicates, - cache: HashMap::new(), - } - } - - /// Instantiate the struct with precomputed duplicates and empty cache. - pub fn from_single_tree(tree: &HctlTreeNode) -> EvalInfo { - EvalInfo { - duplicates: mark_duplicates_canonized_single(tree), - cache: HashMap::new(), - } - } - - /// Instantiate the struct with precomputed duplicates and empty cache. - pub fn from_multiple_trees(trees: &Vec) -> EvalInfo { - EvalInfo { - duplicates: mark_duplicates_canonized_multiple(trees), - cache: HashMap::new(), - } - } - - pub fn get_duplicates(&self) -> HashMap { - self.duplicates.clone() - } -} - -#[cfg(test)] -mod tests { - use crate::evaluation::eval_info::EvalInfo; - use crate::preprocessing::parser::parse_hctl_formula; - use std::collections::HashMap; - - #[test] - /// Test equivalent ways to generate EvalInfo object. - fn test_eval_info_creation() { - let formula = "!{x}: (AX {x} & AX {x})".to_string(); - let syntax_tree = parse_hctl_formula(formula.as_str()).unwrap(); - - let expected_duplicates = HashMap::from([("(Ax {var0})".to_string(), 1)]); - let eval_info = EvalInfo::new(expected_duplicates.clone()); - - assert_eq!(eval_info, EvalInfo::from_single_tree(&syntax_tree)); - assert_eq!(eval_info, EvalInfo::from_multiple_trees(&vec![syntax_tree])); - assert_eq!(eval_info.get_duplicates(), expected_duplicates); - } -} diff --git a/src/evaluation/mark_duplicate_subform.rs b/src/evaluation/mark_duplicate_subform.rs index c24869f..3d12f82 100644 --- a/src/evaluation/mark_duplicate_subform.rs +++ b/src/evaluation/mark_duplicate_subform.rs @@ -4,13 +4,16 @@ use crate::evaluation::canonization::{get_canonical, get_canonical_and_mapping}; use crate::preprocessing::node::{HctlTreeNode, NodeType}; +use crate::preprocessing::operator_enums::Atomic; use std::collections::{BinaryHeap, HashMap, HashSet}; /// Check if there are some duplicate subtrees in a given formula syntax tree. /// This function uses canonization and thus recognizes duplicates with differently named /// variables (e.g., `AX {y}` and `AX {z}`). /// Return the CANONICAL versions of duplicate sub-formulae + the number of their appearances. -/// Note that terminal nodes (props, vars, constants) are not considered. +/// +/// Note that except for wild-card properties, most of the terminal nodes (props, vars, constants) +/// are not considered. pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> HashMap { // go through each tree from top, use height to compare only the nodes with the same level // once we find duplicate, do not continue traversing its branch (it will be skipped during eval) @@ -34,10 +37,13 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> Has // because we are traversing trees, we dont care about cycles while let Some(current_node) = heap_queue.pop() { - // lets stop the process when we hit the first terminal node - // terminals are not worth to mark as duplicates and use them for caching - if current_node.height == 0 { - break; + // if current node is terminal, process it only if it represents the `wild-card prop` + // other kinds of terminals are not worth to be considered and cached during eval + if let NodeType::TerminalNode(atom) = ¤t_node.node_type { + if let Atomic::WildCardProp(_) = atom { + } else { + continue; + } } let mut skip = false; @@ -45,6 +51,7 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> Has get_canonical_and_mapping(current_node.subform_str.clone()); // only mark duplicates with at max 1 variable (to not cause var name collisions during caching) + // todo: extend this for any number of variables if (last_height == current_node.height) & (renaming.len() <= 1) { // if we have saved some nodes of the same height, compare them with the current one for other_canonical_string in same_height_canonical_strings.clone() { @@ -62,13 +69,13 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> Has } } - // do not traverse subtree of the duplicate later (will be cached during eval) + // do not traverse subtree of the duplicate later (whole node is cached during eval) if skip { continue; } same_height_canonical_strings.insert(current_subform_canonical); } else { - // we got node from lower level, so we empty the set of nodes to compare + // we continue with node from lower level, so we empty the set of nodes to compare last_height = current_node.height; same_height_canonical_strings.clear(); same_height_canonical_strings.insert(get_canonical(current_node.subform_str.clone())); @@ -175,20 +182,22 @@ mod tests { use crate::evaluation::mark_duplicate_subform::{ mark_duplicates_canonized_multiple, mark_duplicates_canonized_single, }; - use crate::preprocessing::parser::parse_and_minimize_hctl_formula; + use crate::preprocessing::parser::{ + parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula, + }; use biodivine_lib_param_bn::BooleanNetwork; use std::collections::HashMap; #[test] /// Compare automatically detected duplicate sub-formulae to expected ones. fn test_duplicates_single_simple() { - let formula = "!{x}: 3{y}: (AX {x} & AX {y})".to_string(); + let formula = "!{x}: 3{y}: (AX {x} & AX {y})"; let expected_duplicates = HashMap::from([("(Ax {var0})".to_string(), 1)]); // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); - let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str()).unwrap(); + let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); let duplicates = mark_duplicates_canonized_single(&tree); assert_eq!(duplicates, expected_duplicates); @@ -197,8 +206,7 @@ mod tests { #[test] /// Compare automatically detected duplicate sub-formulae to expected ones. fn test_duplicates_single_complex() { - let formula = - "(!{x}: 3{y}: ((AG EF {x} & AG EF {y}) & (EF {y}))) & (!{z}: EF {z})".to_string(); + let formula = "(!{x}: 3{y}: ((AG EF {x} & AG EF {y}) & (EF {y}))) & (!{z}: EF {z})"; let expected_duplicates = HashMap::from([ ("(Ag (Ef {var0}))".to_string(), 1), ("(Ef {var0})".to_string(), 2), @@ -207,7 +215,7 @@ mod tests { // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); - let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str()).unwrap(); + let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); let duplicates = mark_duplicates_canonized_single(&tree); assert_eq!(duplicates, expected_duplicates); } @@ -217,9 +225,9 @@ mod tests { /// Use multiple input formulae. fn test_duplicates_multiple() { let formulae = vec![ - "!{x}: 3{y}: (AX {x} & AX {y})".to_string(), - "!{x}: (AX {x})".to_string(), - "!{z}: AX {z}".to_string(), + "!{x}: 3{y}: (AX {x} & AX {y})", + "!{x}: (AX {x})", + "!{z}: AX {z}", ]; let expected_duplicates = HashMap::from([ ("(Ax {var0})".to_string(), 2), @@ -231,11 +239,25 @@ mod tests { let mut trees = Vec::new(); for formula in formulae { - let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str()).unwrap(); + let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); trees.push(tree); } let duplicates = mark_duplicates_canonized_multiple(&trees); assert_eq!(duplicates, expected_duplicates); } + + #[test] + /// Test that wild-card propositions are also detected correctly (opposed to other terminals). + fn test_duplicates_wild_cards() { + // define a placeholder bn + let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + + let formula = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%) & v1 & v1"; + let expected_duplicates = HashMap::from([("%subst%".to_string(), 1)]); + + let tree = parse_and_minimize_extended_formula(&bn, formula).unwrap(); + let duplicates = mark_duplicates_canonized_single(&tree); + assert_eq!(duplicates, expected_duplicates); + } } diff --git a/src/evaluation/mod.rs b/src/evaluation/mod.rs index e69c410..9f077ef 100644 --- a/src/evaluation/mod.rs +++ b/src/evaluation/mod.rs @@ -1,7 +1,7 @@ //! Components regarding the evaluation of formulae, including the main model-checking algorithm. pub mod algorithm; -pub mod eval_info; +pub mod eval_context; pub mod mark_duplicate_subform; mod canonization; diff --git a/src/lib.rs b/src/lib.rs index c9c2c9c..9df3d74 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,9 +1,11 @@ //! A small library regarding analysis of dynamic properties of Boolean networks through HCTL model checking. //! As of now, the library supports: -//! - Overall symbolic model-checking analysis of multiple HCTL formulae on a given model at once. -//! - Manipulation with HCTL formulae, such as tokenizing, parsing, or canonization. -//! - Searching for common sub-formulae across multiple formulae. +//! - Model-checking analysis of HCTL properties on a (partially specified) BNs. +//! - Various formulae preprocessing utilities, such as tokenizing, parsing, or some canonization. +//! - Manipulation with abstract syntactic trees for HCTL formulae. +//! - Searching for common sub-formulae across multiple properties. //! - Optimised evaluation for several patterns, such as various attractor types or reachability. +//! - Simultaneous evaluation of several formulae, sharing common computation via cache. //! pub mod analysis; diff --git a/src/mc_utils.rs b/src/mc_utils.rs index 734ed68..110c259 100644 --- a/src/mc_utils.rs +++ b/src/mc_utils.rs @@ -1,7 +1,7 @@ //! Model checking utilities such as generating extended STG or checking STG for variable support. use crate::preprocessing::node::{HctlTreeNode, NodeType}; -use crate::preprocessing::operator_enums::HybridOp; +use crate::preprocessing::operator_enums::{Atomic, HybridOp}; use biodivine_lib_param_bn::symbolic_async_graph::{SymbolicAsyncGraph, SymbolicContext}; use biodivine_lib_param_bn::BooleanNetwork; @@ -27,18 +27,28 @@ pub fn get_extended_symbolic_graph( /// Compute the set of all uniquely named HCTL variables in the formula tree. /// Variable names are collected from three quantifiers: bind, exists, forall (which is sufficient, /// as the formula must not contain free variables). -pub fn collect_unique_hctl_vars( +pub fn collect_unique_hctl_vars(formula_tree: HctlTreeNode) -> HashSet { + collect_unique_hctl_vars_recursive(formula_tree, HashSet::new()) +} + +fn collect_unique_hctl_vars_recursive( formula_tree: HctlTreeNode, mut seen_vars: HashSet, ) -> HashSet { match formula_tree.node_type { NodeType::TerminalNode(_) => {} NodeType::UnaryNode(_, child) => { - seen_vars.extend(collect_unique_hctl_vars(*child, seen_vars.clone())); + seen_vars.extend(collect_unique_hctl_vars_recursive( + *child, + seen_vars.clone(), + )); } NodeType::BinaryNode(_, left, right) => { - seen_vars.extend(collect_unique_hctl_vars(*left, seen_vars.clone())); - seen_vars.extend(collect_unique_hctl_vars(*right, seen_vars.clone())); + seen_vars.extend(collect_unique_hctl_vars_recursive(*left, seen_vars.clone())); + seen_vars.extend(collect_unique_hctl_vars_recursive( + *right, + seen_vars.clone(), + )); } // collect variables from exist and binder nodes NodeType::HybridNode(op, var_name, child) => { @@ -48,15 +58,61 @@ pub fn collect_unique_hctl_vars( } _ => {} } - seen_vars.extend(collect_unique_hctl_vars(*child, seen_vars.clone())); + seen_vars.extend(collect_unique_hctl_vars_recursive( + *child, + seen_vars.clone(), + )); } } seen_vars } -/// Check that extended symbolic graph's BDD supports enough extra variables for the computation. +/// Compute the set of all uniquely named `wild-card propositions` in the formula tree. +pub fn collect_unique_wild_card_props(formula_tree: HctlTreeNode) -> HashSet { + collect_unique_wild_card_props_recursive(formula_tree, HashSet::new()) +} + +fn collect_unique_wild_card_props_recursive( + formula_tree: HctlTreeNode, + mut seen_props: HashSet, +) -> HashSet { + match formula_tree.node_type { + NodeType::TerminalNode(atom) => { + if let Atomic::WildCardProp(prop_name) = atom { + seen_props.insert(prop_name); + } + } + NodeType::UnaryNode(_, child) => { + seen_props.extend(collect_unique_wild_card_props_recursive( + *child, + seen_props.clone(), + )); + } + NodeType::BinaryNode(_, left, right) => { + seen_props.extend(collect_unique_wild_card_props_recursive( + *left, + seen_props.clone(), + )); + seen_props.extend(collect_unique_wild_card_props_recursive( + *right, + seen_props.clone(), + )); + } + NodeType::HybridNode(_, _, child) => { + seen_props.extend(collect_unique_wild_card_props_recursive( + *child, + seen_props.clone(), + )); + } + } + seen_props +} + +/// Check that extended symbolic graph's BDD supports enough extra variables for the evaluation of +/// the formula given by a `hctl_syntactic_tree`. /// There must be `num_hctl_vars` extra symbolic BDD vars for each BN variable. -pub fn check_hctl_var_support(stg: &SymbolicAsyncGraph, num_hctl_vars: usize) -> bool { +pub fn check_hctl_var_support(stg: &SymbolicAsyncGraph, hctl_syntactic_tree: HctlTreeNode) -> bool { + let num_hctl_vars = collect_unique_hctl_vars(hctl_syntactic_tree).len(); for bn_var in stg.as_network().variables() { if num_hctl_vars > stg.symbolic_context().extra_state_variables(bn_var).len() { return false; @@ -64,3 +120,78 @@ pub fn check_hctl_var_support(stg: &SymbolicAsyncGraph, num_hctl_vars: usize) -> } true } + +#[cfg(test)] +mod tests { + use crate::mc_utils::{ + check_hctl_var_support, collect_unique_hctl_vars, collect_unique_wild_card_props, + get_extended_symbolic_graph, + }; + use crate::preprocessing::parser::{ + parse_and_minimize_hctl_formula, parse_extended_formula, parse_hctl_formula, + }; + use crate::preprocessing::utils::check_props_and_rename_vars; + + use biodivine_lib_param_bn::BooleanNetwork; + + use std::collections::{HashMap, HashSet}; + + #[test] + /// Test collecting state vars from HCTL formulae. + fn test_state_var_collecting() { + // conjunction of 2 formulae which are semantically same, just use different var names + let formula = "(!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))) & (!{x1}: 3{y1}: (@{x1}: ~{y1} & (!{z1}: AX {z1})) & (@{y1}: (!{z1}: AX {z1})))"; + let tree = parse_hctl_formula(formula).unwrap(); + + // test for original tree + let expected_vars = HashSet::from_iter(vec![ + "x".to_string(), + "y".to_string(), + "z".to_string(), + "x1".to_string(), + "y1".to_string(), + "z1".to_string(), + ]); + assert_eq!(collect_unique_hctl_vars(tree.clone()), expected_vars); + + // define any placeholder bn + let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + + // and for tree with minimized number of renamed state vars + let modified_tree = + check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).unwrap(); + let expected_vars = + HashSet::from_iter(vec!["x".to_string(), "xx".to_string(), "xxx".to_string()]); + assert_eq!(collect_unique_hctl_vars(modified_tree), expected_vars); + } + + #[test] + /// Test collecting wild-card propositions from extended HCTL formulae. + fn test_wild_card_prop_collecting() { + let formula = "!{x}: 3{y}: (@{x}: ~{y} & %A% & %B%) & (@{y}: %A% & %C%)"; + let tree = parse_extended_formula(formula).unwrap(); + + let expected_vars = + HashSet::from_iter(vec!["A".to_string(), "B".to_string(), "C".to_string()]); + assert_eq!(collect_unique_wild_card_props(tree.clone()), expected_vars); + } + + #[test] + /// Test collecting wild-card propositions from extended HCTL formulae. + fn test_check_hctl_var_support() { + // define any placeholder bn and stg with enough variables + let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + + // formula with 3 variables + let formula = "!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))"; + let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); + + // the stg that supports the same amount variables as the formula (3) + let stg = get_extended_symbolic_graph(&bn, 3).unwrap(); + assert!(check_hctl_var_support(&stg, tree.clone())); + + // the stg that supports less variables than the formula (1 vs 3) + let stg = get_extended_symbolic_graph(&bn, 1).unwrap(); + assert!(!check_hctl_var_support(&stg, tree)); + } +} diff --git a/src/model_checking.rs b/src/model_checking.rs index 3d01387..0aedf21 100644 --- a/src/model_checking.rs +++ b/src/model_checking.rs @@ -1,34 +1,43 @@ //! High-level functionality regarding the whole model-checking process. +//! Several variants of the model-checking procedure are provided: +//! - variants for both single or multiple formulae +//! - variants for formulae given by a string or a syntactic tree +//! - `dirty` variants that do not sanitize the resulting BDDs (and thus, the BDDs retain additional vars) +//! - variants allowing `extended` HCTL with special propositions referencing raw sets +//! - variants using potentially unsafe optimizations, targeted for specific use cases use crate::evaluation::algorithm::{compute_steady_states, eval_node}; -use crate::evaluation::eval_info::EvalInfo; +use crate::evaluation::eval_context::EvalContext; use crate::mc_utils::*; use crate::postprocessing::sanitizing::sanitize_colored_vertices; use crate::preprocessing::node::HctlTreeNode; -use crate::preprocessing::parser::parse_and_minimize_hctl_formula; +use crate::preprocessing::parser::{ + parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula, +}; use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph}; -use std::collections::HashSet; +use std::collections::HashMap; -/// Perform the model checking for the list of HCTL syntax trees on GIVEN graph. +/// Perform the model checking for the list of HCTL syntax trees on a given transition `graph`. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. /// Return the list of resulting sets of colored vertices (in the same order as input formulae). -/// There MUST be enough symbolic variables to represent HCTL vars. -/// Does not sanitize the resulting BDDs. +/// +/// This version does not sanitize the resulting BDDs (`model_check_multiple_trees` does). pub fn model_check_multiple_trees_dirty( formula_trees: Vec, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result, String> { // find duplicate sub-formulae throughout all formulae + initiate caching structures - let mut eval_info = EvalInfo::from_multiple_trees(&formula_trees); - // compute states with self-loops which will be needed, and add them to graph object - let self_loop_states = compute_steady_states(stg); + let mut eval_info = EvalContext::from_multiple_trees(&formula_trees); + // pre-compute states with self-loops which will be needed during eval + let self_loop_states = compute_steady_states(graph); // evaluate the formulae (perform the actual model checking) and collect results let mut results: Vec = Vec::new(); for parse_tree in formula_trees { results.push(eval_node( parse_tree, - stg, + graph, &mut eval_info, &self_loop_states, )); @@ -36,146 +45,225 @@ pub fn model_check_multiple_trees_dirty( Ok(results) } -/// Perform the model checking for the list of HCTL syntax trees on GIVEN graph. +/// Perform the model checking for the syntactic tree, but do not sanitize the results. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. +pub fn model_check_tree_dirty( + formula_tree: HctlTreeNode, + graph: &SymbolicAsyncGraph, +) -> Result { + let result = model_check_multiple_trees_dirty(vec![formula_tree], graph)?; + Ok(result[0].clone()) +} + +/// Perform the model checking for the list of HCTL syntax trees on a given transition `graph`. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. /// Return the list of resulting sets of colored vertices (in the same order as input formulae). -/// There MUST be enough symbolic variables to represent HCTL vars. -pub fn model_check_trees( +pub fn model_check_multiple_trees( formula_trees: Vec, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result, String> { // evaluate the formulae and collect results - let results = model_check_multiple_trees_dirty(formula_trees, stg)?; + let results = model_check_multiple_trees_dirty(formula_trees, graph)?; // sanitize the results' bdds - get rid of additional bdd vars used for HCTL vars let sanitized_results: Vec = results .iter() - .map(|x| sanitize_colored_vertices(stg, x)) + .map(|x| sanitize_colored_vertices(graph, x)) .collect(); Ok(sanitized_results) } -/// Perform the model checking for a given HCTL syntax tree on GIVEN graph. +/// Perform the model checking for a given HCTL formula's syntax tree on a given transition `graph`. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. /// Return the resulting set of colored vertices. -/// There MUST be enough symbolic variables to represent all needed HCTL vars. pub fn model_check_tree( formula_tree: HctlTreeNode, - stg: &SymbolicAsyncGraph, -) -> Result { - let result = model_check_trees(vec![formula_tree], stg)?; - Ok(result[0].clone()) -} - -/// Perform the model checking for the syntactic tree, but do not sanitize the results. -pub fn model_check_tree_dirty( - formula_tree: HctlTreeNode, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result { - let result = model_check_multiple_trees_dirty(vec![formula_tree], stg)?; + let result = model_check_multiple_trees(vec![formula_tree], graph)?; Ok(result[0].clone()) } -fn parse_into_trees( +/// Parse given HCTL formulae into syntactic trees and perform compatibility check with +/// the provided `graph` (i.e., check if `graph` object supports enough symbolic variables). +fn parse_hctl_and_validate( formulae: Vec, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result, String> { - // first parse all the formulae and check that graph supports enough HCTL vars + // parse all the formulae and check that graph supports enough HCTL vars let mut parsed_trees = Vec::new(); for formula in formulae { - let tree = parse_and_minimize_hctl_formula(stg.as_network(), formula.as_str())?; - + let tree = parse_and_minimize_hctl_formula(graph.as_network(), formula.as_str())?; // check that given extended symbolic graph supports enough stated variables - let num_vars_formula = collect_unique_hctl_vars(tree.clone(), HashSet::new()).len(); - if !check_hctl_var_support(stg, num_vars_formula) { + if !check_hctl_var_support(graph, tree.clone()) { return Err("Graph does not support enough HCTL state variables".to_string()); } - parsed_trees.push(tree); } Ok(parsed_trees) } -/// Perform the model checking for the list of formulae on GIVEN graph and return the list -/// of resulting sets of colored vertices (in the same order as input formulae). -/// Return Error if the given extended symbolic graph does not support enough extra BDD variables to -/// represent all needed HCTL state-variables or if some formula is badly formed. +/// Perform the model checking for the list of HCTL formulae on a given transition `graph`. +/// Return the resulting sets of colored vertices (in the same order as input formulae). +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. pub fn model_check_multiple_formulae( formulae: Vec, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result, String> { // get the abstract syntactic trees - let parsed_trees = parse_into_trees(formulae, stg)?; + let parsed_trees = parse_hctl_and_validate(formulae, graph)?; // run the main model-checking procedure on formulae trees - model_check_trees(parsed_trees, stg) + model_check_multiple_trees(parsed_trees, graph) } /// Perform the model checking for the list of formulae, but do not sanitize the results. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. pub fn model_check_multiple_formulae_dirty( formulae: Vec, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result, String> { // get the abstract syntactic trees - let parsed_trees = parse_into_trees(formulae, stg)?; + let parsed_trees = parse_hctl_and_validate(formulae, graph)?; // run the main model-checking procedure on formulae trees - model_check_multiple_trees_dirty(parsed_trees, stg) + model_check_multiple_trees_dirty(parsed_trees, graph) } -/// Perform the model checking for given formula on GIVEN graph and return the resulting -/// set of colored vertices. -/// Return Error if the given extended symbolic graph does not support enough extra BDD variables -/// to represent all needed HCTL state-variables or if the formula is badly formed. +/// Perform the model checking for a given HCTL formula on a given transition `graph`. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. +/// Return the resulting set of colored vertices. pub fn model_check_formula( formula: String, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result { - let result = model_check_multiple_formulae(vec![formula], stg)?; + let result = model_check_multiple_formulae(vec![formula], graph)?; Ok(result[0].clone()) } /// Perform the model checking for given formula, but do not sanitize the result. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. pub fn model_check_formula_dirty( formula: String, - stg: &SymbolicAsyncGraph, + graph: &SymbolicAsyncGraph, ) -> Result { - let result = model_check_multiple_formulae_dirty(vec![formula], stg)?; + let result = model_check_multiple_formulae_dirty(vec![formula], graph)?; Ok(result[0].clone()) } -#[allow(dead_code)] -/// Perform the model checking on GIVEN graph and return the resulting set of colored vertices. -/// Self-loops are not pre-computed, and thus are ignored in EX computation, which is fine for -/// some formulae, but incorrect for others - it is thus an UNSAFE optimisation - only use it -/// if you are sure everything will work fine. -/// This must NOT be used for formulae containing `!{x}:AX{x}` sub-formulae. -/// Also, does not sanitize results. -pub fn model_check_formula_unsafe_ex( +/// Parse given extended HCTL formulae into syntactic trees and perform compatibility check with +/// the provided `graph` (i.e., check if `graph` object supports enough symbolic variables). +fn parse_extended_and_validate( + formulae: Vec, + graph: &SymbolicAsyncGraph, + substitution_context: &HashMap, +) -> Result, String> { + // parse all the formulae and check that graph supports enough HCTL vars + let mut parsed_trees = Vec::new(); + for formula in formulae { + let tree = parse_and_minimize_extended_formula(graph.as_network(), formula.as_str())?; + + // check that given extended symbolic graph supports enough stated variables + if !check_hctl_var_support(graph, tree.clone()) { + return Err("Graph does not support enough HCTL state variables".to_string()); + } + // check that all occurring wild-card propositions are present in `substitution_context` + for wild_card_prop in collect_unique_wild_card_props(tree.clone()) { + if !substitution_context.contains_key(wild_card_prop.as_str()) { + return Err(format!( + "Wild-card proposition `{}` lacks evaluation context.", + wild_card_prop + )); + } + } + parsed_trees.push(tree); + } + Ok(parsed_trees) +} + +/// Perform the model checking for list of `extended` HCTL formulae on a given transition `graph`. +/// Return the resulting sets of colored vertices (in the same order as input formulae). +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. +/// +/// The `substitution context` is a mapping determining how `wild-card propositions` are evaluated. +pub fn model_check_multiple_extended_formulae( + formulae: Vec, + stg: &SymbolicAsyncGraph, + substitution_context: HashMap, +) -> Result, String> { + // get the abstract syntactic trees and check compatibility with graph + let parsed_trees = parse_extended_and_validate(formulae, stg, &substitution_context)?; + + // prepare the extended evaluation context + + // 1) find normal duplicate sub-formulae throughout all formulae + initiate caching structures + let mut eval_info = EvalContext::from_multiple_trees(&parsed_trees); + // 2) extended the cache with given substitution context for wild-card nodes + eval_info.extend_context_with_wild_cards(substitution_context); + // 3) pre-compute compute states with self-loops which will be needed during eval + let self_loop_states = compute_steady_states(stg); + + // evaluate the formulae (perform the actual model checking) and collect results + let mut results: Vec = Vec::new(); + for parse_tree in parsed_trees { + results.push(eval_node( + parse_tree, + stg, + &mut eval_info, + &self_loop_states, + )); + } + + // sanitize the results' bdds - get rid of additional bdd vars used for HCTL vars + let sanitized_results: Vec = results + .iter() + .map(|x| sanitize_colored_vertices(stg, x)) + .collect(); + Ok(sanitized_results) +} + +/// Perform the model checking for a given `extended` HCTL formula on a given transition `graph`. +/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars. +/// +/// The `substitution context` is a mapping determining how `wild-card propositions` are evaluated. +pub fn model_check_extended_formula( formula: String, stg: &SymbolicAsyncGraph, + substitution_context: HashMap, ) -> Result { - let tree = parse_and_minimize_hctl_formula(stg.as_network(), formula.as_str())?; - // check that given extended symbolic graph supports enough stated variables - let num_vars_formula = collect_unique_hctl_vars(tree.clone(), HashSet::new()).len(); - if !check_hctl_var_support(stg, num_vars_formula) { - return Err("Graph does not support enough HCTL state variables".to_string()); - } + let result = model_check_multiple_extended_formulae(vec![formula], stg, substitution_context)?; + Ok(result[0].clone()) +} - let mut eval_info = EvalInfo::from_single_tree(&tree); +/// Model check HCTL `formula` on a given transition `graph`. +/// This version does not compute with self-loops. They are thus ignored in EX computation, which +/// might fine for some formulae, but can be incorrect for others. It is an UNSAFE optimisation, +/// only use it if you are sure everything will work fine. +/// This function must NOT be used for formulae containing `!{x}:AX{x}` sub-formulae. +/// +/// Also, this does not sanitize results. +pub fn model_check_formula_unsafe_ex( + formula: String, + graph: &SymbolicAsyncGraph, +) -> Result { + let tree = parse_hctl_and_validate(vec![formula], graph)?[0].clone(); + let mut eval_info = EvalContext::from_single_tree(&tree); // do not consider self-loops during EX computation (UNSAFE optimisation) - let result = eval_node(tree, stg, &mut eval_info, &stg.mk_empty_vertices()); + let result = eval_node(tree, graph, &mut eval_info, &graph.mk_empty_vertices()); Ok(result) } #[cfg(test)] mod tests { - use crate::mc_utils::{collect_unique_hctl_vars, get_extended_symbolic_graph}; - use crate::model_checking::{model_check_formula, model_check_formula_dirty}; - use crate::preprocessing::parser::parse_hctl_formula; - use crate::preprocessing::utils::check_props_and_rename_vars; - + use crate::mc_utils::get_extended_symbolic_graph; + use crate::model_checking::{ + model_check_extended_formula, model_check_formula, model_check_formula_dirty, + model_check_formula_unsafe_ex, parse_extended_and_validate, + }; + use std::collections::HashMap; + + use crate::postprocessing::sanitizing::sanitize_colored_vertices; use biodivine_lib_param_bn::BooleanNetwork; - use std::collections::{HashMap, HashSet}; - // model FISSION-YEAST-2008 const MODEL_FISSION_YEAST: &str = r" targets,factors @@ -333,6 +421,11 @@ $DivK: (!PleC & DivJ) "(~(!{x}:AG EF{x})) AU (!{x}:AG EF{x})", "~EG~(!{x}:AG EF{x}) & ~(~(!{x}:AG EF{x}) EU (~(!{x}:AG EF{x}) & (!{x}:AG EF{x})))", ), + // AU equivalence (where phi1 are fixed points, and phi2 the rest) + ( + "(~(!{x}:AX{x})) AU (!{x}:AX{x})", + "~EG~(!{x}:AX{x}) & ~(~(!{x}:AX{x}) EU (~(!{x}:AX{x}) & (!{x}:AX{x})))", + ), // formulae for attractors, one is evaluated directly through optimisation ("!{x}: AG EF {x}", "!{x}: AG EF ({x} & {x})"), // formulae for fixed-points, one is evaluated directly through optimisation @@ -447,36 +540,128 @@ $DivK: (!PleC & DivJ) } #[test] - /// Test regarding collecting state vars from HCTL formulae. - fn test_state_var_collecting() { - // formula "FORKS1 & FORKS2" - both parts are semantically same, just use different var names - let formula = "(!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))) & (!{x1}: 3{y1}: (@{x1}: ~{y1} & (!{z1}: AX {z1})) & (@{y1}: (!{z1}: AX {z1})))".to_string(); - let tree = parse_hctl_formula(formula.as_str()).unwrap(); - - // test for original tree - let expected_vars = vec![ - "x".to_string(), - "y".to_string(), - "z".to_string(), - "x1".to_string(), - "y1".to_string(), - "z1".to_string(), - ]; - assert_eq!( - collect_unique_hctl_vars(tree.clone(), HashSet::new()), - HashSet::from_iter(expected_vars) - ); + /// Test evaluation of (very simple) extended formulae, where special propositions are + /// evaluated as various simple pre-computed sets. + fn test_model_check_extended_formulae_simple() { + let bn = BooleanNetwork::try_from(MODEL_ASYMMETRIC_CELL_DIVISION).unwrap(); + let stg = get_extended_symbolic_graph(&bn, 1).unwrap(); - // define any placeholder bn - let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + // 1) first test, only proposition substituted + let formula_v1 = "PleC & EF PleC".to_string(); + let sub_formula = "PleC".to_string(); + let formula_v2 = "%s% & EF %s%".to_string(); + + let result_v1 = model_check_formula(formula_v1, &stg).unwrap(); + // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars) + let result_sub = model_check_formula_dirty(sub_formula, &stg).unwrap(); + let context = HashMap::from([("s".to_string(), result_sub)]); + let result_v2 = model_check_extended_formula(formula_v2, &stg, context).unwrap(); + assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true()); + + // 2) second test, disjunction substituted + let formula_v1 = "EX (PleC | DivK)".to_string(); + let sub_formula = "PleC | DivK".to_string(); + let formula_v2 = "EX %s%".to_string(); + + let result_v1 = model_check_formula(formula_v1, &stg).unwrap(); + // use 'dirty' version to avoid sanitation (for BDD to retain all symbolic vars) + let result_sub = model_check_formula_dirty(sub_formula, &stg).unwrap(); + let context = HashMap::from([("s".to_string(), result_sub)]); + let result_v2 = model_check_extended_formula(formula_v2, &stg, context).unwrap(); + assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true()); + } + + /// Test evaluation of extended HCTL formulae, in which `wild-card properties` can + /// represent already pre-computed results. + fn test_model_check_extended_formulae(bn: BooleanNetwork) { + // test formulae use 3 HCTL vars at most + let stg = get_extended_symbolic_graph(&bn, 3).unwrap(); + + // the test is conducted on two different formulae + + // first define and evaluate the two formulae normally in one step + let formula1 = "!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))"; + let formula2 = "3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & (!{z}: AX {z})) & EF ({y} & (!{z}: AX {z})) & AX (EF ({x} & (!{z}: AX {z})) ^ EF ({y} & (!{z}: AX {z})))"; + let result1 = model_check_formula(formula1.to_string(), &stg).unwrap(); + let result2 = model_check_formula(formula2.to_string(), &stg).unwrap(); + + // now precompute part of the formula, and then substitute it as `wild-card proposition` + let substitution_formula = "(!{z}: AX {z})"; + // we must use 'dirty' version to avoid sanitation (BDDs must retain all symbolic vars) + let raw_set = model_check_formula_dirty(substitution_formula.to_string(), &stg).unwrap(); + let context = HashMap::from([("subst".to_string(), raw_set)]); + + let formula1_v2 = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%)"; + let formula2_v2 = "3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & %subst%) & EF ({y} & %subst%) & AX (EF ({x} & %subst%) ^ EF ({y} & %subst%))"; + let result1_v2 = + model_check_extended_formula(formula1_v2.to_string(), &stg, context.clone()).unwrap(); + let result2_v2 = + model_check_extended_formula(formula2_v2.to_string(), &stg, context).unwrap(); + + assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true()); + assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true()); + + // also double check that running "extended" evaluation on the original formula (without + // wild-card propositions) is the same as running the standard variant + let result1_v2 = + model_check_extended_formula(formula1.to_string(), &stg, HashMap::new()).unwrap(); + let result2_v2 = + model_check_extended_formula(formula2.to_string(), &stg, HashMap::new()).unwrap(); + assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true()); + assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true()); + } + + #[test] + /// Test evaluation of extended HCTL formulae, in which `wild-card properties` can + /// represent already pre-computed results. Use all 3 pre-defined models. + fn test_model_check_extended_all_models() { + let bn1 = BooleanNetwork::try_from(MODEL_ASYMMETRIC_CELL_DIVISION).unwrap(); + let bn2 = BooleanNetwork::try_from_bnet(MODEL_MAMMALIAN_CELL_CYCLE).unwrap(); + let bn3 = BooleanNetwork::try_from_bnet(MODEL_FISSION_YEAST).unwrap(); + + test_model_check_extended_formulae(bn1); + test_model_check_extended_formulae(bn2); + test_model_check_extended_formulae(bn3); + } + + #[test] + /// Test that the (potentially unsafe) optimization works on several formulae where it + /// should be applicable without any loss of information. + fn test_model_check_unsafe_version() { + let bn1 = BooleanNetwork::try_from(MODEL_ASYMMETRIC_CELL_DIVISION).unwrap(); + let bn2 = BooleanNetwork::try_from_bnet(MODEL_MAMMALIAN_CELL_CYCLE).unwrap(); + let bn3 = BooleanNetwork::try_from_bnet(MODEL_FISSION_YEAST).unwrap(); + let bns = vec![bn1, bn2, bn3]; + + for bn in bns { + let stg = get_extended_symbolic_graph(&bn, 3).unwrap(); + // use formula for attractors that won't be recognized as the "attractor pattern" + let formula = "!{x}: AG EF ({x} & {x})".to_string(); + let result1 = model_check_formula(formula.clone(), &stg).unwrap(); + // result of the unsafe eval must be sanitized + let result2 = sanitize_colored_vertices( + &stg, + &model_check_formula_unsafe_ex(formula.clone(), &stg).unwrap(), + ); + assert!(result1.as_bdd().iff(result2.as_bdd()).is_true()); + } + } + + #[test] + /// Test that the helper function for parsing and validating extended formulae properly + /// discovers errors. + fn test_validation_extended_context() { + let bn = BooleanNetwork::try_from(MODEL_ASYMMETRIC_CELL_DIVISION).unwrap(); + let stg = get_extended_symbolic_graph(&bn, 1).unwrap(); - // and for tree with minimized number of renamed state vars - let modified_tree = - check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).unwrap(); - let expected_vars = vec!["x".to_string(), "xx".to_string(), "xxx".to_string()]; + // test situation where one substitution is missing + let sub_context = HashMap::from([("s".to_string(), stg.mk_empty_vertices())]); + let formula = "%s% & EF %t%".to_string(); + let res = parse_extended_and_validate(vec![formula], &stg, &sub_context); + assert!(res.is_err()); assert_eq!( - collect_unique_hctl_vars(modified_tree, HashSet::new()), - HashSet::from_iter(expected_vars) + res.err().unwrap(), + "Wild-card proposition `t` lacks evaluation context.".to_string() ); } } diff --git a/src/preprocessing/node.rs b/src/preprocessing/node.rs index 33da9ab..2aa2209 100644 --- a/src/preprocessing/node.rs +++ b/src/preprocessing/node.rs @@ -1,6 +1,8 @@ //! Contains a syntax tree struct for HCTL formulae and functionality regarding the manipulation with it. use crate::preprocessing::operator_enums::*; +use crate::preprocessing::parser::parse_hctl_tokens; +use crate::preprocessing::tokenizer::HctlToken; use std::cmp; use std::cmp::Ordering; @@ -49,88 +51,120 @@ impl Ord for HctlTreeNode { } } -impl Default for HctlTreeNode { - fn default() -> Self { - Self::new() +impl HctlTreeNode { + /// Parse `tokens` of HCTL formula into an abstract syntax tree using recursive steps. + /// It is recommended to not use this method for parsing, but rather choose from functions + /// provided in `preprocessing::parser` module. + pub fn new(tokens: &[HctlToken]) -> Result { + parse_hctl_tokens(tokens) } -} -impl HctlTreeNode { - /// Create a default node - the `True` constant (terminal) node. - pub fn new() -> Self { - Self { - subform_str: "True".to_string(), - height: 0, - node_type: NodeType::TerminalNode(Atomic::True), + /// Create a hybrid node from given arguments. + pub fn mk_hybrid_node(child: HctlTreeNode, var: String, op: HybridOp) -> HctlTreeNode { + HctlTreeNode { + subform_str: format!("({} {{{}}}: {})", op, var, child.subform_str), + height: child.height + 1, + node_type: NodeType::HybridNode(op, var, Box::new(child)), } } -} -impl fmt::Display for HctlTreeNode { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", self.subform_str) + /// Create an unary node from given arguments. + pub fn mk_unary_node(child: HctlTreeNode, op: UnaryOp) -> HctlTreeNode { + HctlTreeNode { + subform_str: format!("({} {})", op, child.subform_str), + height: child.height + 1, + node_type: NodeType::UnaryNode(op, Box::new(child)), + } } -} -/// Create a hybrid node from given arguments. -pub fn create_hybrid(child: HctlTreeNode, var: String, op: HybridOp) -> HctlTreeNode { - HctlTreeNode { - subform_str: format!("({} {{{}}}: {})", op, var, child.subform_str), - height: child.height + 1, - node_type: NodeType::HybridNode(op, var, Box::new(child)), + /// Create a binary node from given arguments. + pub fn mk_binary_node(left: HctlTreeNode, right: HctlTreeNode, op: BinaryOp) -> HctlTreeNode { + HctlTreeNode { + subform_str: format!("({} {} {})", left.subform_str, op, right.subform_str), + height: cmp::max(left.height, right.height) + 1, + node_type: NodeType::BinaryNode(op, Box::new(left), Box::new(right)), + } } -} -/// Create an unary node from given arguments. -pub fn create_unary(child: HctlTreeNode, op: UnaryOp) -> HctlTreeNode { - HctlTreeNode { - subform_str: format!("({} {})", op, child.subform_str), - height: child.height + 1, - node_type: NodeType::UnaryNode(op, Box::new(child)), + /// Create a terminal `variable` node from given arguments. + pub fn mk_var_node(var_name: String) -> HctlTreeNode { + HctlTreeNode { + subform_str: format!("{{{var_name}}}"), + height: 0, + node_type: NodeType::TerminalNode(Atomic::Var(var_name)), + } + } + + /// Create a terminal `proposition` node from given arguments. + pub fn mk_prop_node(prop_name: String) -> HctlTreeNode { + HctlTreeNode { + subform_str: prop_name.clone(), + height: 0, + node_type: NodeType::TerminalNode(Atomic::Prop(prop_name)), + } } -} -/// Create a binary node from given arguments. -pub fn create_binary(left: HctlTreeNode, right: HctlTreeNode, op: BinaryOp) -> HctlTreeNode { - HctlTreeNode { - subform_str: format!("({} {} {})", left.subform_str, op, right.subform_str), - height: cmp::max(left.height, right.height) + 1, - node_type: NodeType::BinaryNode(op, Box::new(left), Box::new(right)), + /// Create a terminal `constant` node (true/false) from given arguments. + /// `constant` should only be "true" or "false" + pub fn mk_constant_node(constant_val: bool) -> HctlTreeNode { + if constant_val { + HctlTreeNode { + subform_str: "True".to_string(), + height: 0, + node_type: NodeType::TerminalNode(Atomic::True), + } + } else { + HctlTreeNode { + subform_str: "False".to_string(), + height: 0, + node_type: NodeType::TerminalNode(Atomic::False), + } + } } -} -/// Create a terminal `variable` node from given arguments. -pub fn create_var_node(var_name: String) -> HctlTreeNode { - HctlTreeNode { - subform_str: format!("{{{var_name}}}"), - height: 0, - node_type: NodeType::TerminalNode(Atomic::Var(var_name)), + /// Create a terminal `wild-card proposition` node from given arguments. + pub fn mk_wild_card_node(prop_name: String) -> HctlTreeNode { + HctlTreeNode { + subform_str: format!("%{prop_name}%"), + height: 0, + node_type: NodeType::TerminalNode(Atomic::WildCardProp(prop_name)), + } } } -/// Create a terminal `proposition` node from given arguments. -pub fn create_prop_node(prop_name: String) -> HctlTreeNode { - HctlTreeNode { - subform_str: prop_name.clone(), - height: 0, - node_type: NodeType::TerminalNode(Atomic::Prop(prop_name)), +impl fmt::Display for HctlTreeNode { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "{}", self.subform_str) } } -/// Create a terminal `constant` node (true/false) from given arguments. -/// `constant` should only be "true" or "false" -pub fn create_constant_node(constant_val: bool) -> HctlTreeNode { - if constant_val { - HctlTreeNode { - subform_str: "True".to_string(), - height: 0, - node_type: NodeType::TerminalNode(Atomic::True), - } - } else { - HctlTreeNode { - subform_str: "False".to_string(), - height: 0, - node_type: NodeType::TerminalNode(Atomic::False), - } +#[cfg(test)] +mod tests { + use crate::preprocessing::node::HctlTreeNode; + use crate::preprocessing::tokenizer::{try_tokenize_extended_formula, try_tokenize_formula}; + + #[test] + /// Test creation, ordering, and display of HCTL tree nodes. + fn test_tree_nodes() { + // formula containing all kinds of operators and terminals (even wild-card propositions) + let formula1 = "!{x}: 3{y}: (@{x}: ~{y} & %subst% & True ^ v1)".to_string(); + // much shorter formula to generate shallower tree + let formula2 = "!{x}: AX {x}".to_string(); + + // test `new` function works + let tokens1 = try_tokenize_extended_formula(formula1).unwrap(); + let tokens2 = try_tokenize_formula(formula2).unwrap(); + let node1 = HctlTreeNode::new(&tokens1).unwrap(); + let node2 = HctlTreeNode::new(&tokens2).unwrap(); + + // higher tree should be greater + assert!(node1 > node2); + assert!(node2 <= node1); + + // test display + let node1_str = "(Bind {x}: (Exists {y}: (Jump {x}: (((~ {y}) & (%subst% & True)) ^ v1))))"; + let node2_str = "(Bind {x}: (Ax {x}))"; + assert_eq!(node1.to_string(), node1_str.to_string()); + assert_eq!(node2.to_string(), node2_str.to_string()); } } diff --git a/src/preprocessing/operator_enums.rs b/src/preprocessing/operator_enums.rs index af7e0e5..0e105ac 100644 --- a/src/preprocessing/operator_enums.rs +++ b/src/preprocessing/operator_enums.rs @@ -38,12 +38,15 @@ pub enum HybridOp { } /// Enum for atomic sub-formulae - propositions, variables, and constants. +/// There are also `wild-card propositions`, that will be directly evaluated as some precomputed +/// coloured set. We have to differentiate them from classical propositions. #[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd)] pub enum Atomic { - Prop(String), // A proposition name - Var(String), // A variable name - True, // A true constant - False, // A false constant + Prop(String), // A proposition name + Var(String), // A variable name + True, // A true constant + False, // A false constant + WildCardProp(String), // A wild-card proposition name } impl fmt::Display for UnaryOp { @@ -82,6 +85,7 @@ impl fmt::Display for Atomic { Atomic::Prop(name) => write!(f, "{name}"), Atomic::True => write!(f, "True"), Atomic::False => write!(f, "False"), + Atomic::WildCardProp(name) => write!(f, "%{name}%"), } } } diff --git a/src/preprocessing/parser.rs b/src/preprocessing/parser.rs index 30ba717..30e8d3a 100644 --- a/src/preprocessing/parser.rs +++ b/src/preprocessing/parser.rs @@ -9,7 +9,9 @@ use crate::preprocessing::node::*; use crate::preprocessing::operator_enums::*; -use crate::preprocessing::tokenizer::{try_tokenize_formula, HctlToken}; +use crate::preprocessing::tokenizer::{ + try_tokenize_extended_formula, try_tokenize_formula, HctlToken, +}; use crate::preprocessing::utils::check_props_and_rename_vars; use biodivine_lib_param_bn::BooleanNetwork; @@ -18,6 +20,7 @@ use std::collections::HashMap; /// Parse an HCTL formula string representation into an actual formula tree. /// Basically a wrapper for tokenize+parse (used often for testing/debug purposes). +/// /// NEEDS to call procedure for renaming variables to fully finish the preprocessing step. pub fn parse_hctl_formula(formula: &str) -> Result { let tokens = try_tokenize_formula(formula.to_string())?; @@ -25,6 +28,16 @@ pub fn parse_hctl_formula(formula: &str) -> Result { Ok(tree) } +/// Parse an extended HCTL formula string representation into an actual formula tree. +/// Extended formulae can include `wild-card propositions` in form "%proposition%". +/// +/// NEEDS to call procedure for renaming variables to fully finish the preprocessing step. +pub fn parse_extended_formula(formula: &str) -> Result { + let tokens = try_tokenize_extended_formula(formula.to_string())?; + let tree = parse_hctl_tokens(&tokens)?; + Ok(tree) +} + /// Parse an HCTL formula string representation into an actual formula tree with renamed (minimized) /// set of variables. /// Basically a wrapper for the whole preprocessing step (tokenize + parse + rename vars). @@ -32,8 +45,19 @@ pub fn parse_and_minimize_hctl_formula( bn: &BooleanNetwork, formula: &str, ) -> Result { - let tokens = try_tokenize_formula(formula.to_string())?; - let tree = parse_hctl_tokens(&tokens)?; + let tree = parse_hctl_formula(formula)?; + let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?; + Ok(tree) +} + +/// Parse an extended HCTL formula string representation into an actual formula tree +/// with renamed (minimized) set of variables. +/// Extended formulae can include `wild-card propositions` in form "%proposition%". +pub fn parse_and_minimize_extended_formula( + bn: &BooleanNetwork, + formula: &str, +) -> Result { + let tree = parse_extended_formula(formula)?; let tree = check_props_and_rename_vars(tree, HashMap::new(), String::new(), bn)?; Ok(tree) } @@ -99,10 +123,12 @@ fn parse_1_hybrid(tokens: &[HctlToken]) -> Result { )); } match &tokens[i] { - HctlToken::Hybrid(op, var) => { - create_hybrid(parse_1_hybrid(&tokens[(i + 1)..])?, var.clone(), op.clone()) - } - _ => HctlTreeNode::new(), // This branch cant happen, but must result in same type + HctlToken::Hybrid(op, var) => HctlTreeNode::mk_hybrid_node( + parse_1_hybrid(&tokens[(i + 1)..])?, + var.clone(), + op.clone(), + ), + _ => unreachable!(), // we already made sure that this is indeed a hybrid token } } else { parse_2_iff(tokens)? @@ -113,7 +139,7 @@ fn parse_1_hybrid(tokens: &[HctlToken]) -> Result { fn parse_2_iff(tokens: &[HctlToken]) -> Result { let iff_token = index_of_first(tokens, HctlToken::Binary(BinaryOp::Iff)); Ok(if let Some(i) = iff_token { - create_binary( + HctlTreeNode::mk_binary_node( parse_3_imp(&tokens[..i])?, parse_2_iff(&tokens[(i + 1)..])?, BinaryOp::Iff, @@ -127,7 +153,7 @@ fn parse_2_iff(tokens: &[HctlToken]) -> Result { fn parse_3_imp(tokens: &[HctlToken]) -> Result { let imp_token = index_of_first(tokens, HctlToken::Binary(BinaryOp::Imp)); Ok(if let Some(i) = imp_token { - create_binary( + HctlTreeNode::mk_binary_node( parse_4_or(&tokens[..i])?, parse_3_imp(&tokens[(i + 1)..])?, BinaryOp::Imp, @@ -141,7 +167,7 @@ fn parse_3_imp(tokens: &[HctlToken]) -> Result { fn parse_4_or(tokens: &[HctlToken]) -> Result { let or_token = index_of_first(tokens, HctlToken::Binary(BinaryOp::Or)); Ok(if let Some(i) = or_token { - create_binary( + HctlTreeNode::mk_binary_node( parse_5_xor(&tokens[..i])?, parse_4_or(&tokens[(i + 1)..])?, BinaryOp::Or, @@ -155,7 +181,7 @@ fn parse_4_or(tokens: &[HctlToken]) -> Result { fn parse_5_xor(tokens: &[HctlToken]) -> Result { let xor_token = index_of_first(tokens, HctlToken::Binary(BinaryOp::Xor)); Ok(if let Some(i) = xor_token { - create_binary( + HctlTreeNode::mk_binary_node( parse_6_and(&tokens[..i])?, parse_5_xor(&tokens[(i + 1)..])?, BinaryOp::Xor, @@ -169,7 +195,7 @@ fn parse_5_xor(tokens: &[HctlToken]) -> Result { fn parse_6_and(tokens: &[HctlToken]) -> Result { let and_token = index_of_first(tokens, HctlToken::Binary(BinaryOp::And)); Ok(if let Some(i) = and_token { - create_binary( + HctlTreeNode::mk_binary_node( parse_7_binary_temp(&tokens[..i])?, parse_6_and(&tokens[(i + 1)..])?, BinaryOp::And, @@ -184,12 +210,12 @@ fn parse_7_binary_temp(tokens: &[HctlToken]) -> Result { let binary_token = index_of_first_binary_temp(tokens); Ok(if let Some(i) = binary_token { match &tokens[i] { - HctlToken::Binary(op) => create_binary( + HctlToken::Binary(op) => HctlTreeNode::mk_binary_node( parse_8_unary(&tokens[..i])?, parse_7_binary_temp(&tokens[(i + 1)..])?, op.clone(), ), - _ => HctlTreeNode::new(), // This branch cant happen, but must result in same type + _ => unreachable!(), // we already made sure that this is indeed a binary token } } else { parse_8_unary(tokens)? @@ -201,8 +227,10 @@ fn parse_8_unary(tokens: &[HctlToken]) -> Result { let unary_token = index_of_first_unary(tokens); Ok(if let Some(i) = unary_token { match &tokens[i] { - HctlToken::Unary(op) => create_unary(parse_8_unary(&tokens[(i + 1)..])?, op.clone()), - _ => HctlTreeNode::new(), // This branch cant happen, but must result in same type + HctlToken::Unary(op) => { + HctlTreeNode::mk_unary_node(parse_8_unary(&tokens[(i + 1)..])?, op.clone()) + } + _ => unreachable!(), // we already made sure that this is indeed an unary token } } else { parse_9_terminal_and_parentheses(tokens)? @@ -215,18 +243,24 @@ fn parse_9_terminal_and_parentheses(tokens: &[HctlToken]) -> Result { return if name == "true" || name == "True" || name == "1" { - Ok(create_constant_node(true)) + Ok(HctlTreeNode::mk_constant_node(true)) } else if name == "false" || name == "False" || name == "0" { - Ok(create_constant_node(false)) + Ok(HctlTreeNode::mk_constant_node(false)) } else { - Ok(create_prop_node(name.clone())) + Ok(HctlTreeNode::mk_prop_node(name.clone())) } } - HctlToken::Atom(Atomic::Var(name)) => return Ok(create_var_node(name.clone())), + HctlToken::Atom(Atomic::Var(name)) => { + return Ok(HctlTreeNode::mk_var_node(name.clone())) + } + HctlToken::Atom(Atomic::WildCardProp(name)) => { + return Ok(HctlTreeNode::mk_wild_card_node(name.clone())) + } // recursively solve sub-formulae in parentheses HctlToken::Tokens(inner) => return parse_hctl_tokens(inner), _ => {} // otherwise, fall through to the error at the end. @@ -240,64 +274,70 @@ fn parse_9_terminal_and_parentheses(tokens: &[HctlToken]) -> Result ((PROP2 | False) => True)) Au (True ^ False))".to_string() ); + + // all formulae must be correctly parsed also using the extended version of HCTL + assert!(parse_extended_formula(valid1).is_ok()); + assert!(parse_extended_formula(valid2).is_ok()); + assert!(parse_extended_formula(valid3).is_ok()); + assert!(parse_extended_formula(valid4).is_ok()); } #[test] /// Test parsing of several valid HCTL formulae against expected results. fn compare_parser_with_expected() { - let formula = "(false & p1)".to_string(); - let expected_tree = create_binary( - create_constant_node(false), - create_prop_node("p1".to_string()), + let formula = "(false & p1)"; + let expected_tree = HctlTreeNode::mk_binary_node( + HctlTreeNode::mk_constant_node(false), + HctlTreeNode::mk_prop_node("p1".to_string()), BinaryOp::And, ); - assert_eq!(parse_hctl_formula(formula.as_str()).unwrap(), expected_tree); + assert_eq!(parse_hctl_formula(formula).unwrap(), expected_tree); - let formula = "!{x}: (AX {x})".to_string(); - let expected_tree = create_hybrid( - create_unary(create_var_node("x".to_string()), UnaryOp::Ax), + let formula = "!{x}: (AX {x})"; + let expected_tree = HctlTreeNode::mk_hybrid_node( + HctlTreeNode::mk_unary_node(HctlTreeNode::mk_var_node("x".to_string()), UnaryOp::Ax), "x".to_string(), HybridOp::Bind, ); - assert_eq!(parse_hctl_formula(formula.as_str()).unwrap(), expected_tree); + assert_eq!(parse_hctl_formula(formula).unwrap(), expected_tree); } #[test] - /// Test parsing of several invalid HCTL formulae. + /// Test parsing of several completely invalid HCTL formulae. fn test_parse_invalid_formulae() { let invalid_formulae = vec![ "!{x}: AG EK {x}", @@ -313,6 +353,31 @@ mod tests { for formula in invalid_formulae { assert!(parse_hctl_formula(formula).is_err()); + // all formulae are invalid regardless if we allow for wild-card propositions + assert!(parse_extended_formula(formula).is_err()); } } + + #[test] + /// Test parsing several extended HCTL formulae. + fn test_parse_extended_formulae() { + let formula = "(!{x}: AG EF {x}) & %p%"; + // parser for standard HCTL should fail, for extended succeed + assert!(parse_hctl_formula(formula).is_err()); + assert!(parse_extended_formula(formula).is_ok()); + let tree = parse_extended_formula(formula).unwrap(); + assert_eq!( + tree.subform_str, + "((Bind {x}: (Ag (Ef {x}))) & %p%)".to_string() + ); + + let formula = "!{x}: 3{y}: (@{x}: ~{y} & %s%) & (@{y}: %s%)"; + assert!(parse_hctl_formula(formula).is_err()); + assert!(parse_extended_formula(formula).is_ok()); + let tree = parse_extended_formula(formula).unwrap(); + assert_eq!( + tree.subform_str, + "(Bind {x}: (Exists {y}: ((Jump {x}: ((~ {y}) & %s%)) & (Jump {y}: %s%))))".to_string() + ); + } } diff --git a/src/preprocessing/tokenizer.rs b/src/preprocessing/tokenizer.rs index 7ad7beb..487097a 100644 --- a/src/preprocessing/tokenizer.rs +++ b/src/preprocessing/tokenizer.rs @@ -19,13 +19,21 @@ pub enum HctlToken { /// Try to tokenize given HCTL formula string. /// Wrapper for the recursive `try_tokenize_formula` function. pub fn try_tokenize_formula(formula: String) -> Result, String> { - try_tokenize_recursive(&mut formula.chars().peekable(), true) + try_tokenize_recursive(&mut formula.chars().peekable(), true, false) +} + +/// Try to tokenize given `extended` HCTL formula string. That means that formula can include +/// `wild-card properties` in form of "%proposition%". +/// Wrapper for the recursive `try_tokenize_formula` function. +pub fn try_tokenize_extended_formula(formula: String) -> Result, String> { + try_tokenize_recursive(&mut formula.chars().peekable(), true, true) } /// Process a peekable iterator of characters into a vector of `HctlToken`s. fn try_tokenize_recursive( input_chars: &mut Peekable, top_level: bool, + parse_wild_cards: bool, ) -> Result, String> { let mut output = Vec::new(); @@ -140,7 +148,7 @@ fn try_tokenize_recursive( } '(' => { // start a nested token group - let token_group = try_tokenize_recursive(input_chars, false)?; + let token_group = try_tokenize_recursive(input_chars, false, parse_wild_cards)?; output.push(HctlToken::Tokens(token_group)); } // variable name @@ -154,6 +162,17 @@ fn try_tokenize_recursive( return Err("Expected '}'.".to_string()); } } + // wild-card proposition name + '%' if parse_wild_cards => { + let name = collect_name(input_chars)?; + if name.is_empty() { + return Err("Wild-card proposition name can't be empty.".to_string()); + } + output.push(HctlToken::Atom(Atomic::WildCardProp(name))); + if Some('%') != input_chars.next() { + return Err("Expected '%'.".to_string()); + } + } // proposition name or constant // these 2 are NOT distinguished now but later during parsing c if is_valid_in_name(c) => { @@ -250,6 +269,7 @@ impl fmt::Display for HctlToken { HctlToken::Hybrid(op, var) => write!(f, "{op:?} {{{var}}}:"), HctlToken::Atom(Atomic::Prop(name)) => write!(f, "{name}"), HctlToken::Atom(Atomic::Var(name)) => write!(f, "{{{name}}}"), + HctlToken::Atom(Atomic::WildCardProp(name)) => write!(f, "%{name}%"), HctlToken::Atom(constant) => write!(f, "{constant:?}"), HctlToken::Tokens(_) => write!(f, "( TOKENS )"), // debug purposes only } @@ -277,15 +297,20 @@ pub fn print_tokens(tokens: &Vec) { #[cfg(test)] mod tests { use crate::preprocessing::operator_enums::*; - use crate::preprocessing::tokenizer::{try_tokenize_formula, HctlToken}; + use crate::preprocessing::tokenizer::{ + try_tokenize_extended_formula, try_tokenize_formula, HctlToken, + }; #[test] /// Test tokenization process on several valid HCTL formulae. + /// Test both some important and meaningful formulae and formulae that include wide + /// range of operators. fn test_tokenize_valid_formulae() { + // formula for attractors let valid1 = "!{x}: AG EF {x}".to_string(); - let tokens1_result = try_tokenize_formula(valid1); + let tokens1 = try_tokenize_formula(valid1).unwrap(); assert_eq!( - tokens1_result.unwrap(), + tokens1, vec![ HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), HctlToken::Unary(UnaryOp::Ag), @@ -294,32 +319,31 @@ mod tests { ] ); - let valid2 = "AF (!{x}: (AX (~{x} & AF {x})))".to_string(); - let tokens2_result = try_tokenize_formula(valid2); + // formula for cyclic attractors + let valid2 = "!{x}: (AX (~{x} & AF {x}))".to_string(); + let tokens2 = try_tokenize_formula(valid2).unwrap(); assert_eq!( - tokens2_result.unwrap(), + tokens2, vec![ - HctlToken::Unary(UnaryOp::Af), + HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), HctlToken::Tokens(vec![ - HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), + HctlToken::Unary(UnaryOp::Ax), HctlToken::Tokens(vec![ - HctlToken::Unary(UnaryOp::Ax), - HctlToken::Tokens(vec![ - HctlToken::Unary(UnaryOp::Not), - HctlToken::Atom(Atomic::Var("x".to_string())), - HctlToken::Binary(BinaryOp::And), - HctlToken::Unary(UnaryOp::Af), - HctlToken::Atom(Atomic::Var("x".to_string())), - ]), + HctlToken::Unary(UnaryOp::Not), + HctlToken::Atom(Atomic::Var("x".to_string())), + HctlToken::Binary(BinaryOp::And), + HctlToken::Unary(UnaryOp::Af), + HctlToken::Atom(Atomic::Var("x".to_string())), ]), ]), ] ); + // formula for bi-stability let valid3 = "!{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y})".to_string(); - let tokens3_result = try_tokenize_formula(valid3); + let tokens3 = try_tokenize_formula(valid3).unwrap(); assert_eq!( - tokens3_result.unwrap(), + tokens3, vec![ HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), HctlToken::Hybrid(HybridOp::Exists, "y".to_string()), @@ -339,25 +363,98 @@ mod tests { ]), ] ); + + // Formula with all kinds of binary operators, and terminals, including propositions + // starting on A/E. Note that constants are treated as propositions at this point. + let valid4 = "(prop1 <=> PROP2 | false => 1) EU (0 AW A_prop ^ E_prop)".to_string(); + let tokens4 = try_tokenize_formula(valid4).unwrap(); + assert_eq!( + tokens4, + vec![ + HctlToken::Tokens(vec![ + HctlToken::Atom(Atomic::Prop("prop1".to_string())), + HctlToken::Binary(BinaryOp::Iff), + HctlToken::Atom(Atomic::Prop("PROP2".to_string())), + HctlToken::Binary(BinaryOp::Or), + HctlToken::Atom(Atomic::Prop("false".to_string())), + HctlToken::Binary(BinaryOp::Imp), + HctlToken::Atom(Atomic::Prop("1".to_string())), + ]), + HctlToken::Binary(BinaryOp::Eu), + HctlToken::Tokens(vec![ + HctlToken::Atom(Atomic::Prop("0".to_string())), + HctlToken::Binary(BinaryOp::Aw), + HctlToken::Atom(Atomic::Prop("A_prop".to_string())), + HctlToken::Binary(BinaryOp::Xor), + HctlToken::Atom(Atomic::Prop("E_prop".to_string())), + ]), + ] + ); } #[test] /// Test tokenization process on several invalid HCTL formulae. + /// Try to cover wide range of invalid possibilities, as well as potential frequent mistakes. fn test_tokenize_invalid_formulae() { let invalid_formulae = vec![ "!{x}: AG EF {x<&}", + "!{x}: A* EF {x}", + "!{x}: AG E* {x}", + "!{x}: AG EF {}", "!{x AG EF {x}", "!{}: AG EF {x}", + "!EF p1", "{x}: AG EF {x}", "V{x} AG EF {x}", "!{x}: AG EX {x} $", "!{x}: # AG EF {x}", "!{x}: AG* EF {x}", "!{x}: (a EW b) =>= (c AU d)", + "p1 )", + "( p1", + "p1 <> p2", + "p1 >= p2", + "p1 <= p2", ]; for formula in invalid_formulae { assert!(try_tokenize_formula(formula.to_string()).is_err()) } } + + #[test] + /// Test tokenization process on several extended HCTL formulae containing + /// `wild-card propositions`. + fn test_tokenize_extended_formulae() { + let formula1 = "p & %p%"; + // tokenizer for standard HCTL should fail, for extended succeed + assert!(try_tokenize_formula(formula1.to_string()).is_err()); + assert!(try_tokenize_extended_formula(formula1.to_string()).is_ok()); + let tokens = try_tokenize_extended_formula(formula1.to_string()).unwrap(); + assert_eq!( + tokens, + vec![ + HctlToken::Atom(Atomic::Prop("p".to_string())), + HctlToken::Binary(BinaryOp::And), + HctlToken::Atom(Atomic::WildCardProp("p".to_string())), + ] + ); + + let formula2 = "!{x}: (@{x}: {x} & %s%)"; + assert!(try_tokenize_formula(formula2.to_string()).is_err()); + assert!(try_tokenize_extended_formula(formula2.to_string()).is_ok()); + let tokens = try_tokenize_extended_formula(formula2.to_string()).unwrap(); + assert_eq!( + tokens, + vec![ + HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), + HctlToken::Tokens(vec![ + HctlToken::Hybrid(HybridOp::Jump, "x".to_string()), + HctlToken::Atom(Atomic::Var("x".to_string())), + HctlToken::Binary(BinaryOp::And), + HctlToken::Atom(Atomic::WildCardProp("s".to_string())), + ]), + ] + ); + } } diff --git a/src/preprocessing/utils.rs b/src/preprocessing/utils.rs index 4601305..419a386 100644 --- a/src/preprocessing/utils.rs +++ b/src/preprocessing/utils.rs @@ -7,7 +7,7 @@ use biodivine_lib_param_bn::BooleanNetwork; use std::collections::HashMap; -/// Checks that all vars in formula are quantified (exactly once) and props are valid. +/// Checks that all vars in formula are quantified (exactly once) and props are valid BN variables. /// Renames hctl vars in the formula tree to canonical form - "x", "xx", ... /// Renames as many state-vars as possible to identical names, without changing the semantics. pub fn check_props_and_rename_vars( @@ -28,7 +28,7 @@ pub fn check_props_and_rename_vars( return Err(format!("Variable {name} is free.")); } let renamed_var = mapping_dict.get(name.as_str()).unwrap(); - Ok(create_var_node(renamed_var.to_string())) + Ok(HctlTreeNode::mk_var_node(renamed_var.to_string())) } Atomic::Prop(name) => { // check that proposition corresponds to valid BN variable @@ -38,14 +38,14 @@ pub fn check_props_and_rename_vars( } Ok(orig_node) } - // constants are always fine + // constants or wild-card propositions are always considered fine _ => return Ok(orig_node), }, // just dive one level deeper for unary nodes, and rename string NodeType::UnaryNode(op, child) => { let node = check_props_and_rename_vars(*child, mapping_dict, last_used_name.clone(), bn)?; - Ok(create_unary(node, op)) + Ok(HctlTreeNode::mk_unary_node(node, op)) } // just dive deeper for binary nodes, and rename string NodeType::BinaryNode(op, left, right) => { @@ -56,7 +56,7 @@ pub fn check_props_and_rename_vars( bn, )?; let node2 = check_props_and_rename_vars(*right, mapping_dict, last_used_name, bn)?; - Ok(create_binary(node1, node2, op)) + Ok(HctlTreeNode::mk_binary_node(node1, node2, op)) } // hybrid nodes are more complicated NodeType::HybridNode(op, var, child) => { @@ -86,29 +86,32 @@ pub fn check_props_and_rename_vars( // rename the variable in the node let renamed_var = mapping_dict.get(var.as_str()).unwrap(); - Ok(create_hybrid(node, renamed_var.clone(), op)) + Ok(HctlTreeNode::mk_hybrid_node(node, renamed_var.clone(), op)) } }; } #[cfg(test)] mod tests { - use crate::preprocessing::parser::{parse_and_minimize_hctl_formula, parse_hctl_formula}; + use crate::preprocessing::parser::{ + parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula, + parse_extended_formula, parse_hctl_formula, + }; use crate::preprocessing::utils::check_props_and_rename_vars; use biodivine_lib_param_bn::BooleanNetwork; use std::collections::HashMap; /// Compare tree for formula with automatically minimized state var number to the /// tree for the semantically same, but already minimized formula. - fn test_state_var_minimization(formula: String, formula_minimized: String) { + fn test_state_var_minimization(formula: &str, formula_minimized: &str) { // define any placeholder bn let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); // automatically modify the original formula via preprocessing step - let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str()).unwrap(); + let tree = parse_and_minimize_hctl_formula(&bn, formula).unwrap(); // get expected tree using the (same) formula with already manually minimized vars - let tree_minimized = parse_hctl_formula(formula_minimized.as_str()).unwrap(); + let tree_minimized = parse_hctl_formula(formula_minimized).unwrap(); assert_eq!(tree_minimized, tree); } @@ -117,24 +120,39 @@ mod tests { /// Test minimization of number of state variables and their renaming. fn test_state_var_minimization_simple() { let formula = "(!{x}: AG EF {x}) | (!{y}: !{x}: (AX {y} & AX {x})) | (!{z}: AG EF {z})"; - // same formula with already minimized vars let formula_minimized = "(!{x}: AG EF {x}) | (!{x}: !{xx}: (AX {x} & AX {xx})) | (!{x}: AG EF {x})"; - test_state_var_minimization(formula.to_string(), formula_minimized.to_string()); + test_state_var_minimization(formula, formula_minimized); } #[test] /// Test minimization of number of state variables and their renaming. fn test_state_var_minimization_complex() { - // formula "FORKS1 & FORKS2" - both parts are semantically same, just use different var names + // conjunction of two semantically same formulae (for FORK states) that use different var names let formula = "(!{x}: 3{y}: (@{x}: ~{y} & (!{z}: AX {z})) & (@{y}: (!{z}: AX {z}))) & (!{x1}: 3{y1}: (@{x1}: ~{y1} & (!{z1}: AX {z1})) & (@{y1}: (!{z1}: AX {z1})))"; - // same formula with already minimized vars let formula_minimized = "(!{x}: 3{xx}: (@{x}: ~{xx} & (!{xxx}: AX {xxx})) & (@{xx}: (!{xxx}: AX {xxx}))) & (!{x}: 3{xx}: (@{x}: ~{xx} & (!{xxx}: AX {xxx})) & (@{xx}: (!{xxx}: AX {xxx})))"; - test_state_var_minimization(formula.to_string(), formula_minimized.to_string()); + test_state_var_minimization(formula, formula_minimized); + } + + #[test] + /// Test minimization of number of state variables and their renaming, but this time with + /// formula containing wild-card propositions (to check they are not affected). + fn test_state_var_minimization_with_wild_cards() { + // define any placeholder bn + let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); + + let formula = "!{x}: 3{y}: (@{x}: ~{y} & %subst%) & (@{y}: %subst%)"; + // same formula with already minimized vars + let formula_minimized = "!{x}: 3{xx}: (@{x}: ~{xx} & %subst%) & (@{xx}: %subst%)"; + + let tree = parse_and_minimize_extended_formula(&bn, formula).unwrap(); + // get expected tree using the (same) formula with already manually minimized vars + let tree_minimized = parse_extended_formula(formula_minimized).unwrap(); + assert_eq!(tree_minimized, tree); } #[test] @@ -144,8 +162,8 @@ mod tests { let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); // define and parse formula with free variable - let formula = "AX {x}".to_string(); - let tree = parse_hctl_formula(formula.as_str()).unwrap(); + let formula = "AX {x}"; + let tree = parse_hctl_formula(formula).unwrap(); assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); } @@ -157,8 +175,8 @@ mod tests { let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); // define and parse formula with two variables - let formula = "!{x}: !{x}: AX {x}".to_string(); - let tree = parse_hctl_formula(formula.as_str()).unwrap(); + let formula = "!{x}: !{x}: AX {x}"; + let tree = parse_hctl_formula(formula).unwrap(); assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); } @@ -170,8 +188,8 @@ mod tests { let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap(); // define and parse formula with invalid proposition - let formula = "AX invalid_proposition".to_string(); - let tree = parse_hctl_formula(formula.as_str()).unwrap(); + let formula = "AX invalid_proposition"; + let tree = parse_hctl_formula(formula).unwrap(); assert!(check_props_and_rename_vars(tree, HashMap::new(), String::new(), &bn).is_err()); }