Skip to content

Commit

Permalink
Merge arguments for raw sets for wild-card properties and variable do…
Browse files Browse the repository at this point in the history 
…mains
  • Loading branch information
@ondrej33
ondrej33 committed Feb 2, 2024
1 parent fd684c1 commit 691eeb2
Show file tree
Hide file tree
Showing 5 changed files with 126 additions and 149 deletions.
86 changes: 57 additions & 29 deletions src/_test_model_checking/_test_extended_formulae.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
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,
model_check_extended_formula, model_check_extended_formula_dirty, model_check_formula,
model_check_formula_dirty,
};
use biodivine_lib_param_bn::BooleanNetwork;
use std::collections::HashMap;
Expand All @@ -21,10 +22,8 @@ fn model_check_extended_simple() {
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();
let context_sets = HashMap::from([("s".to_string(), result_sub)]);
let result_v2 = model_check_extended_formula(formula_v2, &stg, &context_sets).unwrap();
assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true());

// 2) second test, disjunction substituted
Expand All @@ -35,10 +34,8 @@ fn model_check_extended_simple() {
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();
let context_sets = HashMap::from([("s".to_string(), result_sub)]);
let result_v2 = model_check_extended_formula(formula_v2, &stg, &context_sets).unwrap();
assert!(result_v1.as_bdd().iff(result_v2.as_bdd()).is_true());
}

Expand All @@ -60,25 +57,14 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) {
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 context_sets = 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_props,
&context_domains,
)
.unwrap();
let result2_v2 = model_check_extended_formula(
formula2_v2.to_string(),
&stg,
&context_props,
&context_domains,
)
.unwrap();
let result1_v2 =
model_check_extended_formula(formula1_v2.to_string(), &stg, &context_sets).unwrap();
let result2_v2 =
model_check_extended_formula(formula2_v2.to_string(), &stg, &context_sets).unwrap();

assert!(result1.as_bdd().iff(result1_v2.as_bdd()).is_true());
assert!(result2.as_bdd().iff(result2_v2.as_bdd()).is_true());
Expand All @@ -87,11 +73,9 @@ fn model_check_extended_complex_on_bn(bn: BooleanNetwork) {
// 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();
model_check_extended_formula(formula1.to_string(), &stg, &empty_context).unwrap();
let result2_v2 =
model_check_extended_formula(formula2.to_string(), &stg, &empty_context, &empty_context)
.unwrap();
model_check_extended_formula(formula2.to_string(), &stg, &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());
}
Expand All @@ -108,3 +92,47 @@ fn model_check_extended_complex() {
model_check_extended_complex_on_bn(bn2);
model_check_extended_complex_on_bn(bn3);
}

/// Test checking tautology or contradiction formulae that contain both wild-card properties
/// and variable domains.
fn model_check_extended_tautologies_on_bn(bn: BooleanNetwork) {
let formula = "!{x}: AG EF {x}".to_string();
let stg = get_extended_symbolic_graph(&bn, 1).unwrap();

// we must use 'dirty' version to avoid sanitation (BDDs must retain all symbolic vars)
let raw_set = model_check_formula_dirty(formula, &stg).unwrap();

let formulas = [
"V{x} in %1%: @{x}: (%1% & %2%)",
"V{x} in %1%: @{x}: (%2% & %3%)",
"V{x} in %2%: @{x}: (%2% & %3%)",
];

// context with three entries of the same set
let context = HashMap::from([
("1".to_string(), raw_set.clone()),
("2".to_string(), raw_set.clone()),
("3".to_string(), raw_set.clone()),
]);

for f in formulas {
let result = model_check_extended_formula_dirty(f.to_string(), &stg, &context).unwrap();
assert!(result
.as_bdd()
.iff(stg.unit_colored_vertices().as_bdd())
.is_true());
}
}

#[test]
/// Test checking tautology or contradiction formulae that contain both wild-card properties
/// and variable domains. Use all 3 pre-defined models.
fn model_check_extended_tautologies() {
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_tautologies_on_bn(bn1);
model_check_extended_tautologies_on_bn(bn2);
model_check_extended_tautologies_on_bn(bn3);
}
8 changes: 3 additions & 5 deletions src/_test_model_checking/_test_pattern_equivalences.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use std::collections::HashMap;

/// Test evaluation of pairs of equivalent pattern formulae on given BN model.
/// The patterns (wild-card propositions) are evaluated to raw sets specified by `context`.
fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context: LabelToSetMap) {
fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context_sets: LabelToSetMap) {
let equivalent_pattern_pairs = vec![
// AU equivalence
(
Expand All @@ -29,10 +29,8 @@ fn evaluate_equivalent_formulae_in_context(stg: &SymbolicAsyncGraph, context: La
];

for (f1, f2) in equivalent_pattern_pairs {
let result1 =
model_check_extended_formula(f1.to_string(), stg, &context, &HashMap::new()).unwrap();
let result2 =
model_check_extended_formula(f2.to_string(), stg, &context, &HashMap::new()).unwrap();
let result1 = model_check_extended_formula(f1.to_string(), stg, &context_sets).unwrap();
let result2 = model_check_extended_formula(f2.to_string(), stg, &context_sets).unwrap();
assert!(result1.as_bdd().iff(result2.as_bdd()).is_true());
}
}
Expand Down
43 changes: 12 additions & 31 deletions src/_test_model_checking/_test_variable_domains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,21 +43,14 @@ fn model_check_with_domains() {

for (f, f_with_domain) in formulae_pairs {
// eval the variant without domain first (contains wild-card prop)
let ctx_props = HashMap::from([("s".to_string(), raw_set.clone())]);
let ctx_doms = HashMap::new();
let res = model_check_extended_formula(f.to_string(), &stg, &ctx_props, &ctx_doms)
.unwrap();
let ctx_sets = HashMap::from([("s".to_string(), raw_set.clone())]);
let res = model_check_extended_formula(f.to_string(), &stg, &ctx_sets).unwrap();

// eval the variant with a domain
let ctx_props = HashMap::new();
let ctx_doms = HashMap::from([("s".to_string(), raw_set.clone())]);
let res_v2 = model_check_extended_formula(
f_with_domain.to_string(),
&stg,
&ctx_props,
&ctx_doms,
)
.unwrap();
let ctx_sets = HashMap::from([("s".to_string(), raw_set.clone())]);
let res_v2 =
model_check_extended_formula(f_with_domain.to_string(), &stg, &ctx_sets)
.unwrap();
assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
}
}
Expand All @@ -79,21 +72,14 @@ fn model_check_with_empty_domain() {
];

let empty_set = stg.mk_empty_colored_vertices();
let context_domains = HashMap::from([("s".to_string(), empty_set)]);
let context_props = HashMap::new();
let context = HashMap::from([("s".to_string(), empty_set)]);

for (f, domain_f) in formulae_pairs {
// eval the variant without domain first
let res = model_check_formula(f.to_string(), &stg).unwrap();

// and now the variant with empty domain
let res_v2 = model_check_extended_formula(
domain_f.to_string(),
&stg,
&context_props,
&context_domains,
)
.unwrap();
let res_v2 = model_check_extended_formula(domain_f.to_string(), &stg, &context).unwrap();

assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
}
Expand Down Expand Up @@ -151,23 +137,18 @@ fn model_check_with_domains_complex() {

for (f1, f2) in formulae_pairs {
// eval the variant with a domain
let ctx_props = HashMap::new();
let ctx_doms = HashMap::from([
let context = HashMap::from([
("s1".to_string(), raw_set_1.clone()),
("s2".to_string(), raw_set_2.clone()),
]);
let res_v2 =
model_check_extended_formula(f1.to_string(), &stg, &ctx_props, &ctx_doms)
.unwrap();
let res_v2 = model_check_extended_formula(f1.to_string(), &stg, &context).unwrap();

// eval the variant without domain (contains wild-card prop)
let ctx_props = HashMap::from([
let context = HashMap::from([
("s1".to_string(), raw_set_1.clone()),
("s2".to_string(), raw_set_2.clone()),
]);
let ctx_doms = HashMap::new();
let res = model_check_extended_formula(f2.to_string(), &stg, &ctx_props, &ctx_doms)
.unwrap();
let res = model_check_extended_formula(f2.to_string(), &stg, &context).unwrap();

assert!(res.as_bdd().iff(res_v2.as_bdd()).is_true());
}
Expand Down
Loading

0 comments on commit 691eeb2

Please sign in to comment.