diff --git a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
index 0b8c31bc2299c602b3f1444f8d37be3e1697ec10..bc8cc4dd755e5ab00183959d4befe3b4449a4966 100644
--- a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
+++ b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
@@ -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| {
diff --git a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
new file mode 100644
index 0000000000000000000000000000000000000000..71b8ed5a4f6a32750e6668e6042159bceb405714
--- /dev/null
+++ b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
@@ -0,0 +1,56 @@
+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
diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
index fc4b023d9d80d3a8d938e0bd3b04af814dd26250..dd249fc99babac052e19103fe84b7057bb9a2c15 100644
--- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
@@ -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 {
diff --git a/btypes_primitives/src/main/rust/btypes/src/lib.rs b/btypes_primitives/src/main/rust/btypes/src/lib.rs
index 40a68be5c62027875e64e9be023af06ec00ce759..2f9ff7c4685867feaef86d121a73cb13770f7307 100644
--- a/btypes_primitives/src/main/rust/btypes/src/lib.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/lib.rs
@@ -10,3 +10,4 @@ pub mod bstring;
pub mod btuple;
pub mod brelation;
pub mod butils;
+pub mod orderedhashset;
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 9f6a0f91b85bd2a05e676382469e95a8cb913ce2..b6516a12bd242af35f2953ef176054044208475f 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -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| {