Add support for variable domains

Cargo.toml

@@ -30,3 +30,4 @@ biodivine-lib-param-bn = ">=0.5.1, <1.0.0"
 clap = { version = "4.1.4", features = ["derive"] }
 rand = "0.8.5"
 termcolor = "1.1.2"
+zip = "0.6.3"

README.md

@@ -8,9 +8,9 @@
 
 # Symbolic model checker for logic HCTL written in RUST
 
-This repository contains the Rust implementation of the symbolic model checker for hybrid logic HCTL. 
-The method is focused on the analysis of (partially specified) Boolean networks. 
-In particular, it allows to check for any behavioural hypotheses expressible in HCTL on large, non-trivial networks. 
+This repository contains the Rust implementation of the symbolic model checker for hybrid logic HCTL.
+The method is focused on the analysis of (partially specified) Boolean networks.
+In particular, it allows to check for any behavioural hypotheses expressible in HCTL on large, non-trivial networks.
 This includes properties like stability, bi-stability, attractors, or oscillatory behaviour.
 
 ## Prerequisites
@@ -26,25 +26,28 @@ This repository encompasses the CLI model-checking tool, and the model-checking
 
 ### Model-checking tool
 
-Given a (partially defined) Boolean network and HCTL formulae (encoding properties we want to check), the tool computes all the states of the network (and corresponding parametrizations) that satisfy the formula.
+Given a (partially defined) Boolean network model and HCTL formulae (encoding properties we want to check), 
+the tool computes all the states of the network (and corresponding parametrizations) that satisfy the formula.
 Currently, there is only a command-line interface, with a GUI soon to be implemented.
-Depending on the mode, the program can either print the numbers of satisfying states and colours, or print all the satisfying assignments.
+Depending on the mode, the program can generate BDDs encoding the resulting states and parametrizations,
+it can print the numbers of satisfying states and colours, or print all the satisfying assignments.
 
 To directly invoke the model checker, compile the code using
 ```
 cargo build --release
 ```
 and then run the binary:
 ```
-.\target\release\hctl-model-checker <MODEL_PATH> <FORMULAE_PATH> [-m <MODEL_FORMAT>] [-p <PRINT_OPTION>] [-h]
+.\target\release\hctl-model-checker <MODEL_PATH> <FORMULAE_PATH>
 ```
-
 - `MODEL_PATH` is a path to a file with BN model in selected format (see below, `aeon` is default)
 - `FORMULAE_PATH` is path to a file with a set of valid HCTL formulae (one per line)
-- `PRINT_OPTION` is one of `no-print`/`summary`/`with-progress`/`exhaustive` and defines the amount of information on the output (`summary` is a default mode)
-- `MODEL_FORMAT` is one of `aeon`/`bnet`/`smbl` and defines the input format (`aeon` is default)
 
-For more help, use option `-h` or `--help`.
+We support the following optional arguments:
+- `-o <OUTPUT_BUNDLE>` - A path to generate a zip bundle with resulting BDDs.
+- `-e <EXTENDED_CONTEXT>` -  A path to an input zip bundle with BDDs specifying context of wild-cards (only relevant for extended formulae).
+- `-p <PRINT_OPTION>` - An amount of information printed - one of `no-print`/`summary`/`with-progress`/`exhaustive`.
+- `-h` or `--help` for more information
 
 ### Library
 
