diff --git a/Cargo.toml b/Cargo.toml index 8ac7528..d7d0d00 100644 --- a/Cargo.toml +++ b/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). diff --git a/aeon_models/005.aeon b/aeon_models/005.aeon new file mode 100644 index 0000000..8641cdf --- /dev/null +++ b/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)) diff --git a/src/_impl_extended_boolean.rs b/src/_impl_extended_boolean.rs index 8b16784..9b662eb 100644 --- a/src/_impl_extended_boolean.rs +++ b/src/_impl_extended_boolean.rs @@ -22,6 +22,15 @@ impl From for ExtendedBoolean { } } +impl From> for ExtendedBoolean { + fn from(value: Option) -> 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 { diff --git a/src/_impl_space.rs b/src/_impl_space.rs index 6200f9f..6e9391f 100644 --- a/src/_impl_space.rs +++ b/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 { 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() + } } diff --git a/src/bin/bench_trap_spaces_minimal.rs b/src/bin/bench_trap_spaces_minimal.rs new file mode 100644 index 0000000..46fae55 --- /dev/null +++ b/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::>(); + 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() + ); +} diff --git a/src/lib.rs b/src/lib.rs index c2886e9..7f4e762 100644 --- a/src/lib.rs +++ b/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. diff --git a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs index a6498d5..20fbe3f 100644 --- a/src/symbolic_async_graph/_impl_graph_colored_vertices.rs +++ b/src/symbolic_async_graph/_impl_graph_colored_vertices.rs @@ -9,8 +9,6 @@ use crate::symbolic_async_graph::{ use crate::VariableId; use biodivine_lib_bdd::{Bdd, BddVariable}; use num_bigint::BigInt; -use num_traits::ToPrimitive; -use std::ops::Shr; /// Basic utility operations. impl GraphColoredVertices { @@ -52,19 +50,17 @@ impl GraphColoredVertices { /// Amount of storage used for this symbolic set. pub fn symbolic_size(&self) -> usize { - self.bdd.size() + BddSet::symbolic_size(self) } /// Approximate size of this set (error grows for large sets). pub fn approx_cardinality(&self) -> f64 { - self.exact_cardinality().to_f64().unwrap_or(f64::INFINITY) + BddSet::approx_cardinality(self) } /// Compute exact `BigInt` cardinality of this set. pub fn exact_cardinality(&self) -> BigInt { - let unused_variables = self.bdd.num_vars() - - u16::try_from(self.state_variables.len() + self.parameter_variables.len()).unwrap(); - self.bdd.exact_cardinality().shr(unused_variables) + BddSet::exact_cardinality(self) } /// Return `true` if the set can be described by a single conjunction of literals. That is, @@ -75,7 +71,22 @@ impl GraphColoredVertices { /// Return `true` if the set represents a single vertex-color pair. pub fn is_singleton(&self) -> bool { - self.bdd.is_valuation() + if self.bdd.is_clause() { + let clause = self.bdd.first_clause().unwrap(); + for var in &self.state_variables { + if clause[*var].is_none() { + return false; + } + } + for var in &self.parameter_variables { + if clause[*var].is_none() { + return false; + } + } + true + } else { + false + } } /// Compute a subset of this set where the given network variable is always fixed to the @@ -99,15 +110,15 @@ impl GraphColoredVertices { /// /// Technically, you can supply any `BddVariable`, but the underlying `Bdd` of this set /// should only depend on *state and parameter variables* (i.e. not on extra state variables). - pub fn raw_projection(&self, variables: &[BddVariable]) -> RawProjection { + pub fn raw_projection(&self, eliminate: &[BddVariable]) -> RawProjection { let mut retained = Vec::new(); for v in &self.state_variables { - if !variables.contains(v) { + if !eliminate.contains(v) { retained.push(*v); } } for v in &self.parameter_variables { - if !variables.contains(v) { + if !eliminate.contains(v) { retained.push(*v); } } @@ -180,7 +191,16 @@ impl GraphColoredVertices { if self.is_empty() { self.clone() } else { - self.copy(self.bdd.sat_witness().unwrap().into()) + let witness = self.bdd.sat_witness().unwrap(); + // Retain only the relevant variables. + let mut partial_valuation = Vec::new(); + for s_var in &self.state_variables { + partial_valuation.push((*s_var, witness[*s_var])); + } + for p_var in &self.parameter_variables { + partial_valuation.push((*p_var, witness[*p_var])); + } + self.copy(self.bdd.select(&partial_valuation)) } } @@ -214,3 +234,54 @@ impl BddSet for GraphColoredVertices { u16::try_from(self.state_variables.len() + self.parameter_variables.len()).unwrap() } } + +#[cfg(test)] +mod tests { + use crate::biodivine_std::traits::Set; + use crate::symbolic_async_graph::SymbolicAsyncGraph; + use crate::BooleanNetwork; + use num_bigint::BigInt; + use num_traits::One; + + #[test] + fn basic_colored_spaces_set_test() { + let bn = BooleanNetwork::try_from_file("aeon_models/005.aeon").unwrap(); + let stg = SymbolicAsyncGraph::new(bn.clone()).unwrap(); + + let unit = stg.mk_unit_colored_vertices(); + assert!(!unit.is_singleton()); + assert_eq!(unit, unit.copy(unit.clone().into_bdd())); + + let singleton = unit.pick_singleton(); + assert_eq!(1.0, singleton.approx_cardinality()); + assert_eq!(BigInt::one(), singleton.exact_cardinality()); + let singleton_color = singleton.colors(); + let singleton_vertices = singleton.vertices(); + assert!(singleton_color.is_singleton()); + assert!(singleton_vertices.is_singleton()); + assert!(!unit.intersect_colors(&singleton_color).is_singleton()); + // There is only one color, hence this holds. Otherwise this should not hold. + assert!(unit.intersect_vertices(&singleton_vertices).is_singleton()); + assert!(unit.minus_colors(&singleton_color).is_empty()); + assert!(unit.minus_vertices(&singleton_vertices).is_subset(&unit)); + + let var = bn.as_graph().find_variable("v_XPF").unwrap(); + let selected = unit.fix_network_variable(var, true); + assert_eq!( + unit.approx_cardinality() / 2.0, + selected.approx_cardinality() + ); + let restricted = unit.restrict_network_variable(var, true); + assert_eq!(unit.approx_cardinality(), restricted.approx_cardinality()); + let restricted = singleton.restrict_network_variable(var, false); + assert_eq!( + singleton.approx_cardinality() * 2.0, + restricted.approx_cardinality() + ); + assert!(singleton.restrict_network_variable(var, true).is_empty()); + + // There are 28 variables and we are eliminating 22 of them, so 6 should be left. + let project = unit.raw_projection(&stg.symbolic_context().state_variables()[0..22]); + assert_eq!(project.iter().count(), 2_usize.pow(6)); + } +} diff --git a/src/symbolic_async_graph/_impl_graph_colors.rs b/src/symbolic_async_graph/_impl_graph_colors.rs index cd9f52d..458c7b0 100644 --- a/src/symbolic_async_graph/_impl_graph_colors.rs +++ b/src/symbolic_async_graph/_impl_graph_colors.rs @@ -5,9 +5,7 @@ use crate::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph, SymbolicConte use crate::VariableId; use biodivine_lib_bdd::{Bdd, BddVariable}; use num_bigint::BigInt; -use num_traits::ToPrimitive; use std::convert::TryFrom; -use std::ops::Shr; impl GraphColors { /// Make a new color set from a `bdd` and a symbolic `context`. @@ -56,20 +54,17 @@ impl GraphColors { /// Approximate size of this set (error grows for large sets). pub fn approx_cardinality(&self) -> f64 { - self.exact_cardinality().to_f64().unwrap_or(f64::INFINITY) + BddSet::approx_cardinality(self) } /// Compute exact `BigInt` cardinality of this set. pub fn exact_cardinality(&self) -> BigInt { - // Includes state variables and extra variables. - let unused_variables = - self.bdd.num_vars() - u16::try_from(self.parameter_variables.len()).unwrap(); - self.bdd.exact_cardinality().shr(unused_variables) + BddSet::exact_cardinality(self) } /// Amount of storage used for this symbolic set. pub fn symbolic_size(&self) -> usize { - self.bdd.size() + BddSet::symbolic_size(self) } /// Convert this set to a `.dot` graph. @@ -102,10 +97,10 @@ impl GraphColors { /// /// Technically, you can supply any `BddVariable`, but the underlying `Bdd` of this set /// should only depend on *parameter variables*. - pub fn raw_projection(&self, variables: &[BddVariable]) -> RawProjection { + pub fn raw_projection(&self, eliminate: &[BddVariable]) -> RawProjection { let mut retained = Vec::new(); for v in &self.parameter_variables { - if !variables.contains(v) { + if !eliminate.contains(v) { retained.push(*v); } } diff --git a/src/symbolic_async_graph/_impl_graph_vertices.rs b/src/symbolic_async_graph/_impl_graph_vertices.rs index f6f5ecd..84ec3d4 100644 --- a/src/symbolic_async_graph/_impl_graph_vertices.rs +++ b/src/symbolic_async_graph/_impl_graph_vertices.rs @@ -2,15 +2,11 @@ use crate::biodivine_std::bitvector::{ArrayBitVector, BitVector}; use crate::biodivine_std::traits::Set; use crate::symbolic_async_graph::bdd_set::BddSet; use crate::symbolic_async_graph::projected_iteration::{RawProjection, StateProjection}; -use crate::symbolic_async_graph::{ - GraphVertexIterator, GraphVertices, IterableVertices, SymbolicContext, -}; +use crate::symbolic_async_graph::{GraphVertexIterator, GraphVertices, SymbolicContext}; use crate::VariableId; -use biodivine_lib_bdd::{Bdd, BddValuation, BddVariable}; +use biodivine_lib_bdd::{Bdd, BddVariable}; use num_bigint::BigInt; -use num_traits::ToPrimitive; use std::convert::TryFrom; -use std::ops::Shr; impl GraphVertices { /// Create a new set of vertices using the given `Bdd` and a symbolic `context`. @@ -41,14 +37,12 @@ impl GraphVertices { /// Approximate size of this set (error grows for large sets). pub fn approx_cardinality(&self) -> f64 { - self.exact_cardinality().to_f64().unwrap_or(f64::INFINITY) + BddSet::approx_cardinality(self) } /// Compute exact `BigInt` cardinality of this set. pub fn exact_cardinality(&self) -> BigInt { - let unused_variables = - self.bdd.num_vars() - u16::try_from(self.state_variables.len()).unwrap(); - self.bdd.exact_cardinality().shr(unused_variables) + BddSet::exact_cardinality(self) } /// Pick one vertex from this set and return it as a singleton. @@ -73,19 +67,17 @@ impl GraphVertices { /// /// Note that sadly you have to use `set.materialize().iter()` to actually iterate over /// the vertices, since we are not moving our the value of this set. - pub fn materialize(&self) -> IterableVertices { - // This is a colossal hack, but it is easier than trying to drag parameter variables into this. - let all_false: Bdd = BddValuation::all_false(self.bdd.num_vars()).into(); - let parameters_false = all_false.exists(&self.state_variables); - IterableVertices { - materialized_bdd: self.bdd.and(¶meters_false), + #[allow(deprecated)] + pub fn materialize(&self) -> crate::symbolic_async_graph::IterableVertices { + crate::symbolic_async_graph::IterableVertices { + projection: RawProjection::new(self.state_variables.clone(), self.as_bdd()), state_variables: self.state_variables.clone(), } } /// Amount of storage used for this symbolic set. pub fn symbolic_size(&self) -> usize { - self.bdd.size() + BddSet::symbolic_size(self) } /// Convert this set to a `.dot` graph. @@ -135,10 +127,10 @@ impl GraphVertices { /// /// Technically, you can supply any `BddVariable`, but the underlying `Bdd` of this set /// should only depend on *state variables*. - pub fn raw_projection(&self, variables: &[BddVariable]) -> RawProjection { + pub fn raw_projection(&self, eliminate: &[BddVariable]) -> RawProjection { let mut retained = Vec::new(); for v in &self.state_variables { - if !variables.contains(v) { + if !eliminate.contains(v) { retained.push(*v); } } @@ -149,29 +141,51 @@ impl GraphVertices { pub fn state_projection(&self, variables: &[VariableId]) -> StateProjection { StateProjection::new(variables.to_vec(), &self.state_variables, &self.bdd) } + + /// Create an iterator equivalent to [GraphVertices::into_iter], but without destroying the + /// original object. + pub fn iter(&self) -> GraphVertexIterator { + let projection = RawProjection::new(self.state_variables.clone(), &self.bdd); + GraphVertexIterator { + inner_iterator: projection.into_iter(), + state_variables: self.state_variables.clone(), + } + } } -impl IterableVertices { +impl IntoIterator for GraphVertices { + type Item = ArrayBitVector; + type IntoIter = GraphVertexIterator; + + fn into_iter(self) -> Self::IntoIter { + let projection = RawProjection::new(self.state_variables.clone(), &self.bdd); + GraphVertexIterator { + inner_iterator: projection.into_iter(), + state_variables: self.state_variables, + } + } +} + +#[allow(deprecated)] +impl crate::symbolic_async_graph::IterableVertices { /// Turn this materialized vertex set into an actual iterator. pub fn iter(&self) -> GraphVertexIterator { - return GraphVertexIterator { - iterator: self.materialized_bdd.sat_valuations(), + GraphVertexIterator { + inner_iterator: self.projection.clone().into_iter(), state_variables: self.state_variables.clone(), - }; + } } } /// Iterate over vertices using `GraphVertexIterator`. -impl Iterator for GraphVertexIterator<'_> { +impl Iterator for GraphVertexIterator { type Item = ArrayBitVector; fn next(&mut self) -> Option { - if let Some(valuation) = self.iterator.next() { + if let Some(valuation) = self.inner_iterator.next() { let mut state = ArrayBitVector::empty(self.state_variables.len()); for (i, v) in self.state_variables.iter().enumerate() { - if valuation[*v] { - state.flip(i); - } + state.set(i, valuation[*v].unwrap()); } Some(state) } else { diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs index dd8f880..6dda911 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs +++ b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs @@ -5,6 +5,7 @@ use crate::symbolic_async_graph::bdd_set::BddSet; use crate::symbolic_async_graph::{ GraphColoredVertices, GraphColors, GraphVertices, SymbolicAsyncGraph, SymbolicContext, }; +use crate::trap_spaces::SymbolicSpaceContext; use crate::{BooleanNetwork, FnUpdate, VariableId}; use crate::{ExtendedBoolean, Space}; use biodivine_lib_bdd::{bdd, Bdd, BddVariable}; @@ -19,6 +20,18 @@ impl SymbolicAsyncGraph { Self::with_custom_context(network, context, unit) } + /// Create a [SymbolicAsyncGraph] that is compatible with an existing [SymbolicSpaceContext]. + /// + /// The `network` argument must be the same as used for the creation of the `context` object. + pub fn with_space_context( + network: BooleanNetwork, + context: &SymbolicSpaceContext, + ) -> Result { + let context = context.inner_context().clone(); + let unit = context.mk_constant(true); + Self::with_custom_context(network, context, unit) + } + /// Create a `SymbolicAsyncGraph` using a given `network`, the symbolic `context` (encoding) /// of said network (possibly with extra symbolic variables), and an initial `unit_bdd` which /// is used to restrict all valid BDDs corresponding to this graph. diff --git a/src/symbolic_async_graph/mod.rs b/src/symbolic_async_graph/mod.rs index 59362b6..ae8f7ed 100644 --- a/src/symbolic_async_graph/mod.rs +++ b/src/symbolic_async_graph/mod.rs @@ -28,10 +28,9 @@ //! any custom BDD operations, but it should be used with caution. //! +use crate::symbolic_async_graph::projected_iteration::{OwnedRawSymbolicIterator, RawProjection}; use crate::BooleanNetwork; -use biodivine_lib_bdd::{ - Bdd, BddSatisfyingValuations, BddVariable, BddVariableSet, ValuationsOfClauseIterator, -}; +use biodivine_lib_bdd::{Bdd, BddVariable, BddVariableSet, ValuationsOfClauseIterator}; use std::iter::Enumerate; /// **(internal)** Implementing conversion between `FnUpdate` and `BooleanExpression`. @@ -64,15 +63,15 @@ pub mod projected_iteration; /// /// These methods should eventually replace code that was previously duplicated across multiple /// set objects but is kept there for now due to compatibility. -mod bdd_set; +pub(crate) mod bdd_set; /// Symbolic representation of a color set. /// /// Implementation contains all symbolic variables, but state variables are unconstrained. #[derive(Clone, Eq, PartialEq, Hash, Debug)] pub struct GraphColors { - bdd: Bdd, - parameter_variables: Vec, + pub(crate) bdd: Bdd, + pub(crate) parameter_variables: Vec, } /// Symbolic representation of a coloured set of graph vertices, i.e. a subset of $V \times C$. @@ -97,15 +96,18 @@ pub struct GraphVertices { /// /// Internally, this struct contains a `Bdd` that has all parameter variables fixed to false, /// so that we only iterate over vertices and can safely disregard colors. +/// +/// **This object is now deprecated and you can call [GraphVertices::into_iter] directly.** #[derive(Clone)] +#[deprecated] pub struct IterableVertices { - materialized_bdd: Bdd, + projection: RawProjection, state_variables: Vec, } -/// Iterator over graph vertices. -pub struct GraphVertexIterator<'a> { - iterator: BddSatisfyingValuations<'a>, +/// Iterator over the states/vertices of a [GraphVertices] set. +pub struct GraphVertexIterator { + inner_iterator: OwnedRawSymbolicIterator, state_variables: Vec, } diff --git a/src/symbolic_async_graph/projected_iteration.rs b/src/symbolic_async_graph/projected_iteration.rs index b6882ee..8375bb0 100644 --- a/src/symbolic_async_graph/projected_iteration.rs +++ b/src/symbolic_async_graph/projected_iteration.rs @@ -38,6 +38,7 @@ use std::collections::HashSet; /// has all non-retained variables fixed to `False`. This ensures that when we iterate through /// its valuations, we do not repeat valuations that only differ in variables that /// are not retained. +#[derive(Clone)] pub struct RawProjection { retained_variables: Vec, bdd: Bdd, @@ -50,6 +51,27 @@ pub struct RawSymbolicIterator<'a> { inner_iterator: BddSatisfyingValuations<'a>, } +/// A version of [RawSymbolicIterator] which actually owns the underlying [RawProjection]. +/// This means the iterator is not tied to the lifetime of the projection. +/// +/// Note that due to our unfortunate API design, this `struct` has to use a minor "hack" to +/// make it work. In particular, we have to "fake" a `'static` lifetime on +/// the [BddSatisfyingValuations] iterator. In our case, this is safe because (a) we don't +/// leak the inner iterator anywhere, so the hack is contained to our private code, and (b) +/// we still own the original projection, so it actually lives as long as the iterator. +/// Finally, (c), the destruction of the iterator is passive and does not perform any actions +/// on the underlying projection (which may have been destroyed at this time, depending +/// on the destructor invocation order). +/// +/// Also note that the `Box` around `RawProjection` is essential! When we are constructing +/// the inner iterator, we need to reference the final memory location of the `RawProjection`. +/// Hence we need a heap pointer that will stay the same after we move the projection into +/// the [OwnedRawSymbolicIterator]. +pub struct OwnedRawSymbolicIterator { + raw_projection: Box, + inner_iterator: BddSatisfyingValuations<'static>, +} + impl RawProjection { /// Create a `RawProjection` from the given set of retained variables and a `Bdd`. /// @@ -81,18 +103,51 @@ impl RawProjection { } } +impl IntoIterator for RawProjection { + type Item = BddPartialValuation; + type IntoIter = OwnedRawSymbolicIterator; + + fn into_iter(self) -> Self::IntoIter { + let iterable = Box::new(self); + let static_iterable = unsafe { + (iterable.as_ref() as *const RawProjection) + .as_ref() + .unwrap() + }; + OwnedRawSymbolicIterator { + raw_projection: iterable, + inner_iterator: static_iterable.bdd.sat_valuations(), + } + } +} + +/// Restrict a BDD valuation only to the provided "retained" variables. +fn restrict_valuation(valuation: BddValuation, retain: &[BddVariable]) -> BddPartialValuation { + let mut partial = BddPartialValuation::empty(); + for var in retain { + partial.set_value(*var, valuation[*var]); + } + partial +} + impl<'a> Iterator for RawSymbolicIterator<'a> { type Item = BddPartialValuation; fn next(&mut self) -> Option { // Extract only the symbolic variables that are actually retained in this projection. - self.inner_iterator.next().map(|valuation| { - let mut partial_valuation = BddPartialValuation::empty(); - for var in &self.raw_projection.retained_variables { - partial_valuation.set_value(*var, valuation.value(*var)) - } - partial_valuation - }) + self.inner_iterator + .next() + .map(|valuation| restrict_valuation(valuation, &self.raw_projection.retained_variables)) + } +} + +impl Iterator for OwnedRawSymbolicIterator { + type Item = BddPartialValuation; + + fn next(&mut self) -> Option { + self.inner_iterator + .next() + .map(|valuation| restrict_valuation(valuation, &self.raw_projection.retained_variables)) } } diff --git a/src/trap_spaces/_impl_network_colored_spaces.rs b/src/trap_spaces/_impl_network_colored_spaces.rs new file mode 100644 index 0000000..8a5a1d3 --- /dev/null +++ b/src/trap_spaces/_impl_network_colored_spaces.rs @@ -0,0 +1,243 @@ +use crate::biodivine_std::traits::Set; +use crate::symbolic_async_graph::bdd_set::BddSet; +use crate::symbolic_async_graph::projected_iteration::{FnUpdateProjection, RawProjection}; +use crate::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; +use crate::trap_spaces::{NetworkColoredSpaces, NetworkSpaces, SymbolicSpaceContext}; +use crate::VariableId; +use biodivine_lib_bdd::{Bdd, BddVariable}; +use num_bigint::BigInt; + +impl NetworkColoredSpaces { + /// Construct a new [NetworkColoredSpaces] from a raw [Bdd] and a [SymbolicSpaceContext]. + pub fn new(bdd: Bdd, context: &SymbolicSpaceContext) -> NetworkColoredSpaces { + NetworkColoredSpaces { + bdd, + parameter_variables: context.inner_context().parameter_variables().clone(), + dual_variables: context.dual_variables.clone(), + } + } + + /// Construct a new [NetworkColoredSpaces] by copying the context of the current set. + /// + /// The contents of the set are completely replaced using the provided [Bdd], but the + /// underlying [SymbolicSpaceContext] remains the same. + pub fn copy(&self, bdd: Bdd) -> NetworkColoredSpaces { + BddSet::copy(self, bdd) + } + + /// Convert this set to a raw [Bdd]. + pub fn into_bdd(self) -> Bdd { + self.bdd + } + + /// View this set as a raw [Bdd]. + pub fn as_bdd(&self) -> &Bdd { + BddSet::as_bdd(self) + } + + /// Amount of storage used for this symbolic set. + pub fn symbolic_size(&self) -> usize { + BddSet::symbolic_size(self) + } + + /// Approximate size of this set (error grows for large sets). + pub fn approx_cardinality(&self) -> f64 { + BddSet::approx_cardinality(self) + } + + /// Compute exact `BigInt` cardinality of this set. + pub fn exact_cardinality(&self) -> BigInt { + BddSet::exact_cardinality(self) + } + + /// Return `true` if the set represents a single space-color pair. + pub fn is_singleton(&self) -> bool { + if !self.bdd.is_clause() { + return false; + } + let clause = self.bdd.first_clause().unwrap(); + for (t_var, f_var) in &self.dual_variables { + if clause[*t_var].is_none() || clause[*f_var].is_none() { + return false; + } + } + for p_var in &self.parameter_variables { + if clause[*p_var].is_none() { + return false; + } + } + true + } + + /// Perform a "raw projection" which eliminates the given symbolic variables from this set. + /// + /// Technically, you can supply any `BddVariable`, but the underlying `Bdd` of this set + /// should only depend on the *state and parameter variables* (i.e. not on any extra state + /// variables). + pub fn raw_projection(&self, eliminate: &[BddVariable]) -> RawProjection { + let mut retained = Vec::new(); + for p_var in &self.parameter_variables { + if !eliminate.contains(p_var) { + retained.push(*p_var); + } + } + for (t_var, f_var) in &self.dual_variables { + if !eliminate.contains(t_var) { + retained.push(*t_var); + } + if !eliminate.contains(f_var) { + retained.push(*f_var); + } + } + RawProjection::new(retained, &self.bdd) + } + + /// Create an iterable symbolic projection which only retains the update functions + /// of the specified network variables. + pub fn fn_update_projection<'a>( + &self, + functions: &[VariableId], + context: &'a SymbolicAsyncGraph, + ) -> FnUpdateProjection<'a> { + FnUpdateProjection::new(functions.to_vec(), context, &self.bdd) + } + + fn space_variables(&self) -> Vec { + let mut variables = Vec::new(); + for (t_var, f_var) in &self.dual_variables { + variables.push(*t_var); + variables.push(*f_var); + } + variables + } +} + +/// Relation operations. +impl NetworkColoredSpaces { + /// Remove every occurrence of a color form `colors` set. + pub fn minus_colors(&self, colors: &GraphColors) -> Self { + self.copy(self.bdd.and_not(colors.as_bdd())) + } + + /// Only retain colours in the supplied `colors` set. + pub fn intersect_colors(&self, colors: &GraphColors) -> Self { + self.copy(self.bdd.and(colors.as_bdd())) + } + + /// Remove every occurrence of a space from the `spaces` set, regardless of color. + pub fn minus_spaces(&self, spaces: &NetworkSpaces) -> Self { + self.copy(self.bdd.and_not(&spaces.bdd)) + } + + /// Retain only occurrences of vertices from the `spaces` set, regardless of color. + pub fn intersect_spaces(&self, spaces: &NetworkSpaces) -> Self { + self.copy(self.bdd.and(&spaces.bdd)) + } + + /// For every color, pick exactly one space. + pub fn pick_space(&self) -> Self { + let variables = self.space_variables(); + self.copy(self.bdd.pick(&variables)) + } + + /// For every vertex, pick exactly one color. + pub fn pick_color(&self) -> Self { + self.copy(self.bdd.pick(&self.parameter_variables)) + } + + /// Pick one (space, color) pair from this set and return it as a singleton. + /// + /// If the set is empty, return empty set. + pub fn pick_singleton(&self) -> NetworkColoredSpaces { + if self.is_empty() { + self.clone() + } else { + let witness = self.bdd.sat_witness().unwrap(); + // Retain only the relevant variables. + let mut partial_valuation = Vec::new(); + for (t_var, f_var) in &self.dual_variables { + partial_valuation.push((*t_var, witness[*t_var])); + partial_valuation.push((*f_var, witness[*f_var])); + } + for p_var in &self.parameter_variables { + partial_valuation.push((*p_var, witness[*p_var])); + } + self.copy(self.bdd.select(&partial_valuation)) + } + } + + /// Set of all colors which are in this set for at least one vertex. + pub fn colors(&self) -> GraphColors { + let variables = self.space_variables(); + GraphColors { + bdd: self.bdd.exists(&variables), + parameter_variables: self.parameter_variables.clone(), + } + } + + /// Set of all spaces which are in this set for at least one colour. + pub fn spaces(&self) -> NetworkSpaces { + NetworkSpaces { + bdd: self.bdd.exists(&self.parameter_variables), + dual_variables: self.dual_variables.clone(), + } + } +} + +impl BddSet for NetworkColoredSpaces { + fn as_bdd(&self) -> &Bdd { + &self.bdd + } + + fn copy(&self, bdd: Bdd) -> Self { + NetworkColoredSpaces { + bdd, + dual_variables: self.dual_variables.clone(), + parameter_variables: self.parameter_variables.clone(), + } + } + + fn active_variables(&self) -> u16 { + let x = self.dual_variables.len() * 2 + self.parameter_variables.len(); + u16::try_from(x).unwrap() + } +} + +#[cfg(test)] +mod tests { + use crate::biodivine_std::traits::Set; + use crate::symbolic_async_graph::SymbolicAsyncGraph; + use crate::trap_spaces::SymbolicSpaceContext; + use crate::BooleanNetwork; + use num_bigint::BigInt; + use num_traits::One; + + #[test] + fn basic_colored_spaces_set_test() { + let bn = BooleanNetwork::try_from_file("aeon_models/005.aeon").unwrap(); + let ctx = SymbolicSpaceContext::new(&bn); + let stg = SymbolicAsyncGraph::with_space_context(bn.clone(), &ctx).unwrap(); + + let unit = ctx.mk_unit_colored_spaces(&stg); + assert!(!unit.is_singleton()); + assert_eq!(unit, unit.copy(unit.clone().into_bdd())); + + let singleton = unit.pick_singleton(); + assert_eq!(1.0, singleton.approx_cardinality()); + assert_eq!(BigInt::one(), singleton.exact_cardinality()); + let singleton_color = singleton.colors(); + let singleton_space = singleton.spaces(); + assert!(singleton_color.is_singleton()); + assert!(singleton_space.is_singleton()); + assert!(!unit.intersect_colors(&singleton_color).is_singleton()); + // There is only one color, hence this holds. Otherwise this should not hold. + assert!(unit.intersect_spaces(&singleton_space).is_singleton()); + assert!(unit.minus_colors(&singleton_color).is_empty()); + assert!(unit.minus_spaces(&singleton_space).is_subset(&unit)); + + // There are 28 network variables and we are eliminating 22 of them, so 6 should be left. + let dual_vars = ctx.inner_context().all_extra_state_variables(); + let project = unit.raw_projection(&dual_vars[0..44]); + assert_eq!(project.iter().count(), 3_usize.pow(6)); + } +} diff --git a/src/trap_spaces/_impl_network_spaces.rs b/src/trap_spaces/_impl_network_spaces.rs new file mode 100644 index 0000000..89fac8b --- /dev/null +++ b/src/trap_spaces/_impl_network_spaces.rs @@ -0,0 +1,190 @@ +use crate::biodivine_std::traits::Set; +use crate::symbolic_async_graph::bdd_set::BddSet; +use crate::symbolic_async_graph::projected_iteration::RawProjection; +use crate::trap_spaces::{NetworkSpaces, SpaceIterator, SymbolicSpaceContext}; +use crate::{ExtendedBoolean, Space}; +use biodivine_lib_bdd::{Bdd, BddVariable}; +use num_bigint::BigInt; + +impl NetworkSpaces { + /// Create a new set of network spaces using a "raw" [Bdd] object w.r.t. the given `context`. + pub fn new(bdd: Bdd, context: &SymbolicSpaceContext) -> NetworkSpaces { + NetworkSpaces { + bdd, + dual_variables: context.dual_variables.clone(), + } + } + + /// Create a new set of network spaces using a "raw" [Bdd] while transferring the context + /// from this existing set. + fn copy(&self, bdd: Bdd) -> Self { + NetworkSpaces { + bdd, + dual_variables: self.dual_variables.clone(), + } + } + + /// Consume this object and return the underlying raw [Bdd]. + pub fn into_bdd(self) -> Bdd { + self.bdd + } + + /// Obtain the reference to the underlying raw [Bdd] of this set. + pub fn as_bdd(&self) -> &Bdd { + &self.bdd + } + + /// Approximate the size of this set using `f64`. + pub fn approx_cardinality(&self) -> f64 { + BddSet::approx_cardinality(self) + } + + /// The exact size of this set (i.e. number of elements). + pub fn exact_cardinality(&self) -> BigInt { + BddSet::exact_cardinality(self) + } + + /// Deterministically pick a single space from this set, and return it as a symbolic + /// singleton set. + /// + /// If this set is empty, returns an empty set. + pub fn pick_singleton(&self) -> NetworkSpaces { + if self.is_empty() { + self.clone() + } else { + // Pick one witness valuation from the BDD. + let witness = self.bdd.sat_witness().unwrap(); + // Retain only the relevant variables. + let mut partial_valuation = Vec::with_capacity(self.dual_variables.len() * 2); + for (t_var, f_var) in &self.dual_variables { + partial_valuation.push((*t_var, witness[*t_var])); + partial_valuation.push((*f_var, witness[*f_var])); + } + self.copy(self.bdd.select(&partial_valuation)) + } + } + + /// Amount of storage used for this symbolic set. + pub fn symbolic_size(&self) -> usize { + BddSet::symbolic_size(self) + } + + /// Returns true if this set represents a single space. + pub fn is_singleton(&self) -> bool { + if !self.bdd.is_clause() { + return false; + } + let clause = self.bdd.first_clause().unwrap(); + for (t_var, f_var) in &self.dual_variables { + if clause[*t_var].is_none() || clause[*f_var].is_none() { + return false; + } + } + true + } + + pub fn raw_projection(&self, eliminate: &[BddVariable]) -> RawProjection { + let mut retained = Vec::new(); + for (t_var, f_var) in &self.dual_variables { + if !eliminate.contains(t_var) { + retained.push(*t_var); + } + if !eliminate.contains(f_var) { + retained.push(*f_var); + } + } + RawProjection::new(retained, &self.bdd) + } + + /// Returns an iterator over all elements stored in this set. + /// + /// In the case of symbolic sets, `iter` and `into_iter` have the same result because + /// we have to recreate the the items anyway, so there is no true "iterate by reference" + /// option. + pub fn iter(&self) -> SpaceIterator { + let mut variables = Vec::with_capacity(2 * self.dual_variables.len()); + for (t_var, f_var) in &self.dual_variables { + variables.push(*t_var); + variables.push(*f_var); + } + let projection = RawProjection::new(variables, self.as_bdd()); + SpaceIterator { + inner_iterator: projection.into_iter(), + dual_variables: self.dual_variables.clone(), + } + } +} + +impl BddSet for NetworkSpaces { + fn as_bdd(&self) -> &Bdd { + &self.bdd + } + + fn copy(&self, bdd: Bdd) -> Self { + NetworkSpaces { + bdd, + dual_variables: self.dual_variables.clone(), + } + } + + fn active_variables(&self) -> u16 { + u16::try_from(self.dual_variables.len() * 2).unwrap() + } +} + +impl IntoIterator for NetworkSpaces { + type Item = Space; + type IntoIter = SpaceIterator; + + fn into_iter(self) -> Self::IntoIter { + self.iter() + } +} + +impl Iterator for SpaceIterator { + type Item = Space; + + fn next(&mut self) -> Option { + let Some(valuation) = self.inner_iterator.next() else { + return None; + }; + let mut space = Space(vec![ExtendedBoolean::Any; self.dual_variables.len()]); + for (i, (t_var, f_var)) in self.dual_variables.iter().enumerate() { + match (valuation[*t_var], valuation[*f_var]) { + (Some(true), Some(false)) => space.0[i] = ExtendedBoolean::One, + (Some(false), Some(true)) => space.0[i] = ExtendedBoolean::Zero, + (Some(true), Some(true)) => space.0[i] = ExtendedBoolean::Any, + _ => unreachable!(), + } + } + Some(space) + } +} + +#[cfg(test)] +mod tests { + use crate::trap_spaces::SymbolicSpaceContext; + use crate::BooleanNetwork; + use num_bigint::BigInt; + use num_traits::One; + + #[test] + fn basic_spaces_set_test() { + let bn = BooleanNetwork::try_from_file("aeon_models/005.aeon").unwrap(); + let ctx = SymbolicSpaceContext::new(&bn); + + let unit = ctx.mk_unit_spaces(); + assert!(!unit.is_singleton()); + assert_eq!(unit, unit.copy(unit.clone().into_bdd())); + + let singleton = unit.pick_singleton(); + assert_eq!(1.0, singleton.approx_cardinality()); + assert_eq!(BigInt::one(), singleton.exact_cardinality()); + assert_eq!(1, singleton.iter().count()); + + // There are 28 network variables and we are eliminating 22 of them, so 6 should be left. + let dual_vars = ctx.inner_context().all_extra_state_variables(); + let project = unit.raw_projection(&dual_vars[0..44]); + assert_eq!(project.iter().count(), 3_usize.pow(6)); + } +} diff --git a/src/trap_spaces/_impl_symbolic_space_context.rs b/src/trap_spaces/_impl_symbolic_space_context.rs new file mode 100644 index 0000000..e2b2986 --- /dev/null +++ b/src/trap_spaces/_impl_symbolic_space_context.rs @@ -0,0 +1,348 @@ +use crate::symbolic_async_graph::{SymbolicAsyncGraph, SymbolicContext}; +use crate::trap_spaces::{NetworkColoredSpaces, NetworkSpaces, SymbolicSpaceContext}; +use crate::{BooleanNetwork, ExtendedBoolean, Space, VariableId}; +use biodivine_lib_bdd::{bdd, Bdd, BddPartialValuation, BddVariable, BddVariableSet}; +use std::collections::HashMap; + +impl SymbolicSpaceContext { + /// Create a new [SymbolicSpaceContext] valid for the given [BooleanNetwork]. + pub fn new(network: &BooleanNetwork) -> SymbolicSpaceContext { + let map = network + .variables() + .map(|it| (it, 2)) + .collect::>(); + let inner_ctx = SymbolicContext::with_extra_state_variables(network, &map).unwrap(); + let positive_variables = inner_ctx.extra_state_variables_by_offset(0); + let negative_variables = inner_ctx.extra_state_variables_by_offset(1); + let dual_variables = positive_variables + .into_iter() + .zip(negative_variables) + .map(|((_v1, var_t), (_v2, var_f))| (var_t, var_f)) + .collect::>(); + SymbolicSpaceContext { + inner_ctx, + dual_variables, + } + } + + /// Access the inner [SymbolicContext]. + pub fn inner_context(&self) -> &SymbolicContext { + &self.inner_ctx + } + + /// A reference to the [BddVariableSet] of the inner [SymbolicContext]. + pub fn bdd_variable_set(&self) -> &BddVariableSet { + self.inner_context().bdd_variable_set() + } + + /// Get the BDD state variable `x` representing the network variable `var`. + pub fn get_state_variable(&self, var: VariableId) -> BddVariable { + self.inner_context().get_state_variable(var) + } + + /// Get the BDD space variable `x_T` for the network variable `var`. + pub fn get_positive_variable(&self, var: VariableId) -> BddVariable { + self.dual_variables[var.to_index()].0 + } + + /// Get the BDD space variable `x_F` for the network variable `var`. + pub fn get_negative_variable(&self, var: VariableId) -> BddVariable { + self.dual_variables[var.to_index()].1 + } + + /// Compute the [Bdd] which contains all correctly encoded spaces tracked by this + /// [SymbolicSpaceContext]. + /// + /// The [Bdd] only constraints the space variables and it has no impact on the space/parameter + /// variables. + pub fn mk_unit_bdd(&self) -> Bdd { + let bdd_vars = self.bdd_variable_set(); + self.dual_variables + .iter() + .cloned() + .fold(bdd_vars.mk_true(), |acc, (t_var, f_var)| { + bdd!(bdd_vars, acc & (t_var | f_var)) + }) + } + + /// Compute the symbolic set of all [NetworkSpaces] valid in this [SymbolicSpaceContext]. + pub fn mk_unit_spaces(&self) -> NetworkSpaces { + NetworkSpaces::new(self.mk_unit_bdd(), self) + } + + /// Compute an empty symbolic set of network spaces. + pub fn mk_empty_spaces(&self) -> NetworkSpaces { + NetworkSpaces::new(self.bdd_variable_set().mk_false(), self) + } + + /// Compute an empty symbolic set of colored network spaces. + pub fn mk_empty_colored_spaces(&self) -> NetworkColoredSpaces { + NetworkColoredSpaces::new(self.bdd_variable_set().mk_false(), self) + } + + /// Compute a unit set of coloured trap spaces which is valid with respect to a specific + /// [SymbolicAsyncGraph]. Note that such graph has to be created using + /// [SymbolicAsyncGraph::with_space_context]. + pub fn mk_unit_colored_spaces(&self, graph: &SymbolicAsyncGraph) -> NetworkColoredSpaces { + let colors = graph.mk_unit_colors().into_bdd(); + let spaces = self.mk_unit_spaces().into_bdd(); + NetworkColoredSpaces { + bdd: colors.and(&spaces), + dual_variables: self.dual_variables.clone(), + parameter_variables: self.inner_ctx.parameter_variables().clone(), + } + } + + /// Compute a [Bdd] which encodes all spaces in which the value of `function` can be + /// `true` for some state. We assume that `function` can depend on state variables and + /// parameter variables, but not on the dual variables used for space encoding. + /// + /// In other words, a space `S` satisfies the result [Bdd] if and only if there exists + /// a state `x \in S` such that `function(x) = true`. + /// + /// To compute this, we evaluate the following (informal) expression: + /// `exists s_1...s_n: [(s_i => s_i_T) & (!s_i => s_i_F)] & function(s_1, ..., s_n)` + /// + /// **WARNING:** The resulting BDD also allows invalid space encodings, mostly because + /// these are to some extent still interesting in some applications. + /// + pub fn mk_can_go_to_true(&self, function: &Bdd) -> Bdd { + let bdd_vars = self.inner_ctx.bdd_variable_set(); + // Only constrain variables that are relevant to `functions`. + let support_set = { + let mut s = function.support_set().into_iter().collect::>(); + s.sort(); + s + }; + let mut result = function.clone(); + for var in support_set.into_iter().rev() { + let index = self + .inner_ctx + .state_variables() + .iter() + .position(|it| *it == var); + let Some(index) = index else { + // Skip non-state variables. + continue; + }; + let state_var = var; + let (t_var, f_var) = self.dual_variables[index]; + let is_in_space = bdd!(bdd_vars, (state_var => t_var) & ((!state_var) => f_var)); + result = result.and(&is_in_space).var_exists(state_var); + } + result + } + + /// Compute a [Bdd] of all spaces that are a super-space of the elements in `spaces`. + /// + /// The process should also preserve any "extra" variables, such as colors/parameters. + /// Also note that this is a simple iterative algorithm that may need `O(n)` iterations + /// and `O(n)` BDD ops to converge (`n` being the number of network variables). + /// + pub fn mk_super_spaces(&self, spaces: &Bdd) -> Bdd { + let vars = self.bdd_variable_set(); + let mut result = spaces.clone(); + for (t_var, f_var) in self.dual_variables.iter().rev() { + // Select every space in which we have `t_var=false`, but there is + // no equivalent space with `t_var=true`. Flips `t_var` on output, + // meaning we actually get the set of super spaces where `true` is added. + /* + Not sure of ternary actually helps here. Should test at some point. + let restricted = result.var_select(*t_var, false); + let adds_true = Bdd::fused_binary_flip_op( + (&restricted, None), + (&result, Some(*t_var)), + Some(*t_var), + and_not + ); + let restricted = result.var_select(*f_var, false); + let adds_false = Bdd::fused_binary_flip_op( + (&restricted, None), + (&result, Some(*f_var)), + Some(*f_var), + and_not + );*/ + let t_var_bdd = vars.mk_literal(*t_var, false); + let adds_true = Bdd::fused_ternary_flip_op( + (&result, None), + (&t_var_bdd, None), + (&result, Some(*t_var)), + Some(*t_var), + and_and_not, + ); + // Symmetrically for `t_false`. + let f_var_bdd = vars.mk_literal(*f_var, false); + let adds_false = Bdd::fused_ternary_flip_op( + (&result, None), + (&f_var_bdd, None), + (&result, Some(*f_var)), + Some(*f_var), + and_and_not, + ); + if !adds_true.is_false() || !adds_false.is_false() { + result = bdd!(vars, result | (adds_true | adds_false)); + if cfg!(feature = "print-progress") && result.size() > 100_000 { + println!( + "Computing super-spaces: {}[nodes:{}].", + result.cardinality(), + result.size(), + ); + } + } + } + result + } + + /// Compute a [Bdd] of all spaces that are a sub-space of the elements in `spaces`. + /// + /// The same notes as for [SymbolicSpaceContext::mk_super_spaces] apply. + pub fn mk_sub_spaces(&self, spaces: &Bdd) -> Bdd { + let vars = self.bdd_variable_set(); + let mut result = spaces.clone(); + for (t_var, f_var) in self.dual_variables.clone().into_iter().rev() { + // A value can go down only in subspaces where both variables are set. + // If only one variable is set, going down will just break the encoding. + let can_go_down = bdd!(vars, t_var & f_var); + // Has `t_var=true`, but the flipped valuation is not present. We return + // the flipped valuation. + let removes_true = Bdd::fused_ternary_flip_op( + (&result, None), + (&can_go_down, None), + (&result, Some(t_var)), + Some(t_var), + and_and_not, + ); + // Symmetrically for `t_false`. + let removes_false = Bdd::fused_ternary_flip_op( + (&result, None), + (&can_go_down, None), + (&result, Some(f_var)), + Some(f_var), + and_and_not, + ); + if !removes_true.is_false() || !removes_false.is_false() { + result = bdd!(vars, result | (removes_true | removes_false)); + if cfg!(feature = "print-progress") && result.size() > 100_000 { + println!( + "Computing sub-spaces: {}[nodes:{}].", + result.cardinality(), + result.size(), + ); + } + } + } + result + } + + /// Construct a symbolic singleton for a [Space]. + pub fn mk_space(&self, space: &Space) -> Bdd { + let mut valuation = BddPartialValuation::empty(); + for (i, (t_var, f_var)) in self.dual_variables.iter().enumerate() { + match space.0[i] { + ExtendedBoolean::Zero => { + valuation.set_value(*t_var, false); + valuation.set_value(*f_var, true); + } + ExtendedBoolean::One => { + valuation.set_value(*t_var, true); + valuation.set_value(*f_var, false); + } + ExtendedBoolean::Any => { + valuation.set_value(*t_var, true); + valuation.set_value(*f_var, true); + } + } + } + self.bdd_variable_set().mk_conjunctive_clause(&valuation) + } +} + +fn and_and_not(a: Option, b: Option, c: Option) -> Option { + // Just `a & b & !c`: + match (a, b, c) { + (Some(true), Some(true), Some(false)) => Some(true), + (Some(false), _, _) => Some(false), + (_, Some(false), _) => Some(false), + (_, _, Some(true)) => Some(false), + (_, _, _) => None, + } +} + +#[cfg(test)] +mod tests { + use crate::biodivine_std::traits::Set; + use crate::trap_spaces::{NetworkSpaces, SymbolicSpaceContext}; + use crate::ExtendedBoolean::{One, Zero}; + use crate::{BooleanNetwork, Space}; + use biodivine_lib_bdd::bdd; + + #[test] + fn test_super_and_sub_spaces() { + let network = BooleanNetwork::try_from_file("./aeon_models/005.aeon").unwrap(); + let ctx = SymbolicSpaceContext::new(&network); + let mut all_zero = Space::new(&network); + for var in network.variables() { + all_zero[var] = Zero; + } + let all_zero = ctx.mk_space(&all_zero); + let super_spaces = ctx.mk_super_spaces(&all_zero); + let sub_spaces = ctx.mk_sub_spaces(&all_zero); + + // all_zero should have only one sub-space: itself. + println!("{} {}", all_zero.cardinality(), sub_spaces.cardinality()); + assert!(sub_spaces.iff(&all_zero).is_true()); + + let all_zero = NetworkSpaces::new(all_zero, &ctx); + let super_spaces = NetworkSpaces::new(super_spaces, &ctx); + + assert!(all_zero.is_singleton()); + assert!(all_zero.is_subset(&super_spaces)); + assert_eq!(1.0, all_zero.approx_cardinality()); + + // A state has exactly 2^n super-spaces, which in this case means 2^28. + // The rationale is that every super-space has a unique subset of variables set to + // `Any` instead of `Zero`. And the number of such subsets is 2^n. + assert_eq!(268435456.0, super_spaces.approx_cardinality()); + + let mut first_10 = Space::new(&network); + for var in network.variables().take(10) { + first_10[var] = One; + } + let first_10 = ctx.mk_space(&first_10); + let super_spaces = ctx.mk_super_spaces(&first_10); + let sub_spaces = ctx.mk_sub_spaces(&first_10); + + //let first_10 = NetworkSpaces::new(first_10, &ctx); + let super_spaces = NetworkSpaces::new(super_spaces, &ctx); + let sub_spaces = NetworkSpaces::new(sub_spaces, &ctx); + + // There are 18 free variables and 10 fixed variables, hence the number of super-spaces + // should be 2^10, and the number of sub-spaces should be 3^18. + assert_eq!(1024.0, super_spaces.approx_cardinality()); + assert_eq!(387420489.0, sub_spaces.approx_cardinality()); + } + + #[test] + fn test_can_go_to_true() { + let network = BooleanNetwork::try_from_file("./aeon_models/005.aeon").unwrap(); + let ctx = SymbolicSpaceContext::new(&network); + let vars = ctx.bdd_variable_set(); + let and_function = bdd!(vars, "v_ADD" & "v_ATM"); + let or_function = bdd!(vars, "v_ADD" | "v_ATM"); + let and_up = ctx.mk_can_go_to_true(&and_function); + let or_up = ctx.mk_can_go_to_true(&or_function); + + let unit = ctx.mk_unit_spaces(); + let and_up = NetworkSpaces::new(and_up, &ctx).intersect(&unit); + let or_up = NetworkSpaces::new(or_up, &ctx).intersect(&unit); + + // In every space where (x & y) goes to true, (x | y) also goes to true. + assert!(and_up.is_subset(&or_up)); + assert!(!or_up.is_subset(&and_up)); + // In this case, the number of such spaces is k*3^26 (remaining variables are unconstrained) + // where `k=4` for AND ([*,*], [1,*], [*,1], [1,1]) and `k=8` for OR ([*,*], [*,0], [0,*] + // [*,1], [1,*], [0,1], [1,0], [1,1]; everything except [0,0]). + assert_eq!(4.0 * 2541865828329.0, and_up.approx_cardinality()); + assert_eq!(8.0 * 2541865828329.0, or_up.approx_cardinality()); + } +} diff --git a/src/trap_spaces/_impl_trap_spaces.rs b/src/trap_spaces/_impl_trap_spaces.rs new file mode 100644 index 0000000..acf2f55 --- /dev/null +++ b/src/trap_spaces/_impl_trap_spaces.rs @@ -0,0 +1,240 @@ +use crate::biodivine_std::traits::Set; +use crate::fixed_points::FixedPoints; +use crate::trap_spaces::{NetworkColoredSpaces, SymbolicSpaceContext, TrapSpaces}; +use crate::BooleanNetwork; +use std::collections::HashSet; + +impl TrapSpaces { + /// Computes the coloured subset of "essential" trap spaces of a Boolean network. + /// + /// A trap space is essential if it cannot be reduced through percolation. In general, every + /// minimal trap space is always essential. + pub fn essential_symbolic( + network: &BooleanNetwork, + ctx: &SymbolicSpaceContext, + restriction: &NetworkColoredSpaces, + ) -> NetworkColoredSpaces { + if cfg!(feature = "print-progress") { + println!( + "Start symbolic essential trap space search with {}[nodes:{}] candidates.", + restriction.approx_cardinality(), + restriction.symbolic_size() + ); + } + + let bdd_ctx = ctx.bdd_variable_set(); + + // We always start with the restriction set, because it should carry the information + // about valid encoding of spaces. + let mut to_merge = vec![restriction.as_bdd().clone()]; + for var in network.variables() { + let update_bdd = if let Some(update) = network.get_update_function(var) { + ctx.inner_context().mk_fn_update_true(update) + } else { + let regulators = network.regulators(var); + ctx.inner_context() + .mk_implicit_function_is_true(var, ®ulators) + }; + let not_update_bdd = update_bdd.not(); + + let has_up_transition = ctx.mk_can_go_to_true(&update_bdd); + let has_down_transition = ctx.mk_can_go_to_true(¬_update_bdd); + + let true_var = ctx.get_positive_variable(var); + let false_var = ctx.get_negative_variable(var); + let is_trap_1 = has_up_transition.imp(&bdd_ctx.mk_var(true_var)); + let is_trap_2 = has_down_transition.imp(&bdd_ctx.mk_var(false_var)); + let is_trap = is_trap_1.and(&is_trap_2); + let is_essential_1 = bdd_ctx.mk_var(true_var).and(&bdd_ctx.mk_var(false_var)); + let is_essential_2 = has_up_transition.and(&has_down_transition); + let is_essential = is_essential_1.imp(&is_essential_2); + // This will work in next version of lib-bdd: + // let is_trap = bdd!(bdd_ctx, (has_up_transition => true_var) & (has_down_transition => false_var)); + // let is_essential = bdd!(bdd_ctx, (true_var & false_var) => (has_up_transition & has_down_transition)); + + if cfg!(feature = "print-progress") { + println!( + " > Created initial sets for {:?} using {}+{} BDD nodes.", + var, + is_trap.size(), + is_essential.size(), + ); + } + + to_merge.push(is_trap.and(&is_essential)); + //to_merge.push(is_essential); + } + + let trap_spaces = FixedPoints::symbolic_merge(bdd_ctx, to_merge, HashSet::default()); + + let trap_spaces = NetworkColoredSpaces::new(trap_spaces, ctx); + + if cfg!(feature = "print-progress") { + println!( + "Found {}[nodes:{}] essential trap spaces.", + trap_spaces.approx_cardinality(), + trap_spaces.symbolic_size(), + ); + } + + trap_spaces + } + + /// Computes the minimal coloured trap spaces of the provided `network` within the specified + /// `restriction` set. + /// + /// This method currently uses [Self::essential_symbolic], hence is always slower than + /// this method. + pub fn minimal_symbolic( + network: &BooleanNetwork, + ctx: &SymbolicSpaceContext, + restriction: &NetworkColoredSpaces, + ) -> NetworkColoredSpaces { + let essential = Self::essential_symbolic(network, ctx, restriction); + Self::minimize(ctx, &essential) + } + + /// Compute the minimal spaces within a particular subset. + pub fn minimize( + ctx: &SymbolicSpaceContext, + spaces: &NetworkColoredSpaces, + ) -> NetworkColoredSpaces { + let mut original = spaces.clone(); + let mut minimal = ctx.mk_empty_colored_spaces(); + + if cfg!(feature = "print-progress") { + println!( + "Start minimal space search with {}[nodes:{}] candidates.", + original.approx_cardinality(), + original.symbolic_size() + ); + } + + while !original.is_empty() { + // TODO: + // The pick-space process could probably be optimized somewhat to prioritize + // the most specific trap spaces (most "false" dual variables) instead of any + // just any trap space. On the other hand, the pick method already favors "lower" + // valuations, so there might not be that much space for improvement. + + // TODO: + // The other option would be to also consider sub-spaces and basically do something + // like normal attractor search, where next candidate is picked only from the + // sub-spaces of the original pick. This would guarantee that every iteration always + // discovers a minimal trap space, but it could just mean extra overhead if the + // "greedy" method using pick is good enough. Initial tests indicate that the + // greedy approach is enough. + let minimum_candidate = original.pick_space(); + // Compute the set of strict super spaces. + // TODO: + // This can take a long time if there are colors and a lot of traps, e.g. + // fixed-points, even though individual colors are easy. We should probably + // find a way to get rid of fixed points and any related super-spaces first, + // as these are clearly minimal. The other option would be to tune the super + // space enumeration to avoid spaces that are clearly irrelevant anyway. + let super_spaces = ctx.mk_super_spaces(minimum_candidate.as_bdd()); + let super_spaces = NetworkColoredSpaces::new(super_spaces, ctx); + + original = original.minus(&super_spaces); + minimal = minimal.minus(&super_spaces).union(&minimum_candidate); + + if cfg!(feature = "print-progress") { + println!( + "Minimization in progress: {}[nodes:{}] unprocessed, {}[nodes:{}] candidates.", + original.approx_cardinality(), + original.symbolic_size(), + minimal.approx_cardinality(), + minimal.symbolic_size(), + ); + } + } + + if cfg!(feature = "print-progress") { + println!( + "Found {}[nodes:{}] minimal spaces.", + minimal.approx_cardinality(), + minimal.symbolic_size(), + ); + } + + minimal + } + + /// The same as [Self::minimize], but searches for maximal spaces within `spaces`. + pub fn maximize( + ctx: &SymbolicSpaceContext, + spaces: &NetworkColoredSpaces, + ) -> NetworkColoredSpaces { + let mut original = spaces.clone(); + let mut maximal = ctx.mk_empty_colored_spaces(); + + if cfg!(feature = "print-progress") { + println!( + "Start maximal space search with {}[nodes:{}] candidates.", + original.approx_cardinality(), + original.symbolic_size() + ); + } + + while !original.is_empty() { + let maximum_candidate = original.pick_space(); + // Compute the set of strict sub spaces. + let super_spaces = ctx.mk_sub_spaces(maximum_candidate.as_bdd()); + let super_spaces = NetworkColoredSpaces::new(super_spaces, ctx); + + original = original.minus(&super_spaces); + maximal = maximal.minus(&super_spaces).union(&maximum_candidate); + + if cfg!(feature = "print-progress") { + println!( + "Maximization in progress: {}[nodes:{}] unprocessed, {}[nodes:{}] candidates.", + original.approx_cardinality(), + original.symbolic_size(), + maximal.approx_cardinality(), + maximal.symbolic_size(), + ); + } + } + + if cfg!(feature = "print-progress") { + println!( + "Found {}[nodes:{}] minimal spaces.", + maximal.approx_cardinality(), + maximal.symbolic_size(), + ); + } + + maximal + } +} + +#[cfg(test)] +mod tests { + use crate::biodivine_std::traits::Set; + use crate::symbolic_async_graph::SymbolicAsyncGraph; + use crate::trap_spaces::{SymbolicSpaceContext, TrapSpaces}; + use crate::BooleanNetwork; + + #[test] + fn test_trap_spaces() { + let network = BooleanNetwork::try_from_file("./aeon_models/005.aeon").unwrap(); + let ctx = SymbolicSpaceContext::new(&network); + let stg = SymbolicAsyncGraph::with_space_context(network.clone(), &ctx).unwrap(); + let unit = ctx.mk_unit_colored_spaces(&stg); + + let essential_traps = TrapSpaces::essential_symbolic(&network, &ctx, &unit); + let minimal_traps = TrapSpaces::minimal_symbolic(&network, &ctx, &unit); + let maximal_traps = TrapSpaces::maximize(&ctx, &essential_traps); + + assert!(minimal_traps.is_subset(&essential_traps)); + assert!(maximal_traps.is_subset(&essential_traps)); + assert_eq!(7.0, essential_traps.approx_cardinality()); + assert_eq!(7, essential_traps.spaces().iter().count()); + assert_eq!(1.0, minimal_traps.approx_cardinality()); + assert_eq!(1.0, maximal_traps.approx_cardinality()); + + assert!(minimal_traps.is_singleton()); + assert!(maximal_traps.is_singleton()); + assert!(!essential_traps.is_singleton()); + } +} diff --git a/src/trap_spaces/mod.rs b/src/trap_spaces/mod.rs new file mode 100644 index 0000000..4a13fe6 --- /dev/null +++ b/src/trap_spaces/mod.rs @@ -0,0 +1,60 @@ +use crate::symbolic_async_graph::projected_iteration::OwnedRawSymbolicIterator; +use crate::symbolic_async_graph::SymbolicContext; +use biodivine_lib_bdd::{Bdd, BddVariable}; + +mod _impl_network_colored_spaces; +mod _impl_network_spaces; +mod _impl_symbolic_space_context; +mod _impl_trap_spaces; + +/// This object is a special extension of [SymbolicContext] which (aside from states and functions) +/// allows representing network subspaces (see also [Space]). +/// +/// The representation uses the "extra state variables" supported by [SymbolicContext]. For each +/// network variable `x`, [SymbolicSpaceContext] adds two extra symbolic variables which we +/// refer to as `x_T` and `x_F`. These then encode individual spaces such that `(1,0) = 1`, +/// `(0,1) = 0` and `(1,1) = *`. Value `(0,0)` is invalid in this encoding. +/// [SymbolicSpaceContext] should document how the `(0,0)` is treated by each method (i.e. if +/// the result discards invalid values, or if they need to be excluded later). +/// +/// Note that the BDDs returned by [SymbolicSpaceContext] are not directly compatible with +/// [SymbolicAsyncGraph], because they use a different [SymbolicContext]. However, you can +/// create a [SymbolicAsyncGraph] that is compatible with the [SymbolicSpaceContext] by +/// using the [SymbolicContext] available in [SymbolicSpaceContext::inner_context] +/// (see also [SymbolicAsyncGraph::with_space_context]). +/// +pub struct SymbolicSpaceContext { + inner_ctx: SymbolicContext, + dual_variables: Vec<(BddVariable, BddVariable)>, +} + +/// A symbolic set consisting of network subspaces (see also [Space]). +/// +/// This is in principle similar to [GraphVertices], but uses [SymbolicSpaceContext] for encoding. +#[derive(Clone, Eq, PartialEq, Hash, Debug)] +pub struct NetworkSpaces { + bdd: Bdd, + dual_variables: Vec<(BddVariable, BddVariable)>, +} + +/// An iterator which goes through the elements of a [NetworkSpaces] set. +pub struct SpaceIterator { + inner_iterator: OwnedRawSymbolicIterator, + dual_variables: Vec<(BddVariable, BddVariable)>, +} + +/// A symbolic relation consisting of network subspaces and parameter colors (valuations). +/// +/// This is similar to [GraphColoredVertices], but uses [SymbolicSpaceContext] for encoding +/// of spaces. Colors/parameters are encoded the same way as in the normal [SymbolicContext]. +#[derive(Clone, Eq, PartialEq, Hash, Debug)] +pub struct NetworkColoredSpaces { + bdd: Bdd, + dual_variables: Vec<(BddVariable, BddVariable)>, + parameter_variables: Vec, +} + +/// A utility object similar to [FixedPoints] which facilitates trap space computation. +pub struct TrapSpaces { + _dummy: (), +}