From b6417399eacd1701c23922167edcb4d0af7cb591 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Chud=C3=AD=C4=8Dek?= Date: Tue, 12 Dec 2023 14:29:54 +0100 Subject: [PATCH] refactor: petri net encoding --- src/symbolic_domains/symbolic_domain.rs | 93 ++++++++++++++++++++++++- tests/some_test.rs | 52 +++++++------- 2 files changed, 118 insertions(+), 27 deletions(-) diff --git a/src/symbolic_domains/symbolic_domain.rs b/src/symbolic_domains/symbolic_domain.rs index 5f8c12a..07efdb3 100644 --- a/src/symbolic_domains/symbolic_domain.rs +++ b/src/symbolic_domains/symbolic_domain.rs @@ -161,6 +161,7 @@ pub trait SymbolicDomainOrd: SymbolicDomain { /// variables to `true` and leave the remaining as `false`. #[derive(Clone, Debug)] pub struct UnaryIntegerDomain { + /// invariant: sorted variables: Vec, // todo maybe Rc<[BddVariable]> } @@ -248,8 +249,8 @@ impl SymbolicDomainOrd for UnaryIntegerDomain { Self { variables } } - fn encode_lt(&self, bdd_variable_set: &BddVariableSet, exclusive_uppper_bound: &u8) -> Bdd { - (0..*exclusive_uppper_bound).fold(self.empty_collection(bdd_variable_set), |acc, val| { + fn encode_lt(&self, bdd_variable_set: &BddVariableSet, exclusive_upper_bound: &u8) -> Bdd { + (0..*exclusive_upper_bound).fold(self.empty_collection(bdd_variable_set), |acc, val| { acc.or(&self.encode_one(bdd_variable_set, &val)) }) @@ -265,3 +266,91 @@ impl SymbolicDomainOrd for UnaryIntegerDomain { lhs.cmp(rhs) } } + +pub struct PetriNetIntegerDomain { + /// invariant: sorted + variables: Vec, +} + +impl SymbolicDomain for PetriNetIntegerDomain { + fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &u8) { + if value > &(self.variables.len() as u8) { + let vars = self + .variables + .iter() + .map(|var| format!("{:?}", var)) + .collect::>() + .join(", "); + + panic!( + "Value is too big for domain {}; value: {}, domain size: {}", + vars, + value, + self.variables.len() + ) + } + + self.variables + .iter() + .enumerate() + .for_each(|(var_idx_within_sym_var, var)| { + bdd_valuation.set_value(*var, var_idx_within_sym_var == (*value as usize)); + }); + } + + fn empty_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd { + bdd_variable_set.mk_false() + } + + fn unit_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd { + bdd_variable_set.mk_sat_exactly_k(1, &self.variables) + } + + fn raw_bdd_variables(&self) -> Vec { + self.variables.clone() // already sorted + } + + fn raw_bdd_variables_unsorted(&self) -> Vec { + self.raw_bdd_variables() // already the optimal performance + } + + fn decode_bits(&self, bdd_valuation: &BddPartialValuation) -> u8 { + // This method does not always check if the valuation is valid in the unary encoding, it + // just picks the "simplest" interpretation of the given valuation. For increased safety, + // we should check that that after the only "true" value, only "false" values follow. + + self.variables + .iter() + .enumerate() + .find(|(_, var)| { + bdd_valuation + .get_value(**var) + .expect("var should be in the valuation") + }) + .map(|(idx, _)| idx as u8) + .expect("a valid value should be encoded by a \"true\" bit") + } +} + +impl SymbolicDomainOrd for PetriNetIntegerDomain { + fn new(builder: &mut BddVariableSetBuilder, name: &str, max_value: &u8) -> Self { + let variables = (0..=*max_value) // notice the inclusive range + .map(|var_idx| { + let name = format!("{name}_v{}", var_idx + 1); + builder.make_variable(name.as_str()) + }) + .collect(); + + Self { variables } + } + + fn encode_lt(&self, bdd_variable_set: &BddVariableSet, exclusive_upper_bound: &u8) -> Bdd { + (0..*exclusive_upper_bound).fold(self.empty_collection(bdd_variable_set), |acc, val| { + acc.or(&self.encode_one(bdd_variable_set, &val)) + }) + } + + fn cmp(lhs: &u8, rhs: &u8) -> std::cmp::Ordering { + lhs.cmp(rhs) + } +} diff --git a/tests/some_test.rs b/tests/some_test.rs index 0f4c733..558be98 100644 --- a/tests/some_test.rs +++ b/tests/some_test.rs @@ -1,7 +1,7 @@ #![allow(dead_code)] use biodivine_lib_bdd::Bdd; -use biodivine_lib_logical_models::prelude::{self as bio, old_symbolic_domain::UnaryIntegerDomain}; +use biodivine_lib_logical_models::prelude as bio; struct TheFourImpls where @@ -128,8 +128,8 @@ impl TheFourImplsBdd { impl TheFourImpls< - bio::symbolic_domain::UnaryIntegerDomain, - bio::old_symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, + bio::old_symbolic_domain::PetriNetIntegerDomain, > { fn from_path(sbml_path: &str) -> Self { @@ -137,36 +137,38 @@ impl std::fs::File::open(sbml_path).expect("should be able to open file"), )); bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find"); - let old_dumb = - bio::old_update_fn::SystemUpdateFn::::try_from_xml(&mut xml) - .expect("should be able to parse"); + let old_dumb = bio::old_update_fn::SystemUpdateFn::< + bio::old_symbolic_domain::PetriNetIntegerDomain, + u8, + >::try_from_xml(&mut xml) + .expect("should be able to parse"); let mut xml = xml::reader::EventReader::new(std::io::BufReader::new( std::fs::File::open(sbml_path).expect("should be able to open file"), )); bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find"); - let old_smart = - bio::old_update_fn::SmartSystemUpdateFn::::try_from_xml( - &mut xml, - ) - .expect("should be able to parse"); + let old_smart = bio::old_update_fn::SmartSystemUpdateFn::< + bio::old_symbolic_domain::PetriNetIntegerDomain, + u8, + >::try_from_xml(&mut xml) + .expect("should be able to parse"); let mut xml = xml::reader::EventReader::new(std::io::BufReader::new( std::fs::File::open(sbml_path).expect("should be able to open file"), )); bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find"); - let new_dumb = - bio::update_fn::SystemUpdateFn::::try_from_xml( - &mut xml, - ) - .expect("should be able to parse"); + let new_dumb = bio::update_fn::SystemUpdateFn::< + bio::symbolic_domain::PetriNetIntegerDomain, + u8, + >::try_from_xml(&mut xml) + .expect("should be able to parse"); let mut xml = xml::reader::EventReader::new(std::io::BufReader::new( std::fs::File::open(sbml_path).expect("should be able to open file"), )); bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find"); let new_smart = bio::update_fn::SmartSystemUpdateFn::< - bio::symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, u8, >::try_from_xml(&mut xml) .expect("should be able to parse"); @@ -329,8 +331,8 @@ fn consistency_check() { // let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string(); let the_four = TheFourImpls::< - bio::symbolic_domain::UnaryIntegerDomain, - bio::old_symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, + bio::old_symbolic_domain::PetriNetIntegerDomain, >::from_path( filepath.to_str().expect("could not convert to str") ); @@ -480,14 +482,14 @@ fn check_specific() { let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string(); let the_four = TheFourImpls::< - bio::symbolic_domain::UnaryIntegerDomain, - bio::old_symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, + bio::old_symbolic_domain::PetriNetIntegerDomain, // >::from_path(filepath.to_str().expect("could not convert to str")); >::from_path(&filepath); let the_four_check = TheFourImpls::< - bio::symbolic_domain::UnaryIntegerDomain, - bio::old_symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, + bio::old_symbolic_domain::PetriNetIntegerDomain, // >::from_path(filepath.to_str().expect("could not convert to str")); >::from_path(&filepath); @@ -687,8 +689,8 @@ fn predecessors_consistency_check() { // let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string(); let the_four = TheFourImpls::< - bio::symbolic_domain::UnaryIntegerDomain, - bio::old_symbolic_domain::UnaryIntegerDomain, + bio::symbolic_domain::PetriNetIntegerDomain, + bio::old_symbolic_domain::PetriNetIntegerDomain, >::from_path( filepath.to_str().expect("could not convert to str") );