diff --git a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
index 564a59a407c5fd65054d7ca75591e56daacab8ee..66dffc50da5e566954f05a11fdc60e89c1ef53fd 100644
--- a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
+++ b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
@@ -1567,10 +1567,6 @@ impl CAN_BUS_tlc {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1579,6 +1575,9 @@ impl CAN_BUS_tlc {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1592,7 +1591,7 @@ impl CAN_BUS_tlc {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
index 3c75c4370810b7ebd5c4a6236b0d6f245220c94d..54815c76044f105c16132a73e9b6bdb1a8c0f636 100644
--- a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
+++ b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
@@ -1876,10 +1876,6 @@ impl Cruise_finite1_deterministic_MC {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1888,6 +1884,9 @@ impl Cruise_finite1_deterministic_MC {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1901,7 +1900,7 @@ impl Cruise_finite1_deterministic_MC {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/LandingGear_R6.rs b/benchmarks/model_checking/Rust/LandingGear_R6.rs
index 60e94590d2447ac06c93eaa51f5268bdb9425edf..016ef4e20cbc8eb49f226ee94c8e80b597d27e9a 100644
--- a/benchmarks/model_checking/Rust/LandingGear_R6.rs
+++ b/benchmarks/model_checking/Rust/LandingGear_R6.rs
@@ -2283,10 +2283,6 @@ impl LandingGear_R6 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -2295,6 +2291,9 @@ impl LandingGear_R6 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -2308,7 +2307,7 @@ impl LandingGear_R6 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Lift_MC_Large.rs b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
index 3e458e750db453b1496c8f2180f4adad6cb05ba4..a6d2852de22649ab73a611cb329f53dc86ed28a6 100644
--- a/benchmarks/model_checking/Rust/Lift_MC_Large.rs
+++ b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
@@ -270,10 +270,6 @@ impl Lift_MC_Large {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -282,6 +278,9 @@ impl Lift_MC_Large {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -295,7 +294,7 @@ impl Lift_MC_Large {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
index 7af2de3e37a983b86532ea80f68806712bb7c82c..868655dc95ec98eabcddfa98264acf21ccd6cd2b 100644
--- a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
+++ b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
@@ -356,10 +356,6 @@ impl QueensWithEvents_4 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -368,6 +364,9 @@ impl QueensWithEvents_4 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -381,7 +380,7 @@ impl QueensWithEvents_4 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
index 52284d90848b429bfabb17488bac0f9601df55da..f601ad28fbf11b6e90f03b4072c9234a538dd99b 100644
--- a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
+++ b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
@@ -933,10 +933,6 @@ impl Train1_Lukas_POR_v3 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -945,6 +941,9 @@ impl Train1_Lukas_POR_v3 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -958,7 +957,7 @@ impl Train1_Lukas_POR_v3 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs b/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
index b74c92f7d41671bae902e106caef881648b1e5bf..a9a40e693cea1af095cff8d02033635815a0e2b3 100644
--- a/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
+++ b/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
@@ -956,10 +956,6 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -968,6 +964,9 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -981,7 +980,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/nota_v2.rs b/benchmarks/model_checking/Rust/nota_v2.rs
index e4be01aa8806f081bb2e82ecdd48c11871f6c6c7..a52fae3f44cc3204d082dd6708e30d80c765ebde 100644
--- a/benchmarks/model_checking/Rust/nota_v2.rs
+++ b/benchmarks/model_checking/Rust/nota_v2.rs
@@ -1658,10 +1658,6 @@ impl nota_v2 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1670,6 +1666,9 @@ impl nota_v2 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1683,7 +1682,7 @@ impl nota_v2 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
index 73fe42acfa8168b695363fadb0193e6783041433..66673ae8f99ad16bd79dca71435b5e7901ca9760 100644
--- a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
+++ b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
@@ -442,10 +442,6 @@ impl sort_m2_data1000_MC {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -454,6 +450,9 @@ impl sort_m2_data1000_MC {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -467,7 +466,7 @@ impl sort_m2_data1000_MC {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
index d1eab3dffa1067b36e38952b53c5f77198e25e49..2b9cac648fa5ccd76766dffe6c447182e3f2e5e8 100644
--- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
@@ -84,19 +84,9 @@ 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();
- //println!("BRelation: cache miss");
self.hash_cache.replace(Option::Some(hash));
} else {
- //println!("BRelation: cache hit");
hash = cache.unwrap();
}
hash.hash(state);
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index b0171b192148a704bdf536336b034fd3e8576426..63e8c5dab228b56bf87ccf5af82c22b389003ead 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -951,10 +951,6 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -963,6 +959,9 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -976,7 +975,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },