Add support for wild-card propositions (#9)

* WIP: Add model checking for formulae that use wild-card propositions

* Refactor, fix small bugs, add test cases, modify HctlTreeNode

* Extend tests

* Update readme regarding new functionality

* Refactoring

* Add validation step for substitution context.

* Fix github workflow

* Update instructions

* Downgrade clap dependency for compatibility

* Downgrade termcolor dependency for compatibility

* Remove unused githooks

.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/[email protected]
         with:

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "biodivine-hctl-model-checker"
-version = "0.1.7"
+version = "0.2.0"
 authors = ["Ondřej Huvar <[email protected]>", "Samuel Pastva <[email protected]>"]
 edition = "2021"
 description = "Library for symbolic HCTL model checking on partially defined Boolean networks."

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%`.

src/analysis.rs

@@ -1,15 +1,15 @@
 //! 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;
 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());
     }
 }

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(),

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<String, i32>,
+    /// Cached sub-formulae and their result + corresponding mapping of variable renaming
+    pub cache: HashMap<String, (GraphColoredVertices, HashMap<String, String>)>,
+}
+
+impl EvalContext {
+    /// Instantiate the struct with precomputed duplicates and empty cache.
+    pub fn new(duplicates: HashMap<String, i32>) -> 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<HctlTreeNode>) -> 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<String, i32> {
+        self.duplicates.clone()
+    }
+
+    /// Get the cache field containing the cached sub-formulae, their result and var renaming.
+    pub fn get_cache(&self) -> HashMap<String, (GraphColoredVertices, HashMap<String, String>)> {
+        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<String, GraphColoredVertices>,
+    ) {
+        // 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);
+    }
+}