Skip to content
Snippets Groups Projects
Commit 2dd2db6e authored by Cookiebowser's avatar Cookiebowser
Browse files

fixed inefficiencies in rust template and started set-hash caching

parent ab734614
Branches
No related tags found
1 merge request!28Rust support
Show whitespace changes
Inline Side-by-side
benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
+ 12
− 60
View file @ 2dd2db6e
......@@ -11,6 +11,7 @@ use derivative::Derivative;
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::bboolean::IntoBool;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
use btypes::brelation::BRelation;
......@@ -49,7 +50,7 @@ impl sort_m2_data1000_MC {
return m;
}
fn init(&mut self) {
self.n = BInteger::new(1000);
self.n = BInteger::new(300);
let mut _ic_set_0 = BRelation::<BInteger, BInteger>::new(vec![]);
for _ic_i_1 in BSet::<BInteger>::interval(&BInteger::new(1), &self.n).clone().iter().cloned() {
_ic_set_0 = _ic_set_0._union(&BRelation::<BInteger, BInteger>::new(vec![BTuple::new(_ic_i_1, BInteger::new(15000).minus(&_ic_i_1))]));
......@@ -87,7 +88,7 @@ impl sort_m2_data1000_MC {
}
pub fn progress(&mut self) -> () {
if (self.k.unequal(&self.n).and(&self.j.equal(&self.n))).booleanValue() {
if (self.k.unequal(&self.n).booleanValue() && self.j.equal(&self.n).booleanValue()).booleanValue() {
let mut _ld_g = self.g.clone();
let mut _ld_k = self.k.clone();
let mut _ld_l = self.l.clone();
......@@ -101,7 +102,7 @@ impl sort_m2_data1000_MC {
}
pub fn prog1(&mut self) -> () {
if (self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
if (self.k.unequal(&self.n).booleanValue() && self.j.unequal(&self.n).booleanValue().booleanValue() && self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))).booleanValue()).booleanValue() {
let mut _ld_j = self.j.clone();
let mut _ld_l = self.l.clone();
self.l = _ld_l;
......@@ -112,7 +113,7 @@ impl sort_m2_data1000_MC {
}
pub fn prog2(&mut self) -> () {
if (self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
if (self.k.unequal(&self.n).booleanValue() && self.j.unequal(&self.n).booleanValue().booleanValue() && self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))).booleanValue()).booleanValue() {
let mut _ld_j = self.j.clone();
self.j = _ld_j.plus(&BInteger::new(1));
self.l = _ld_j.plus(&BInteger::new(1));
......@@ -131,7 +132,7 @@ impl sort_m2_data1000_MC {
pub fn _tr_progress(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_progress.is_none() {
let mut __tmp__val__ = self.k.unequal(&self.n).and(&self.j.equal(&self.n)).booleanValue();
let mut __tmp__val__ = self.k.unequal(&self.n).booleanValue() && self.j.equal(&self.n).booleanValue().booleanValue();
self._tr_cache_progress = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
......@@ -142,7 +143,7 @@ impl sort_m2_data1000_MC {
pub fn _tr_prog1(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_prog1.is_none() {
let mut __tmp__val__ = self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1))))).booleanValue();
let mut __tmp__val__ = self.k.unequal(&self.n).booleanValue() && self.j.unequal(&self.n).booleanValue().booleanValue() && self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))).booleanValue().booleanValue();
self._tr_cache_prog1 = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
......@@ -153,7 +154,7 @@ impl sort_m2_data1000_MC {
pub fn _tr_prog2(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_prog2.is_none() {
let mut __tmp__val__ = self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1))))).booleanValue();
let mut __tmp__val__ = self.k.unequal(&self.n).booleanValue() && self.j.unequal(&self.n).booleanValue().booleanValue() && self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))).booleanValue().booleanValue();
self._tr_cache_prog2 = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
......@@ -222,14 +223,9 @@ impl sort_m2_data1000_MC {
invariant_dependency: &HashMap<&str, HashSet<&'static str>>,
dependent_invariant_m: Arc<Mutex<HashMap<sort_m2_data1000_MC, HashSet<&str>>>>,
guard_dependency: &HashMap<&str, HashSet<&'static str>>,
dependent_guard_m: Arc<Mutex<HashMap<sort_m2_data1000_MC, HashSet<&str>>>>,
guardCache: Arc<Mutex<HashMap<sort_m2_data1000_MC, PersistentHashMap<&str, bool>>>>,
parents_m: Arc<Mutex<HashMap<sort_m2_data1000_MC, sort_m2_data1000_MC>>>,
transitions: Arc<AtomicI64>) -> HashSet<sort_m2_data1000_MC> {
let mut result = HashSet::<sort_m2_data1000_MC>::new();
if isCaching {
let mut parents_guard_o = parents_m.lock().unwrap().get(state).and_then(|p| guardCache.lock().unwrap().get(p).cloned());
let mut newCache = if parents_guard_o.is_none() { PersistentHashMap::new() } else { parents_guard_o.as_ref().unwrap().clone() };
//model_check_transition
let mut _trid_1 = state._tr_progress(isCaching);
if _trid_1 {
......@@ -239,18 +235,10 @@ impl sort_m2_data1000_MC {
match guard_dependency.get("progress") { Some(map) => copiedState.invalidate_caches(map), _ => (),}
{
let mut dependent_invariant = dependent_invariant_m.lock().unwrap();
let mut dependent_guard = dependent_guard_m.lock().unwrap();
let mut parents = parents_m.lock().unwrap();
if !dependent_invariant.contains_key(&copiedState) {
dependent_invariant.insert(copiedState.clone(), invariant_dependency.get("progress").unwrap().clone());
}
if !dependent_guard.contains_key(&copiedState) {
dependent_guard.insert(copiedState.clone(), guard_dependency.get("progress").unwrap().clone());
}
if !parents.contains_key(&copiedState) {
parents.insert(copiedState.clone(), state.clone());
}
}
result.insert(copiedState);
transitions.fetch_add(1, Ordering::AcqRel);
......@@ -264,18 +252,10 @@ impl sort_m2_data1000_MC {
match guard_dependency.get("prog1") { Some(map) => copiedState.invalidate_caches(map), _ => (),}
{
let mut dependent_invariant = dependent_invariant_m.lock().unwrap();
let mut dependent_guard = dependent_guard_m.lock().unwrap();
let mut parents = parents_m.lock().unwrap();
if !dependent_invariant.contains_key(&copiedState) {
dependent_invariant.insert(copiedState.clone(), invariant_dependency.get("prog1").unwrap().clone());
}
if !dependent_guard.contains_key(&copiedState) {
dependent_guard.insert(copiedState.clone(), guard_dependency.get("prog1").unwrap().clone());
}
if !parents.contains_key(&copiedState) {
parents.insert(copiedState.clone(), state.clone());
}
}
result.insert(copiedState);
transitions.fetch_add(1, Ordering::AcqRel);
......@@ -289,18 +269,10 @@ impl sort_m2_data1000_MC {
match guard_dependency.get("prog2") { Some(map) => copiedState.invalidate_caches(map), _ => (),}
{
let mut dependent_invariant = dependent_invariant_m.lock().unwrap();
let mut dependent_guard = dependent_guard_m.lock().unwrap();
let mut parents = parents_m.lock().unwrap();
if !dependent_invariant.contains_key(&copiedState) {
dependent_invariant.insert(copiedState.clone(), invariant_dependency.get("prog2").unwrap().clone());
}
if !dependent_guard.contains_key(&copiedState) {
dependent_guard.insert(copiedState.clone(), guard_dependency.get("prog2").unwrap().clone());
}
if !parents.contains_key(&copiedState) {
parents.insert(copiedState.clone(), state.clone());
}
}
result.insert(copiedState);
transitions.fetch_add(1, Ordering::AcqRel);
......@@ -314,24 +286,14 @@ impl sort_m2_data1000_MC {
match guard_dependency.get("final_evt") { Some(map) => copiedState.invalidate_caches(map), _ => (),}
{
let mut dependent_invariant = dependent_invariant_m.lock().unwrap();
let mut dependent_guard = dependent_guard_m.lock().unwrap();
let mut parents = parents_m.lock().unwrap();
if !dependent_invariant.contains_key(&copiedState) {
dependent_invariant.insert(copiedState.clone(), invariant_dependency.get("final_evt").unwrap().clone());
}
if !dependent_guard.contains_key(&copiedState) {
dependent_guard.insert(copiedState.clone(), guard_dependency.get("final_evt").unwrap().clone());
}
if !parents.contains_key(&copiedState) {
parents.insert(copiedState.clone(), state.clone());
}
}
result.insert(copiedState);
transitions.fetch_add(1, Ordering::AcqRel);
}
guardCache.lock().unwrap().insert(state.clone(), newCache);
} else {
//model_check_transition
if state._tr_progress(isCaching) {
......@@ -379,7 +341,8 @@ impl sort_m2_data1000_MC {
//model_check_invariants
pub fn checkInvariants(state: &sort_m2_data1000_MC,
isCaching: bool,
dependent_invariant_m: Arc<Mutex<HashMap<sort_m2_data1000_MC, HashSet<&str>>>> ) -> bool {
dependent_invariant_m: Arc<Mutex<HashMap<sort_m2_data1000_MC, HashSet<&str>>>> ) -> bool
{
let cached_invariants = dependent_invariant_m.lock().unwrap().get(&state).cloned();
if cached_invariants.is_some() && isCaching {
let dependent_invariants_of_state = cached_invariants.unwrap().clone();
......@@ -464,9 +427,6 @@ impl sort_m2_data1000_MC {
let mut invariantDependency = HashMap::<&str, HashSet<&'static str>>::new();
let mut guardDependency = HashMap::<&str, HashSet<&'static str>>::new();
let mut dependent_invariant_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, HashSet<&str>>::new()));
let mut dependent_guard_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, HashSet<&str>>::new()));
let mut guard_cache = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, PersistentHashMap<&'static str, bool>>::new()));
let mut parents_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, sort_m2_data1000_MC>::new()));
if is_caching {
//model_check_init_static
......@@ -486,7 +446,6 @@ impl sort_m2_data1000_MC {
//model_check_init_static
guardDependency.insert("final_evt", HashSet::from([]));
dependent_invariant_m.lock().unwrap().insert(machine.clone(), HashSet::new());
parents_m.lock().unwrap().remove(&machine);
}
let transitions = Arc::new(AtomicI64::new(0));
......@@ -494,7 +453,7 @@ impl sort_m2_data1000_MC {
while !stop_threads.load(Ordering::Acquire) && !collection_m.lock().unwrap().is_empty() {
let mut state = Self::next(Arc::clone(&collection_m), mc_type);
let next_states = Self::generateNextStates(&mut state, is_caching, &mut invariantDependency, Arc::clone(&dependent_invariant_m), &mut guardDependency, Arc::clone(&dependent_guard_m), Arc::clone(&guard_cache), Arc::clone(&parents_m), Arc::clone(&transitions));
let next_states = Self::generateNextStates(&mut state, is_caching, &mut invariantDependency, Arc::clone(&dependent_invariant_m), &mut guardDependency, Arc::clone(&transitions));
next_states.iter().cloned().for_each(|next_state| {
if !states.contains(&next_state) {
......@@ -548,9 +507,6 @@ impl sort_m2_data1000_MC {
let mut invariantDependency = HashMap::<&str, HashSet<&'static str>>::new();
let mut guardDependency = HashMap::<&str, HashSet<&'static str>>::new();
let mut dependent_invariant_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, HashSet<&str>>::new()));
let mut dependent_guard_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, HashSet<&str>>::new()));
let mut guard_cache_b = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, PersistentHashMap<&'static str, bool>>::new()));
let mut parents_m = Arc::new(Mutex::new(HashMap::<sort_m2_data1000_MC, sort_m2_data1000_MC>::new()));
if is_caching {
//model_check_init_static
......@@ -570,7 +526,6 @@ impl sort_m2_data1000_MC {
//model_check_init_static
guardDependency.insert("final_evt", HashSet::from([]));
dependent_invariant_m.lock().unwrap().insert(machine.clone(), HashSet::new());
parents_m.lock().unwrap().remove(&machine);
}
let num_transitions = Arc::new(AtomicI64::new(0));
......@@ -591,16 +546,13 @@ impl sort_m2_data1000_MC {
let invariant_dependency = Arc::clone(&invariant_dependency_arc);
let guard_dependency = Arc::clone(&guard_dependency_arc);
let dependent_invariant_m2 = Arc::clone(&dependent_invariant_m);
let dependent_guard_m2 = Arc::clone(&dependent_guard_m);
let parents_m2 = Arc::clone(&parents_m);
let guard_cache = Arc::clone(&guard_cache_b);
let transitions = Arc::clone(&num_transitions);
let states_m2 = Arc::clone(&states_m);
let number_states = Arc::clone(&number_states_arc);
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, &invariant_dependency, Arc::clone(&dependent_invariant_m2), &guard_dependency, dependent_guard_m2, guard_cache, parents_m2, Arc::clone(&transitions));
let next_states = Self::generateNextStates(&mut state, is_caching, &invariant_dependency, Arc::clone(&dependent_invariant_m2), &guard_dependency, Arc::clone(&transitions));
//println!("Thread {:?} executing", thread::current().id());
next_states.iter().cloned().for_each(|next_state| {
......
btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs 0 → 100644
+ 56
− 0
View file @ 2dd2db6e
use std::collections::hash_map::DefaultHasher;
use std::cell::RefCell;
use std::hash::{Hash, Hasher};
use im::OrdSet;
use crate::bobject::BObject;
#[derive(Default, Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
pub struct OrderedHashSet<I: BObject> {
set: OrdSet<I>,
hash_cache: RefCell<Option<u64>>,
}
impl<I: BObject> Hash for OrderedHashSet<I> {
fn hash<H: Hasher>(self: &OrderedHashSet<I>, state: &mut H) {
let cache = self.hash_cache.clone().take();
let hash: u64;
if cache.is_none() {
let mut hasher = DefaultHasher::new();
self.set.hash(&mut hasher);
hash = hasher.finish();
self.hash_cache.replace(Option::Some(hash));
} else {
hash = cache.unwrap();
}
hash.hash(state);
}
}
impl<I: BObject> OrderedHashSet<I> {
pub fn new() -> Self { Self::from_set(OrdSet::new()) }
pub fn from_set(val: OrdSet<I>) -> Self { OrderedHashSet {set: val, hash_cache: RefCell::new(Option::None)} }
pub fn unit(item: I) -> Self { Self::from_set(OrdSet::unit(item)) }
pub fn from(items: Vec<I>) -> Self { Self::from_set(OrdSet::from(items)) }
pub fn update(&self, item: I) -> Self { Self::from_set(self.set.update(item)) }
pub fn unions<A: IntoIterator<Item = Self>>(a: A) -> Self {
Self::from_set(OrdSet::unions(a))
}
pub fn iter(&self) -> Iter<I> { self.set.iter() }
pub fn len(&self) -> usize { self.set.len() }
pub fn is_empty(&self) -> bool { self.set.is_empty() }
pub fn contains(&self, value: &I) -> bool { self.set.contains(value) }
pub fn union(&self, other: Self) -> Self { Self::from_set(self.set.union(other.set)) }
pub fn intersection(&self, other: Self) -> Self { Self::from_set(self.set.intersection(other.set)) }
pub fn relative_complement(&self, other: Self) -> Self { Self::from_set(self.set.relative_complement(other.set)) }
}
\ No newline at end of file
btypes_primitives/src/main/rust/btypes/src/brelation.rs
+ 5
− 1
View file @ 2dd2db6e
......@@ -12,7 +12,8 @@ use std::hash::{Hash, Hasher};
use std::convert::TryInto;
use std::iter::FromIterator;
use rand::prelude::IteratorRandom;
use im::{HashMap, OrdSet};
use crate::orderedhashset::OrderedHashSet as OrdSet; //TODO try OrdMap instead
use im::OrdMap as HashMap;
use crate::bboolean::BBoolean;
use crate::brelation::CombiningType::{DIFFERENCE, INTERSECTION, UNION};
use crate::bset::{BSet, SetLike, TBSet};
......@@ -50,12 +51,15 @@ impl<L: BObject, R: BObject> Hash for BRelation<L, R> {
if cache.is_none() {
let mut hasher = DefaultHasher::new();
self.map.hash(&mut hasher);
/*
let mut kvs = self.map.iter().collect::<Vec<(&L, &OrdSet<R>)>>();
kvs.sort_by(|(k1, _v1), (k2, _v2)| k1.cmp(k2));
for (key, value) in kvs {
key.hash(&mut hasher);
value.iter().for_each(|v| v.hash(&mut hasher));
}
*/
hash = hasher.finish();
self.hash_cache.replace(Option::Some(hash));
} else {
......
btypes_primitives/src/main/rust/btypes/src/lib.rs
+ 1
− 0
View file @ 2dd2db6e
......@@ -10,3 +10,4 @@ pub mod bstring;
pub mod btuple;
pub mod brelation;
pub mod butils;
pub mod orderedhashset;
src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+ 4
− 29
View file @ 2dd2db6e
......@@ -771,16 +771,10 @@ fn generateNextStates(state: &mut <machine>,
invariant_dependency: &HashMap\<&str, HashSet\<&'static str>\>,
dependent_invariant_m: Arc\<Mutex\<HashMap\<<machine>, HashSet\<&str>\>\>>,
guard_dependency: &HashMap\<&str, HashSet\<&'static str\>>,
dependent_guard_m: Arc\<Mutex\<HashMap\<<machine>, HashSet\<&str>\>\>>,
guardCache: Arc\<Mutex\<HashMap\<<machine>, PersistentHashMap\<&str, bool>\>\>>,
parents_m: Arc\<Mutex\<HashMap\<<machine>, <machine>\>\>>,
transitions: Arc\<AtomicI64>) -> HashSet\<<machine>\> {
let mut result = HashSet::\<<machine>\>::new();
if isCaching {
let mut parents_guard_o = parents_m.lock().unwrap().get(state).and_then(|p| guardCache.lock().unwrap().get(p).cloned());
let mut newCache = if parents_guard_o.is_none() { PersistentHashMap::new() } else { parents_guard_o.as_ref().unwrap().clone() };
<transitionsWithCaching>
guardCache.lock().unwrap().insert(state.clone(), newCache);
} else {
<transitionsWithoutCaching>
}
......@@ -804,12 +798,12 @@ for param in <transitionIdentifier>.iter().cloned() {
<endif>
<else>
<if(isCaching)>
let mut <transitionIdentifier> = state.<evalTransitions>(isCaching);
let mut <transitionIdentifier> = state.<evalTransitions>(true);
if <transitionIdentifier> {
<execTransitions>
}
<else>
if state.<evalTransitions>(isCaching) {
if state.<evalTransitions>(false) {
<execTransitions>
}
<endif>
......@@ -851,18 +845,10 @@ match guard_dependency.get("<operation>") { Some(map) => copiedState.invalidate_
<if(isCaching)>
{
let mut dependent_invariant = dependent_invariant_m.lock().unwrap();
let mut dependent_guard = dependent_guard_m.lock().unwrap();
let mut parents = parents_m.lock().unwrap();
if !dependent_invariant.contains_key(&copiedState) {
dependent_invariant.insert(copiedState.clone(), invariant_dependency.get("<operation>").unwrap().clone());
}
if !dependent_guard.contains_key(&copiedState) {
dependent_guard.insert(copiedState.clone(), guard_dependency.get("<operation>").unwrap().clone());
}
if !parents.contains_key(&copiedState) {
parents.insert(copiedState.clone(), state.clone());
}
}
<endif>
result.insert(copiedState);
......@@ -939,15 +925,11 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
let mut invariantDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
let mut guardDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
let mut dependent_invariant_m = Arc::new(Mutex::new(HashMap::\<<machine>, HashSet\<&str>\>::new()));
let mut dependent_guard_m = Arc::new(Mutex::new(HashMap::\<<machine>, HashSet\<&str>\>::new()));
let mut guard_cache = Arc::new(Mutex::new(HashMap::\<<machine>, PersistentHashMap\<&'static str, bool\>>::new()));
let mut parents_m = Arc::new(Mutex::new(HashMap::\<<machine>, <machine>\>::new()));
if is_caching {
<invariantDependency; separator="\n">
<guardDependency; separator="\n">
dependent_invariant_m.lock().unwrap().insert(machine.clone(), HashSet::new());
parents_m.lock().unwrap().remove(&machine);
}
let transitions = Arc::new(AtomicI64::new(0));
......@@ -955,7 +937,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
while !stop_threads.load(Ordering::Acquire) && !collection_m.lock().unwrap().is_empty() {
let mut state = Self::next(Arc::clone(&collection_m), mc_type);
let next_states = Self::generateNextStates(&mut state, is_caching, &mut invariantDependency, Arc::clone(&dependent_invariant_m), &mut guardDependency, Arc::clone(&dependent_guard_m), Arc::clone(&guard_cache), Arc::clone(&parents_m), Arc::clone(&transitions));
let next_states = Self::generateNextStates(&mut state, is_caching, &mut invariantDependency, Arc::clone(&dependent_invariant_m), &mut guardDependency, Arc::clone(&transitions));
next_states.iter().cloned().for_each(|next_state| {
if !states.contains(&next_state) {
......@@ -1009,15 +991,11 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
let mut invariantDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
let mut guardDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
let mut dependent_invariant_m = Arc::new(Mutex::new(HashMap::\<<machine>, HashSet\<&str>\>::new()));
let mut dependent_guard_m = Arc::new(Mutex::new(HashMap::\<<machine>, HashSet\<&str>\>::new()));
let mut guard_cache_b = Arc::new(Mutex::new(HashMap::\<<machine>, PersistentHashMap\<&'static str, bool\>>::new()));
let mut parents_m = Arc::new(Mutex::new(HashMap::\<<machine>, <machine>\>::new()));
if is_caching {
<invariantDependency; separator="\n">
<guardDependency; separator="\n">
dependent_invariant_m.lock().unwrap().insert(machine.clone(), HashSet::new());
parents_m.lock().unwrap().remove(&machine);
}
let num_transitions = Arc::new(AtomicI64::new(0));
......@@ -1038,16 +1016,13 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
let invariant_dependency = Arc::clone(&invariant_dependency_arc);
let guard_dependency = Arc::clone(&guard_dependency_arc);
let dependent_invariant_m2 = Arc::clone(&dependent_invariant_m);
let dependent_guard_m2 = Arc::clone(&dependent_guard_m);
let parents_m2 = Arc::clone(&parents_m);
let guard_cache = Arc::clone(&guard_cache_b);
let transitions = Arc::clone(&num_transitions);
let states_m2 = Arc::clone(&states_m);
let number_states = Arc::clone(&number_states_arc);
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, &invariant_dependency, Arc::clone(&dependent_invariant_m2), &guard_dependency, dependent_guard_m2, guard_cache, parents_m2, Arc::clone(&transitions));
let next_states = Self::generateNextStates(&mut state, is_caching, &invariant_dependency, Arc::clone(&dependent_invariant_m2), &guard_dependency, Arc::clone(&transitions));
//println!("Thread {:?} executing", thread::current().id());
next_states.iter().cloned().for_each(|next_state| {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment