Computation of minimal trap spaces (#51)

* Update dependencies.

* Basic utility updates.

* `OwnedSymbolicIterator` and other iteration-related updates.

* Actual implementation of minimal trap space search.

* Use `BddSet` more.

* Actually add the test model.

* Add `maximize` routine as a counterpart to `minimize`.

* Add some additional basic tests.

* Extend basic tests.

* Rename confusing projection argument.

Cargo.toml

@@ -42,10 +42,10 @@ solver-z3 = ["dep:z3"]
 [dependencies]
 regex = "1.10.2"                # Regexes used for parsing of basic .aeon constructs.
 lazy_static = "1.4.0"           # Used for initialization of commonly used regexes.
-biodivine-lib-bdd = ">=0.5.2, <1.0.0"
+biodivine-lib-bdd = ">=0.5.6, <1.0.0"
 num-bigint = "0.4.4"            # Used as infinite-precision representation in BDDs.
 num-traits = "0.2.17"          # `BigInt::to_f64`
-roxmltree = "0.18.1"            # Used for SBML parsing.
+roxmltree = "0.19.0"            # Used for SBML parsing.
 bitvector = "0.1.5"             # Represents Boolean states of complex networks.
 z3 = { version = "0.12.1", optional = true }     # Used for fixed-point enumeration (and hopefully other things soon).
 

aeon_models/005.aeon

@@ -0,0 +1,151 @@
+v_BRCA1 -> v_FANCD1N
+v_CHKREC -| v_FANCD1N
+v_ssDNARPA -> v_FANCD1N
+v_FANCD2I -> v_FANCD1N
+v_ATM -> v_BRCA1
+v_CHK2 -> v_BRCA1
+v_DSB -> v_BRCA1
+v_ATR -> v_BRCA1
+v_CHKREC -| v_BRCA1
+v_DSB -> v_ATM
+v_ATR -> v_ATM
+v_CHKREC -| v_ATM
+v_ATM -> v_FANCD2I
+v_FAcore -> v_FANCD2I
+v_DSB -> v_FANCD2I
+v_ATR -> v_FANCD2I
+v_H2AX -> v_FANCD2I
+v_USP1 -| v_FANCD2I
+v_FAcore ->? v_PCNATLS
+v_FAN1 -| v_PCNATLS
+v_ADD -> v_PCNATLS
+v_USP1 -| v_PCNATLS
+v_BRCA1 -> v_HRR
+v_FANCD1N -> v_HRR
+v_DSB -> v_HRR
+v_RAD51 -> v_HRR
+v_CHKREC -| v_HRR
+v_DSB -> v_DNAPK
+v_KU -> v_DNAPK
+v_CHKREC -| v_DNAPK
+v_ATM -> v_MRN
+v_DSB -> v_MRN
+v_KU -| v_MRN
+v_RAD51 -| v_MRN
+v_CHKREC -| v_MRN
+v_FANCD2I -? v_MRN
+v_ATM -| v_NHEJ
+v_DNAPK -> v_NHEJ
+v_DSB -> v_NHEJ
+v_ATR -? v_NHEJ
+v_KU -> v_NHEJ
+v_CHKREC -| v_NHEJ
+v_FANCJBRCA1 -| v_NHEJ
+v_ssDNARPA -? v_NHEJ
+v_XPF -> v_NHEJ
+v_MRN -| v_KU
+v_DSB -> v_KU
+v_CHKREC -| v_KU
+v_FANCD2I -| v_KU
+v_ICL -> v_FANCM
+v_CHKREC -| v_FANCM
+v_ATM -> v_CHK2
+v_DNAPK -> v_CHK2
+v_ATR -> v_CHK2
+v_CHKREC -| v_CHK2
+v_ATM -> v_H2AX
+v_DNAPK -> v_H2AX
+v_DSB -> v_H2AX
+v_ATR -> v_H2AX
+v_CHKREC -| v_H2AX
+v_NHEJ -| v_DSB
+v_HRR -| v_DSB
+v_DSB -> v_DSB
+v_FAN1 -> v_DSB
+v_XPF -> v_DSB
+v_NHEJ -> v_CHKREC
+v_ICL -| v_CHKREC
+v_PCNATLS -> v_CHKREC
+v_HRR -> v_CHKREC
+v_DSB -| v_CHKREC
+v_CHKREC -| v_CHKREC
+v_ADD -| v_CHKREC
+v_MRN -> v_ssDNARPA
+v_DSB -> v_ssDNARPA
+v_KU -| v_ssDNARPA
+v_RAD51 -| v_ssDNARPA
+v_FANCJBRCA1 -> v_ssDNARPA
+v_FANCD2I -> v_ssDNARPA
+v_ATM -> v_FAcore
+v_FANCM -> v_FAcore
+v_ATR -> v_FAcore
+v_CHKREC -| v_FAcore
+v_FANCM -| v_USP1
+v_FANCD1N -> v_USP1
+v_PCNATLS -> v_USP1
+v_FANCD2I -> v_USP1
+v_ATM -> v_FANCJBRCA1
+v_ICL -> v_FANCJBRCA1
+v_ATR -> v_FANCJBRCA1
+v_ssDNARPA -> v_FANCJBRCA1
+v_FANCM -| v_XPF
+v_p53 -> v_XPF
+v_MUS81 -> v_XPF
+v_FAcore -| v_XPF
+v_FAN1 -? v_XPF
+v_FANCD2I -? v_XPF
+v_ICL -> v_MUS81
+v_ATM -> v_CHK1
+v_DNAPK -> v_CHK1
+v_ATR -> v_CHK1
+v_CHKREC -| v_CHK1
+v_ATM -> v_p53
+v_CHK2 -> v_p53
+v_DNAPK -> v_p53
+v_ATR -> v_p53
+v_CHKREC -| v_p53
+v_CHK1 -> v_p53
+v_PCNATLS -| v_ADD
+v_MUS81 -> v_ADD
+v_FAN1 -> v_ADD
+v_ADD -> v_ADD
+v_XPF -> v_ADD
+v_ICL -> v_ICL
+v_DSB -| v_ICL
+v_FANCD1N -> v_RAD51
+v_CHKREC -| v_RAD51
+v_ssDNARPA -> v_RAD51
+v_ATM -> v_ATR
+v_FANCM -> v_ATR
+v_CHKREC -| v_ATR
+v_ssDNARPA -> v_ATR
+v_MUS81 -> v_FAN1
+v_FANCD2I -> v_FAN1
+$v_ADD: ((v_ADD & !v_PCNATLS) | ((v_MUS81 & (v_FAN1 | v_XPF)) & !v_PCNATLS))
+$v_ATM: ((v_DSB & !v_CHKREC) | (v_ATR & !v_CHKREC))
+$v_ATR: (((v_FANCM & !v_CHKREC) | (v_ATM & !v_CHKREC)) | (v_ssDNARPA & !v_CHKREC))
+$v_BRCA1: ((v_DSB & ((v_ATM | v_CHK2) | v_ATR)) & !v_CHKREC)
+$v_CHK1: (((v_ATM & !v_CHKREC) | (v_DNAPK & !v_CHKREC)) | (v_ATR & !v_CHKREC))
+$v_CHK2: (((v_ATM & !v_CHKREC) | (v_DNAPK & !v_CHKREC)) | (v_ATR & !v_CHKREC))
+$v_CHKREC: ((((v_PCNATLS & !v_DSB) | (v_NHEJ & !v_DSB)) | (v_HRR & !v_DSB)) | !((((((v_NHEJ | v_ICL) | v_PCNATLS) | v_HRR) | v_DSB) | v_CHKREC) | v_ADD))
+$v_DNAPK: ((v_DSB & v_KU) & !v_CHKREC)
+$v_DSB: (((v_XPF & !(v_HRR | v_NHEJ)) | (v_DSB & !(v_HRR | v_NHEJ))) | (v_FAN1 & !(v_HRR | v_NHEJ)))
+$v_FAN1: (v_MUS81 & v_FANCD2I)
+$v_FANCD1N: ((v_ssDNARPA & v_BRCA1) | ((v_FANCD2I & v_ssDNARPA) & !v_CHKREC))
+$v_FANCD2I: ((v_FAcore & ((v_ATM | v_ATR) | (v_DSB & v_H2AX))) & !v_USP1)
+$v_FANCJBRCA1: ((v_ssDNARPA & (v_ATM | v_ATR)) | (v_ICL & (v_ATM | v_ATR)))
+$v_FANCM: (v_ICL & !v_CHKREC)
+$v_FAcore: ((v_FANCM & (v_ATM | v_ATR)) & !v_CHKREC)
+$v_H2AX: ((v_DSB & ((v_ATM | v_DNAPK) | v_ATR)) & !v_CHKREC)
+$v_HRR: ((v_DSB & ((v_BRCA1 & v_FANCD1N) & v_RAD51)) & !v_CHKREC)
+$v_ICL: (v_ICL & !v_DSB)
+$v_KU: (v_DSB & !((v_CHKREC | v_MRN) | v_FANCD2I))
+$v_MRN: ((v_DSB & v_ATM) & !((v_RAD51 | (v_KU & v_FANCD2I)) | v_CHKREC))
+$v_MUS81: v_ICL
+$v_NHEJ: (((v_KU & (v_DNAPK & v_DSB)) & !(v_ATM & v_ATR)) | ((v_XPF & (v_DNAPK & v_DSB)) & !((v_FANCJBRCA1 & v_ssDNARPA) | v_CHKREC)))
+$v_PCNATLS: (((v_FAcore & v_ADD) & !(v_FAN1 | v_USP1)) | (v_ADD & !(v_FAN1 | v_USP1)))
+$v_RAD51: ((v_ssDNARPA & v_FANCD1N) & !v_CHKREC)
+$v_USP1: (((v_FANCD1N & v_FANCD2I) & !v_FANCM) | (v_PCNATLS & !v_FANCM))
+$v_XPF: (((v_p53 & v_MUS81) & !(v_FAcore & (v_FAN1 & v_FANCD2I))) | (v_MUS81 & !v_FANCM))
+$v_p53: ((((v_ATM & v_CHK2) & !v_CHKREC) | ((v_ATR & v_CHK1) & !v_CHKREC)) | (v_DNAPK & !v_CHKREC))
+$v_ssDNARPA: ((v_DSB & ((v_FANCJBRCA1 & v_FANCD2I) | v_MRN)) & !(v_KU | v_RAD51))

src/_impl_extended_boolean.rs

@@ -22,6 +22,15 @@ impl From<bool> for ExtendedBoolean {
     }
 }
 