@@ -55,14 +58,14 @@ Further, useful functionality and structures regarding parsing (parser, tokenize
 ## Model formats
 
 The model checker takes BN models in `aeon` format as its default input, with many example models present in the `benchmark_models` directory.
-You can also use `sbml` and `bnet` models by specifying the format as a CLI option (see above).
+However, you can also use `SBML` and `boolnet` models.
 
 ## HCTL formulae
 
-All formulae used must not contain free variables.
-In the input file, there has to be one formula in a correct format per line.
+The file with HCTL properties must contain one formula in a correct format per line.
+The formulae must not contain free variables.
 
-Several interesting formulae are listed in the ```benchmark_formulae.txt``` file.
+The format is illustrated on ```benchmark_formulae.txt``` containing several important formulae.
 
 To create custom formulae, you can use any HCTL operators and many derived ones.
 We use the following syntax:
@@ -88,9 +91,26 @@ The operator precedence is following (the lower, the stronger):
 
 However, it is strongly recommended to use parentheses wherever possible to prevent any parsing issues.
 
-#### Wild-card properties
+### Extended formulae
+
+#### Wild-card propositions
+
+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 of states provided 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%`.
+
+#### Restricting domains of quantified variables
+
+You can also directly restrict a domain of any quantified variable in a following manner:
+* `!{x} in %domain%:`
+
+The domain is treated similar as a "wild-card proposition" (see above).
+During the computation, the user provides an arbitrary set of states that will be used as the domain for the variable (the variable may only take the value of states from that set).
+
+This way the user can directly restrict the domain of every `{x}` encountered during bottom-up computation (makes formula more readable and speeds up the computation).
 
-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%`.
+The following equivalences hold:
+* `!{x} in %A%: phi` = `!{x}: %A% & phi`
+* `3{x} in %A%: @{x}: phi` = `3{x}: @{x}: %A% & phi`
+* `V{x} in %A%: @{x}: phi` = `V{x}: @{x}: %A% => phi`

src/aeon/algo_xie_beerel.rs → src/_aeon_algorithms/algo_xie_beerel.rs

@@ -1,4 +1,4 @@
-use crate::aeon::saturated_reachability::{reach_bwd, reachability_step};
+use crate::_aeon_algorithms::saturated_reachability::{reach_bwd, reachability_step};
 
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};

src/aeon/itgr/_impl_extended_component_process.rs → src/_aeon_algorithms/itgr/_impl_extended_component_process.rs

@@ -2,8 +2,8 @@ use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
 
