Skip to content

Commit

Permalink
refactor: petri net encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Dec 12, 2023
1 parent 584d8bb commit b641739
Show file tree
Hide file tree
Showing 2 changed files with 118 additions and 27 deletions.
93 changes: 91 additions & 2 deletions src/symbolic_domains/symbolic_domain.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,7 @@ pub trait SymbolicDomainOrd<T>: SymbolicDomain<T> {
/// variables to `true` and leave the remaining as `false`.
#[derive(Clone, Debug)]
pub struct UnaryIntegerDomain {
/// invariant: sorted
variables: Vec<BddVariable>, // todo maybe Rc<[BddVariable]>
}

Expand Down Expand Up @@ -248,8 +249,8 @@ impl SymbolicDomainOrd<u8> 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))
})

Expand All @@ -265,3 +266,91 @@ impl SymbolicDomainOrd<u8> for UnaryIntegerDomain {
lhs.cmp(rhs)
}
}

pub struct PetriNetIntegerDomain {
/// invariant: sorted
variables: Vec<BddVariable>,
}

impl SymbolicDomain<u8> 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::<Vec<_>>()
.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<BddVariable> {
self.variables.clone() // already sorted
}

fn raw_bdd_variables_unsorted(&self) -> Vec<BddVariable> {
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<u8> 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)
}
}
52 changes: 27 additions & 25 deletions tests/some_test.rs
View file
Original file line number Diff line number Diff line change
@@ -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<D, OD>
where
Expand Down Expand Up @@ -128,45 +128,47 @@ 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 {
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_dumb =
bio::old_update_fn::SystemUpdateFn::<UnaryIntegerDomain, u8>::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::<UnaryIntegerDomain, u8>::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::<bio::symbolic_domain::UnaryIntegerDomain, u8>::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");
Expand Down Expand Up @@ -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")
);
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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")
);
Expand Down

0 comments on commit b641739

Please sign in to comment.