-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #17 from sybila/dev-variable-domains
Add support for variable domains
- Loading branch information
Showing
43 changed files
with
2,728 additions
and
1,389 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
src/aeon/algo_xie_beerel.rs → src/_aeon_algorithms/algo_xie_beerel.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
4 changes: 2 additions & 2 deletions
4
src/aeon/itgr/_impl_fwd_bwd_process.rs → ..._algorithms/itgr/_impl_fwd_bwd_process.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
File renamed without changes.
File renamed without changes.
File renamed without changes.
4 changes: 2 additions & 2 deletions
4
src/aeon/scc_computation.rs → src/_aeon_algorithms/scc_computation.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } |
Oops, something went wrong.