Skip to content

Commit

Permalink
fix: removed primed domains from unit set in new smart; still some bu…
Browse files Browse the repository at this point in the history
…gs present tho
  • Loading branch information
Lukáš Chudíček committed Dec 11, 2023
1 parent c21d8d8 commit 7d3b920
Show file tree
Hide file tree
Showing 3 changed files with 307 additions and 163 deletions.
2 changes: 2 additions & 0 deletions src/prototype/smart_system_update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1440,6 +1440,8 @@ mod tests {
println!("dirent = {:?}", dirent);
let filepath = dirent.expect("could not read file").path();

let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string();

let smart_system_update_fn = {
let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open(filepath.clone()).expect("cannot open the file"),
Expand Down
19 changes: 5 additions & 14 deletions src/update/update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -388,9 +388,10 @@ where

let unit_set = named_symbolic_domains.iter().fold(
bdd_variable_set.mk_true(),
|acc, ((_, domain), (_, primed_domain))| {
|acc, ((_, domain), _)| {
acc.and(&domain.unit_collection(&bdd_variable_set))
.and(&primed_domain.unit_collection(&bdd_variable_set))
// primed ones must not affect unit collection -> ignore
// .and(&primed_domain.unit_collection(&bdd_variable_set))
},
);

Expand Down Expand Up @@ -467,24 +468,14 @@ where
let forgor_old_val =
source_states_transition_relation.exists(target_domain.raw_bdd_variables().as_slice());

// todo remove this; unit_collection should be cached somehow (or otherwise optimize this)
let unit_collection = self
.variables_transition_relation_and_domain
.iter()
.fold(self.bdd_variable_set.mk_true(), |acc, (_, var_info)| {
acc.and(&var_info.domain.unit_collection(&self.bdd_variable_set))
});

let unpruned_res = target_domain
target_domain
.raw_bdd_variables()
.into_iter()
.zip(primed_domain.raw_bdd_variables())
.fold(forgor_old_val, |mut acc, (unprimed, primed)| {
unsafe { acc.rename_variable(primed, unprimed) };
acc
});

unpruned_res.and(&unit_collection)
})
}

/// Like `successors_async`, but a state that "transitions" to itself under
Expand Down
Loading

0 comments on commit 7d3b920

Please sign in to comment.