+impl From<Option<bool>> for ExtendedBoolean {
+    fn from(value: Option<bool>) -> Self {
+        match value {
+            Some(value) => ExtendedBoolean::from(value),
+            None => Any,
+        }
+    }
+}
+
 impl Display for ExtendedBoolean {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         write!(f, "{:?}", self)
@@ -61,7 +70,6 @@ impl ExtendedBoolean {
 }
 
 /// Logical operations on extended booleans.
-
 impl ExtendedBoolean {
     pub fn negate(self) -> Self {
         match self {

src/_impl_space.rs

@@ -57,7 +57,7 @@ impl Space {
         Space(vec![Any; network.num_vars()])
     }
 
-    /// Convert a list of values (such as used by `SymbolicAsyncGraph`) into a proper "space".
+    /// Convert a list of values (such as used by `SymbolicAsyncGraph`) into a proper "space" object.
     pub fn from_values(bn: &BooleanNetwork, values: Vec<(VariableId, bool)>) -> Space {
         let mut result = Self::new(bn);
         for (k, v) in values {
@@ -66,6 +66,7 @@ impl Space {
         result
     }
 
+    /// Convert a space into a list of values compatible with the normal `SymbolicAsyncGraph`.
     pub fn to_values(&self) -> Vec<(VariableId, bool)> {
         let mut result = Vec::new();
         for (k, v) in self.0.iter().enumerate() {
@@ -76,6 +77,7 @@ impl Space {
         result
     }
 
+    /// Try to intersect two spaces. If the result is empty, returns `None`.
     pub fn intersect(&self, other: &Space) -> Option<Space> {
         let mut result = self.clone();
         for i in 0..self.0.len() {
@@ -97,7 +99,13 @@ impl Space {
         Some(result)
     }
 
+    /// Count the number of `*` in this space.
     pub fn count_any(&self) -> usize {
         self.0.iter().filter(|it| **it == Any).count()
     }
+
+    /// Count the number of `0` and `1` in this space.
+    pub fn count_fixed(&self) -> usize {
+        self.0.iter().filter(|it| **it != Any).count()
+    }
 }

src/bin/bench_trap_spaces_minimal.rs

@@ -0,0 +1,25 @@
+use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
+use biodivine_lib_param_bn::trap_spaces::{SymbolicSpaceContext, TrapSpaces};
+use biodivine_lib_param_bn::BooleanNetwork;
+
+fn main() {
+    let args = std::env::args().collect::<Vec<_>>();
+    let bn = BooleanNetwork::try_from_file(args[1].as_str()).unwrap();
+    let ctx = SymbolicSpaceContext::new(&bn);
+    let stg = SymbolicAsyncGraph::with_space_context(bn.clone(), &ctx).unwrap();
+
+    let unit_set = ctx.mk_unit_colored_spaces(&stg);
+    let essential_traps = TrapSpaces::essential_symbolic(&bn, &ctx, &unit_set);
+    println!(
+        "Found {} essential trap(s).",
+        essential_traps.approx_cardinality()
+    );
+
+    let minimal_traps = TrapSpaces::minimize(&ctx, &essential_traps);
+    println!(
+        "Found {}/{}({}) minimal trap(s).",
+        minimal_traps.spaces().approx_cardinality(),
+        minimal_traps.colors().approx_cardinality(),
+        minimal_traps.approx_cardinality()
+    );
+}

src/lib.rs

@@ -24,6 +24,7 @@ pub mod sbml;
 #[cfg(feature = "solver-z3")]
 pub mod solver_context;
 pub mod symbolic_async_graph;
+pub mod trap_spaces;
 pub mod tutorial;
 
 /// **(internal)** Implements `.aeon` parser for `BooleanNetwork` and `RegulatoryGraph` objects.