-use crate::aeon::itgr::{BwdProcess, ExtendedComponentProcess, Process, Scheduler};
-use crate::aeon::saturated_reachability::reach_bwd;
+use crate::_aeon_algorithms::itgr::{BwdProcess, ExtendedComponentProcess, Process, Scheduler};
+use crate::_aeon_algorithms::saturated_reachability::reach_bwd;
 
 impl ExtendedComponentProcess {
     pub fn new(

src/aeon/itgr/_impl_fwd_bwd_process.rs → src/_aeon_algorithms/itgr/_impl_fwd_bwd_process.rs

@@ -1,8 +1,8 @@
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 
-use crate::aeon::itgr::{BwdProcess, FwdProcess, Process, Scheduler};
-use crate::aeon::saturated_reachability::reachability_step;
+use crate::_aeon_algorithms::itgr::{BwdProcess, FwdProcess, Process, Scheduler};
+use crate::_aeon_algorithms::saturated_reachability::reachability_step;
 
 impl BwdProcess {
     pub fn new(initial: GraphColoredVertices, universe: GraphColoredVertices) -> BwdProcess {

src/aeon/itgr/_impl_reachable_process.rs → src/_aeon_algorithms/itgr/_impl_reachable_process.rs

@@ -2,10 +2,10 @@ use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
 
-use crate::aeon::itgr::{
+use crate::_aeon_algorithms::itgr::{
     ExtendedComponentProcess, FwdProcess, Process, ReachableProcess, Scheduler,
 };
-use crate::aeon::saturated_reachability::reach_bwd;
+use crate::_aeon_algorithms::saturated_reachability::reach_bwd;
 
 impl ReachableProcess {
     pub fn new(

src/aeon/itgr/_impl_scheduler.rs → src/_aeon_algorithms/itgr/_impl_scheduler.rs

@@ -2,7 +2,7 @@ use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 use biodivine_lib_param_bn::VariableId;
 
-use crate::aeon::itgr::{Process, Scheduler};
+use crate::_aeon_algorithms::itgr::{Process, Scheduler};
 
 impl Scheduler {
     /// Create a new `Scheduler` with initial universe and active variables.

src/aeon/scc_computation.rs → src/_aeon_algorithms/scc_computation.rs

@@ -1,5 +1,5 @@
-use crate::aeon::algo_xie_beerel::xie_beerel_attractor_set;
-use crate::aeon::itgr::interleaved_transition_guided_reduction;
+use crate::_aeon_algorithms::algo_xie_beerel::xie_beerel_attractor_set;
+use crate::_aeon_algorithms::itgr::interleaved_transition_guided_reduction;
 
 use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
 

src/_test_model_checking/_test_against_precomputed.rs

@@ -0,0 +1,96 @@
+use crate::_test_model_checking::{MODEL_CELL_CYCLE, MODEL_CELL_DIVISION, MODEL_YEAST};
+use crate::mc_utils::get_extended_symbolic_graph;
+use crate::model_checking::{model_check_formula, model_check_formula_dirty};
+use biodivine_lib_param_bn::BooleanNetwork;
+
+/// Run the evaluation for the set of given formulae on a given model.
+/// Compare the result numbers with the given expected numbers.
+/// The `test_tuples` consist of tuples <formula, num_total, num_colors, num_states>.
+fn compare_mc_results_with_expected(test_tuples: Vec<(&str, f64, f64, f64)>, bn: BooleanNetwork) {
+    // test formulae use 3 HCTL vars at most
+    let stg = get_extended_symbolic_graph(&bn, 3).unwrap();
+
+    for (formula, num_total, num_colors, num_states) in test_tuples {
+        let result = model_check_formula(formula.to_string(), &stg).unwrap();
+        assert_eq!(num_total, result.approx_cardinality());
+        assert_eq!(num_colors, result.colors().approx_cardinality());
+        assert_eq!(num_states, result.vertices().approx_cardinality());
+
+        let result = model_check_formula_dirty(formula.to_string(), &stg).unwrap();
+        assert_eq!(num_total, result.approx_cardinality());
+        assert_eq!(num_colors, result.colors().approx_cardinality());
+        assert_eq!(num_states, result.vertices().approx_cardinality());
+    }
+}
+
+#[test]
+/// Test evaluation of several important formulae on model FISSION-YEAST-2008.
+/// Compare numbers of results with the numbers acquired by Python model checker or AEON.
+fn model_check_basic_yeast() {
+    // tuples consisting of <formula, num_total, num_colors, num_states>
+    // num_x are numbers of expected results
+    let test_tuples = vec![
+        ("!{x}: AG EF {x}", 12., 1., 12.),
+        ("!{x}: AX {x}", 12., 1., 12.),
+        ("!{x}: AX EF {x}", 68., 1., 68.),
+        ("AF (!{x}: AX {x})", 60., 1., 60.),
+        ("!{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y})", 12., 1., 12.),
+        ("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})))", 11., 1., 11.),
+        ("!{x}: (AX (AF {x}))", 12., 1., 12.),
+        ("AF (!{x}: (AX (~{x} & AF {x})))", 0., 0., 0.),
+        ("AF (!{x}: ((AX (~{x} & AF {x})) & (EF (!{y}: EX ~AF {y}))))", 0., 0., 0.),
+        // TODO: more tests regarding formulae for inference using concrete observations
+    ];
+
+    // model is in bnet format
+    let bn = BooleanNetwork::try_from_bnet(MODEL_YEAST).unwrap();
+    compare_mc_results_with_expected(test_tuples, bn);
+}
+
+#[test]
+/// Test evaluation of several important formulae on model MAMMALIAN-CELL-CYCLE-2006.
+/// Compare numbers of results with the numbers acquired by Python model checker or AEON.
+fn model_check_basic_mammal() {
+    // tuples consisting of <formula, num_total, num_colors, num_states>
+    // num_x are numbers of expected results
+    let test_tuples = vec![
+        ("!{x}: AG EF {x}", 113., 2., 113.),
+        ("!{x}: AX {x}", 1., 1., 1.),
+        ("!{x}: AX EF {x}", 425., 2., 425.),
+        ("AF (!{x}: AX {x})", 32., 1., 32.),
+        ("!{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y})", 0., 0., 0.),
+        ("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})))", 0., 0., 0.),
+        ("!{x}: (AX (AF {x}))", 1., 1., 1.),
+        ("AF (!{x}: (AX (~{x} & AF {x})))", 0., 0., 0.),
+        ("AF (!{x}: ((AX (~{x} & AF {x})) & (EF (!{y}: EX ~AF {y}))))", 0., 0., 0.),
+        // TODO: more tests regarding formulae for inference using concrete observations
+    ];
+
+    // model is in bnet format
+    let bn = BooleanNetwork::try_from_bnet(MODEL_CELL_CYCLE).unwrap();
+    compare_mc_results_with_expected(test_tuples, bn);
+}
+
+#[test]
+/// Test evaluation of several important formulae on model ASYMMETRIC-CELL-DIVISION-B.
+/// Compare numbers of results with the numbers acquired by Python model checker or AEON.
+fn model_check_basic_cell_division() {
+    // tuples consisting of <formula, num_total, num_colors, num_states>
+    // num_x are numbers of expected results
+    let test_tuples = vec![
+        ("!{x}: AG EF {x}", 1097728., 65536., 512.),
+        ("!{x}: AX {x}", 65536., 53248., 64.),
+        ("!{x}: AX EF {x}", 1499136., 65536., 512.),
+        ("AF (!{x}: AX {x})", 21430272., 53248., 512.),
+        ("!{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y})", 24576., 12288., 64.),
+        ("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})))", 24576., 12288., 48.),
+        ("!{x}: (AX (AF {x}))", 84992., 59392., 112.),
+        ("AF (!{x}: (AX (~{x} & AF {x})))", 49152., 6144., 128.),
+        ("AF (!{x}: ((AX (~{x} & AF {x})) & (EF (!{y}: EX ~AF {y}))))", 28672., 3584., 128.),
+        // TODO: more tests regarding formulae for inference using concrete observations
+    ];
+
+    // model is in aeon format
+    let bn = BooleanNetwork::try_from(MODEL_CELL_DIVISION).unwrap();
+    compare_mc_results_with_expected(test_tuples, bn);
+}

src/_test_model_checking/_test_extended_formulae.rs

@@ -0,0 +1,110 @@
+use crate::_test_model_checking::{MODEL_CELL_CYCLE, MODEL_CELL_DIVISION, MODEL_YEAST};
+use crate::mc_utils::get_extended_symbolic_graph;
+use crate::model_checking::{
+    model_check_extended_formula, model_check_formula, model_check_formula_dirty,
+};
+use biodivine_lib_param_bn::BooleanNetwork;
+use std::collections::HashMap;
+
+#[test]
+/// Test evaluation of (very simple) extended formulae, where special propositions are
+/// evaluated as various simple pre-computed sets.
+fn model_check_extended_simple() {
+    let bn = BooleanNetwork::try_from(MODEL_CELL_DIVISION).unwrap();
+    let stg = get_extended_symbolic_graph(&bn, 1).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_props = HashMap::from([("s".to_string(), result_sub)]);
+    let context_domains = HashMap::new();
+    let result_v2 =
+        model_check_extended_formula(formula_v2, &stg, &context_props, &context_domains).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_props = HashMap::from([("s".to_string(), result_sub)]);
+    let context_domains = HashMap::new();
+    let result_v2 =
+        model_check_extended_formula(formula_v2, &stg, &context_props, &context_domains).unwrap();
+    assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true());
+}
+
+/// Evaluate extended HCTL formulae, in which `wild-card properties` can represent already
+/// pre-computed results. Compare with the equivalent computation that does the whole computation
+/// in one step (without semantic substitution).
+fn model_check_extended_complex_on_bn(bn: BooleanNetwork) {
+    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_props = HashMap::from([("subst".to_string(), raw_set)]);
+    let context_domains = HashMap::new();
+
+    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_props,
+        &context_domains,
+    )
+    .unwrap();
+    let result2_v2 = model_check_extended_formula(
+        formula2_v2.to_string(),
+        &stg,
+        &context_props,
+        &context_domains,
+    )
+    .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 empty_context = HashMap::new();
+    let result1_v2 =
+        model_check_extended_formula(formula1.to_string(), &stg, &empty_context, &empty_context)
+            .unwrap();
+    let result2_v2 =
+        model_check_extended_formula(formula2.to_string(), &stg, &empty_context, &empty_context)
+            .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 model_check_extended_complex() {
+    let bn1 = BooleanNetwork::try_from(MODEL_CELL_DIVISION).unwrap();
+    let bn2 = BooleanNetwork::try_from_bnet(MODEL_CELL_CYCLE).unwrap();
+    let bn3 = BooleanNetwork::try_from_bnet(MODEL_YEAST).unwrap();
+
+    model_check_extended_complex_on_bn(bn1);
+    model_check_extended_complex_on_bn(bn2);
+    model_check_extended_complex_on_bn(bn3);
+}