From c2ec67b283efa220aef7e8ece429ecdd9cc87dd8 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Thu, 24 Feb 2022 16:23:13 +0100
Subject: [PATCH] fixed and/or not short-circuiting
---
benchmarks/model_checking/Rust/CAN_BUS_tlc.rs | 152 +++++++--------
.../Rust/Cruise_finite1_deterministic_MC.rs | 124 ++++++------
.../model_checking/Rust/LandingGear_R6.rs | 180 +++++++++---------
.../model_checking/Rust/Lift_MC_Large.rs | 26 +--
benchmarks/model_checking/Rust/Makefile | 2 +-
.../model_checking/Rust/QueensWithEvents_4.rs | 141 ++++++++------
.../model_checking/Rust/QueensWithEvents_8.rs | 141 ++++++++------
.../Rust/Train1_Lukas_POR_v3.rs | 110 +++++------
...Train_1_beebook_deterministic_MC_POR_v2.rs | 138 +++++++-------
benchmarks/model_checking/Rust/nota_v2.rs | 2 +-
.../Rust/sort_m2_data1000_MC.rs | 30 +--
.../src/main/rust/btypes/src/bboolean.rs | 21 +-
.../src/main/rust/btypes/src/bset.rs | 2 +-
.../hhu/stups/codegenerator/RustTemplate.stg | 5 +-
.../codegenerator/rust/TestMCBenchmarks.java | 2 +-
.../Cruise_finite1_deterministic_MC.out | 2 +-
.../hhu/stups/codegenerator/Lift_MC_Large.out | 2 +-
.../codegenerator/QueensWithEvents_8_MC.out | 3 +
18 files changed, 579 insertions(+), 504 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8_MC.out
diff --git a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
index c64836524..bde161e53 100644
--- a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
+++ b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
@@ -24,9 +24,9 @@ pub enum MC_TYPE { BFS, DFS, MIXED }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T1state {
- T1_EN,
- T1_CALC,
- T1_SEND,
+ T1_EN,
+ T1_CALC,
+ T1_SEND,
T1_WAIT
}
impl T1state {
@@ -39,19 +39,19 @@ impl Default for T1state {
}
impl fmt::Display for T1state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T1state::T1_EN => write!(f, "T1_EN"),
- T1state::T1_CALC => write!(f, "T1_CALC"),
- T1state::T1_SEND => write!(f, "T1_SEND"),
- T1state::T1_WAIT => write!(f, "T1_WAIT"),
- }
+ match *self {
+ T1state::T1_EN => write!(f, "T1_EN"),
+ T1state::T1_CALC => write!(f, "T1_CALC"),
+ T1state::T1_SEND => write!(f, "T1_SEND"),
+ T1state::T1_WAIT => write!(f, "T1_WAIT"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2mode {
- T2MODE_SENSE,
- T2MODE_TRANSMIT,
+ T2MODE_SENSE,
+ T2MODE_TRANSMIT,
T2MODE_RELEASE
}
impl T2mode {
@@ -64,22 +64,22 @@ impl Default for T2mode {
}
impl fmt::Display for T2mode {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T2mode::T2MODE_SENSE => write!(f, "T2MODE_SENSE"),
- T2mode::T2MODE_TRANSMIT => write!(f, "T2MODE_TRANSMIT"),
- T2mode::T2MODE_RELEASE => write!(f, "T2MODE_RELEASE"),
- }
+ match *self {
+ T2mode::T2MODE_SENSE => write!(f, "T2MODE_SENSE"),
+ T2mode::T2MODE_TRANSMIT => write!(f, "T2MODE_TRANSMIT"),
+ T2mode::T2MODE_RELEASE => write!(f, "T2MODE_RELEASE"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2state {
- T2_EN,
- T2_RCV,
- T2_PROC,
- T2_CALC,
- T2_SEND,
- T2_WAIT,
+ T2_EN,
+ T2_RCV,
+ T2_PROC,
+ T2_CALC,
+ T2_SEND,
+ T2_WAIT,
T2_RELEASE
}
impl T2state {
@@ -92,25 +92,25 @@ impl Default for T2state {
}
impl fmt::Display for T2state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T2state::T2_EN => write!(f, "T2_EN"),
- T2state::T2_RCV => write!(f, "T2_RCV"),
- T2state::T2_PROC => write!(f, "T2_PROC"),
- T2state::T2_CALC => write!(f, "T2_CALC"),
- T2state::T2_SEND => write!(f, "T2_SEND"),
- T2state::T2_WAIT => write!(f, "T2_WAIT"),
- T2state::T2_RELEASE => write!(f, "T2_RELEASE"),
- }
+ match *self {
+ T2state::T2_EN => write!(f, "T2_EN"),
+ T2state::T2_RCV => write!(f, "T2_RCV"),
+ T2state::T2_PROC => write!(f, "T2_PROC"),
+ T2state::T2_CALC => write!(f, "T2_CALC"),
+ T2state::T2_SEND => write!(f, "T2_SEND"),
+ T2state::T2_WAIT => write!(f, "T2_WAIT"),
+ T2state::T2_RELEASE => write!(f, "T2_RELEASE"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T3state {
- T3_READY,
- T3_WRITE,
- T3_RELEASE,
- T3_READ,
- T3_PROC,
+ T3_READY,
+ T3_WRITE,
+ T3_RELEASE,
+ T3_READ,
+ T3_PROC,
T3_WAIT
}
impl T3state {
@@ -123,14 +123,14 @@ impl Default for T3state {
}
impl fmt::Display for T3state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T3state::T3_READY => write!(f, "T3_READY"),
- T3state::T3_WRITE => write!(f, "T3_WRITE"),
- T3state::T3_RELEASE => write!(f, "T3_RELEASE"),
- T3state::T3_READ => write!(f, "T3_READ"),
- T3state::T3_PROC => write!(f, "T3_PROC"),
- T3state::T3_WAIT => write!(f, "T3_WAIT"),
- }
+ match *self {
+ T3state::T3_READY => write!(f, "T3_READY"),
+ T3state::T3_WRITE => write!(f, "T3_WRITE"),
+ T3state::T3_RELEASE => write!(f, "T3_RELEASE"),
+ T3state::T3_READ => write!(f, "T3_READ"),
+ T3state::T3_PROC => write!(f, "T3_PROC"),
+ T3state::T3_WAIT => write!(f, "T3_WAIT"),
+ }
}
}
@@ -917,27 +917,27 @@ impl CAN_BUS_tlc {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_T1Evaluate" => {self._tr_T1Evaluate(false);},
- "_tr_T1Calculate" => {self._tr_T1Calculate(false);},
- "_tr_T1SendResult" => {self._tr_T1SendResult(false);},
- "_tr_T1Wait" => {self._tr_T1Wait(false);},
- "_tr_T2Evaluate" => {self._tr_T2Evaluate(false);},
- "_tr_T2ReadBus" => {self._tr_T2ReadBus(false);},
- "_tr_T2Reset" => {self._tr_T2Reset(false);},
- "_tr_T2Complete" => {self._tr_T2Complete(false);},
- "_tr_T2ReleaseBus" => {self._tr_T2ReleaseBus(false);},
- "_tr_T2Calculate" => {self._tr_T2Calculate(false);},
- "_tr_T2WriteBus" => {self._tr_T2WriteBus(false);},
- "_tr_T2Wait" => {self._tr_T2Wait(false);},
- "_tr_T3Initiate" => {self._tr_T3Initiate(false);},
- "_tr_T3Evaluate" => {self._tr_T3Evaluate(false);},
- "_tr_T3writebus" => {self._tr_T3writebus(false);},
- "_tr_T3Read" => {self._tr_T3Read(false);},
- "_tr_T3Poll" => {self._tr_T3Poll(false);},
- "_tr_T3ReleaseBus" => {self._tr_T3ReleaseBus(false);},
- "_tr_T3Wait" => {self._tr_T3Wait(false);},
- "_tr_T3ReEnableWait" => {self._tr_T3ReEnableWait(false);},
- "_tr_Update" => {self._tr_Update(false);},
+ "_tr_T1Evaluate" => {self._tr_T1Evaluate(false);},
+ "_tr_T1Calculate" => {self._tr_T1Calculate(false);},
+ "_tr_T1SendResult" => {self._tr_T1SendResult(false);},
+ "_tr_T1Wait" => {self._tr_T1Wait(false);},
+ "_tr_T2Evaluate" => {self._tr_T2Evaluate(false);},
+ "_tr_T2ReadBus" => {self._tr_T2ReadBus(false);},
+ "_tr_T2Reset" => {self._tr_T2Reset(false);},
+ "_tr_T2Complete" => {self._tr_T2Complete(false);},
+ "_tr_T2ReleaseBus" => {self._tr_T2ReleaseBus(false);},
+ "_tr_T2Calculate" => {self._tr_T2Calculate(false);},
+ "_tr_T2WriteBus" => {self._tr_T2WriteBus(false);},
+ "_tr_T2Wait" => {self._tr_T2Wait(false);},
+ "_tr_T3Initiate" => {self._tr_T3Initiate(false);},
+ "_tr_T3Evaluate" => {self._tr_T3Evaluate(false);},
+ "_tr_T3writebus" => {self._tr_T3writebus(false);},
+ "_tr_T3Read" => {self._tr_T3Read(false);},
+ "_tr_T3Poll" => {self._tr_T3Poll(false);},
+ "_tr_T3ReleaseBus" => {self._tr_T3ReleaseBus(false);},
+ "_tr_T3Wait" => {self._tr_T3Wait(false);},
+ "_tr_T3ReEnableWait" => {self._tr_T3ReEnableWait(false);},
+ "_tr_Update" => {self._tr_Update(false);},
_ => {},
}
}
@@ -1923,10 +1923,10 @@ impl CAN_BUS_tlc {
fn next(collection_m: Arc<Mutex<LinkedList<CAN_BUS_tlc>>>, mc_type: MC_TYPE) -> CAN_BUS_tlc {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -2050,11 +2050,11 @@ impl CAN_BUS_tlc {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -2089,7 +2089,7 @@ impl CAN_BUS_tlc {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() || !machine._check_inv_7() || !machine._check_inv_8() || !machine._check_inv_9() || !machine._check_inv_10() || !machine._check_inv_11() || !machine._check_inv_12() || !machine._check_inv_13() || !machine._check_inv_14() || !machine._check_inv_15() || !machine._check_inv_16() || !machine._check_inv_17() || !machine._check_inv_18() || !machine._check_inv_19() || !machine._check_inv_20() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<CAN_BUS_tlc>::new()));
@@ -2225,14 +2225,14 @@ impl CAN_BUS_tlc {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
index 3d879f315..7f12bc7b4 100644
--- a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
+++ b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
@@ -23,9 +23,9 @@ pub enum MC_TYPE { BFS, DFS, MIXED }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum RSset {
- RSnone,
- RSpos,
- RSneg,
+ RSnone,
+ RSpos,
+ RSneg,
RSequal
}
impl RSset {
@@ -38,19 +38,19 @@ impl Default for RSset {
}
impl fmt::Display for RSset {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- RSset::RSnone => write!(f, "RSnone"),
- RSset::RSpos => write!(f, "RSpos"),
- RSset::RSneg => write!(f, "RSneg"),
- RSset::RSequal => write!(f, "RSequal"),
- }
+ match *self {
+ RSset::RSnone => write!(f, "RSnone"),
+ RSset::RSpos => write!(f, "RSpos"),
+ RSset::RSneg => write!(f, "RSneg"),
+ RSset::RSequal => write!(f, "RSequal"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ODset {
- ODnone,
- ODclose,
+ ODnone,
+ ODclose,
ODveryclose
}
impl ODset {
@@ -63,11 +63,11 @@ impl Default for ODset {
}
impl fmt::Display for ODset {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- ODset::ODnone => write!(f, "ODnone"),
- ODset::ODclose => write!(f, "ODclose"),
- ODset::ODveryclose => write!(f, "ODveryclose"),
- }
+ match *self {
+ ODset::ODnone => write!(f, "ODnone"),
+ ODset::ODclose => write!(f, "ODclose"),
+ ODset::ODveryclose => write!(f, "ODveryclose"),
+ }
}
}
@@ -287,7 +287,7 @@ impl Cruise_finite1_deterministic_MC {
}
if (_ld_NumberOfSetCruise.less(&BInteger::new(1))).booleanValue() {
self.NumberOfSetCruise = _ld_NumberOfSetCruise.plus(&BInteger::new(1));
- }
+ }
}
@@ -387,7 +387,7 @@ impl Cruise_finite1_deterministic_MC {
self.SpeedAboveMax = BBoolean::new(false);
if (self.CruiseActive.equal(&BBoolean::new(true)).and(&self.CruiseSpeedAtMax.equal(&BBoolean::new(true)))).booleanValue() {
self.VehicleAtCruiseSpeed = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -408,7 +408,7 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleStatusJustChanged = BBoolean::new(true);
if (self.ObstacleRelativeSpeed.equal(&RSset::RSpos)).booleanValue() {
self.VehicleTryKeepTimeGap = BBoolean::new(false);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -429,10 +429,10 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleRelativeSpeed = RSset::RSpos;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
if (self.ObstacleDistance.unequal(&ODset::ODveryclose)).booleanValue() {
self.VehicleTryKeepTimeGap = BBoolean::new(false);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -443,7 +443,7 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleRelativeSpeed = RSset::RSequal;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -454,7 +454,7 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleRelativeSpeed = RSset::RSneg;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -465,7 +465,7 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleRelativeSpeed = RSset::RSequal;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -494,7 +494,7 @@ impl Cruise_finite1_deterministic_MC {
self.ObstacleRelativeSpeed = RSset::RSnone;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
self.ObstacleDistance = ODset::ODnone;
self.VehicleTryKeepTimeGap = BBoolean::new(false);
} else {
@@ -1051,32 +1051,32 @@ impl Cruise_finite1_deterministic_MC {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_CruiseBecomesNotAllowed" => {self._tr_CruiseBecomesNotAllowed(false);},
- "_tr_CruiseBecomesAllowed" => {self._tr_CruiseBecomesAllowed(false);},
- "_tr_SetCruiseSpeed" => {self._tr_SetCruiseSpeed(false);},
- "_tr_CCInitialisationFinished" => {self._tr_CCInitialisationFinished(false);},
- "_tr_CCInitialisationDelayFinished" => {self._tr_CCInitialisationDelayFinished(false);},
- "_tr_CruiseSpeedChangeFinished" => {self._tr_CruiseSpeedChangeFinished(false);},
- "_tr_CruiseSpeedChangeDelayFinished" => {self._tr_CruiseSpeedChangeDelayFinished(false);},
- "_tr_CruiseOff" => {self._tr_CruiseOff(false);},
- "_tr_ExternalForcesBecomesExtreme" => {self._tr_ExternalForcesBecomesExtreme(false);},
- "_tr_ExternalForcesBecomesNormal" => {self._tr_ExternalForcesBecomesNormal(false);},
- "_tr_VehicleLeavesCruiseSpeed" => {self._tr_VehicleLeavesCruiseSpeed(false);},
- "_tr_VehicleReachesCruiseSpeed" => {self._tr_VehicleReachesCruiseSpeed(false);},
- "_tr_VehicleExceedsMaxCruiseSpeed" => {self._tr_VehicleExceedsMaxCruiseSpeed(false);},
- "_tr_VehicleFallsBelowMaxCruiseSpeed" => {self._tr_VehicleFallsBelowMaxCruiseSpeed(false);},
- "_tr_ObstacleDistanceBecomesVeryClose" => {self._tr_ObstacleDistanceBecomesVeryClose(false);},
- "_tr_ObstacleDistanceBecomesClose" => {self._tr_ObstacleDistanceBecomesClose(false);},
- "_tr_ObstacleDistanceBecomesBig" => {self._tr_ObstacleDistanceBecomesBig(false);},
- "_tr_ObstacleStartsTravelFaster" => {self._tr_ObstacleStartsTravelFaster(false);},
- "_tr_ObstacleStopsTravelFaster" => {self._tr_ObstacleStopsTravelFaster(false);},
- "_tr_ObstacleStartsTravelSlower" => {self._tr_ObstacleStartsTravelSlower(false);},
- "_tr_ObstacleStopsTravelSlower" => {self._tr_ObstacleStopsTravelSlower(false);},
- "_tr_ObstacleAppearsWhenCruiseActive" => {self._tr_ObstacleAppearsWhenCruiseActive(false);},
- "_tr_ObstacleAppearsWhenCruiseInactive" => {self._tr_ObstacleAppearsWhenCruiseInactive(false);},
- "_tr_ObstacleDisappears" => {self._tr_ObstacleDisappears(false);},
- "_tr_VehicleManageObstacle" => {self._tr_VehicleManageObstacle(false);},
- "_tr_ObstacleBecomesOld" => {self._tr_ObstacleBecomesOld(false);},
+ "_tr_CruiseBecomesNotAllowed" => {self._tr_CruiseBecomesNotAllowed(false);},
+ "_tr_CruiseBecomesAllowed" => {self._tr_CruiseBecomesAllowed(false);},
+ "_tr_SetCruiseSpeed" => {self._tr_SetCruiseSpeed(false);},
+ "_tr_CCInitialisationFinished" => {self._tr_CCInitialisationFinished(false);},
+ "_tr_CCInitialisationDelayFinished" => {self._tr_CCInitialisationDelayFinished(false);},
+ "_tr_CruiseSpeedChangeFinished" => {self._tr_CruiseSpeedChangeFinished(false);},
+ "_tr_CruiseSpeedChangeDelayFinished" => {self._tr_CruiseSpeedChangeDelayFinished(false);},
+ "_tr_CruiseOff" => {self._tr_CruiseOff(false);},
+ "_tr_ExternalForcesBecomesExtreme" => {self._tr_ExternalForcesBecomesExtreme(false);},
+ "_tr_ExternalForcesBecomesNormal" => {self._tr_ExternalForcesBecomesNormal(false);},
+ "_tr_VehicleLeavesCruiseSpeed" => {self._tr_VehicleLeavesCruiseSpeed(false);},
+ "_tr_VehicleReachesCruiseSpeed" => {self._tr_VehicleReachesCruiseSpeed(false);},
+ "_tr_VehicleExceedsMaxCruiseSpeed" => {self._tr_VehicleExceedsMaxCruiseSpeed(false);},
+ "_tr_VehicleFallsBelowMaxCruiseSpeed" => {self._tr_VehicleFallsBelowMaxCruiseSpeed(false);},
+ "_tr_ObstacleDistanceBecomesVeryClose" => {self._tr_ObstacleDistanceBecomesVeryClose(false);},
+ "_tr_ObstacleDistanceBecomesClose" => {self._tr_ObstacleDistanceBecomesClose(false);},
+ "_tr_ObstacleDistanceBecomesBig" => {self._tr_ObstacleDistanceBecomesBig(false);},
+ "_tr_ObstacleStartsTravelFaster" => {self._tr_ObstacleStartsTravelFaster(false);},
+ "_tr_ObstacleStopsTravelFaster" => {self._tr_ObstacleStopsTravelFaster(false);},
+ "_tr_ObstacleStartsTravelSlower" => {self._tr_ObstacleStartsTravelSlower(false);},
+ "_tr_ObstacleStopsTravelSlower" => {self._tr_ObstacleStopsTravelSlower(false);},
+ "_tr_ObstacleAppearsWhenCruiseActive" => {self._tr_ObstacleAppearsWhenCruiseActive(false);},
+ "_tr_ObstacleAppearsWhenCruiseInactive" => {self._tr_ObstacleAppearsWhenCruiseInactive(false);},
+ "_tr_ObstacleDisappears" => {self._tr_ObstacleDisappears(false);},
+ "_tr_VehicleManageObstacle" => {self._tr_VehicleManageObstacle(false);},
+ "_tr_ObstacleBecomesOld" => {self._tr_ObstacleBecomesOld(false);},
_ => {},
}
}
@@ -2311,10 +2311,10 @@ impl Cruise_finite1_deterministic_MC {
fn next(collection_m: Arc<Mutex<LinkedList<Cruise_finite1_deterministic_MC>>>, mc_type: MC_TYPE) -> Cruise_finite1_deterministic_MC {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -2458,11 +2458,11 @@ impl Cruise_finite1_deterministic_MC {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -2497,7 +2497,7 @@ impl Cruise_finite1_deterministic_MC {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() || !machine._check_inv_7() || !machine._check_inv_8() || !machine._check_inv_9() || !machine._check_inv_10() || !machine._check_inv_11() || !machine._check_inv_12() || !machine._check_inv_13() || !machine._check_inv_14() || !machine._check_inv_15() || !machine._check_inv_16() || !machine._check_inv_17() || !machine._check_inv_18() || !machine._check_inv_19() || !machine._check_inv_20() || !machine._check_inv_21() || !machine._check_inv_22() || !machine._check_inv_23() || !machine._check_inv_24() || !machine._check_inv_25() || !machine._check_inv_26() || !machine._check_inv_27() || !machine._check_inv_28() || !machine._check_inv_29() || !machine._check_inv_30() || !machine._check_inv_31() || !machine._check_inv_32() || !machine._check_inv_33() || !machine._check_inv_34() || !machine._check_inv_35() || !machine._check_inv_36() || !machine._check_inv_37() || !machine._check_inv_38() || !machine._check_inv_39() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<Cruise_finite1_deterministic_MC>::new()));
@@ -2653,14 +2653,14 @@ impl Cruise_finite1_deterministic_MC {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/LandingGear_R6.rs b/benchmarks/model_checking/Rust/LandingGear_R6.rs
index d511b15fe..c5d829d63 100644
--- a/benchmarks/model_checking/Rust/LandingGear_R6.rs
+++ b/benchmarks/model_checking/Rust/LandingGear_R6.rs
@@ -23,8 +23,8 @@ pub enum MC_TYPE { BFS, DFS, MIXED }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum DOOR_STATE {
- open,
- closed,
+ open,
+ closed,
door_moving
}
impl DOOR_STATE {
@@ -37,18 +37,18 @@ impl Default for DOOR_STATE {
}
impl fmt::Display for DOOR_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- DOOR_STATE::open => write!(f, "open"),
- DOOR_STATE::closed => write!(f, "closed"),
- DOOR_STATE::door_moving => write!(f, "door_moving"),
- }
+ match *self {
+ DOOR_STATE::open => write!(f, "open"),
+ DOOR_STATE::closed => write!(f, "closed"),
+ DOOR_STATE::door_moving => write!(f, "door_moving"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum GEAR_STATE {
- retracted,
- extended,
+ retracted,
+ extended,
gear_moving
}
impl GEAR_STATE {
@@ -61,17 +61,17 @@ impl Default for GEAR_STATE {
}
impl fmt::Display for GEAR_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- GEAR_STATE::retracted => write!(f, "retracted"),
- GEAR_STATE::extended => write!(f, "extended"),
- GEAR_STATE::gear_moving => write!(f, "gear_moving"),
- }
+ match *self {
+ GEAR_STATE::retracted => write!(f, "retracted"),
+ GEAR_STATE::extended => write!(f, "extended"),
+ GEAR_STATE::gear_moving => write!(f, "gear_moving"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum HANDLE_STATE {
- up,
+ up,
down
}
impl HANDLE_STATE {
@@ -84,17 +84,17 @@ impl Default for HANDLE_STATE {
}
impl fmt::Display for HANDLE_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- HANDLE_STATE::up => write!(f, "up"),
- HANDLE_STATE::down => write!(f, "down"),
- }
+ match *self {
+ HANDLE_STATE::up => write!(f, "up"),
+ HANDLE_STATE::down => write!(f, "down"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum POSITION {
- fr,
- lt,
+ fr,
+ lt,
rt
}
impl POSITION {
@@ -107,17 +107,17 @@ impl Default for POSITION {
}
impl fmt::Display for POSITION {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- POSITION::fr => write!(f, "fr"),
- POSITION::lt => write!(f, "lt"),
- POSITION::rt => write!(f, "rt"),
- }
+ match *self {
+ POSITION::fr => write!(f, "fr"),
+ POSITION::lt => write!(f, "lt"),
+ POSITION::rt => write!(f, "rt"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum SWITCH_STATE {
- switch_open,
+ switch_open,
switch_closed
}
impl SWITCH_STATE {
@@ -130,16 +130,16 @@ impl Default for SWITCH_STATE {
}
impl fmt::Display for SWITCH_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- SWITCH_STATE::switch_open => write!(f, "switch_open"),
- SWITCH_STATE::switch_closed => write!(f, "switch_closed"),
- }
+ match *self {
+ SWITCH_STATE::switch_open => write!(f, "switch_open"),
+ SWITCH_STATE::switch_closed => write!(f, "switch_closed"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum PLANE_STATE {
- ground,
+ ground,
flight
}
impl PLANE_STATE {
@@ -152,16 +152,16 @@ impl Default for PLANE_STATE {
}
impl fmt::Display for PLANE_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- PLANE_STATE::ground => write!(f, "ground"),
- PLANE_STATE::flight => write!(f, "flight"),
- }
+ match *self {
+ PLANE_STATE::ground => write!(f, "ground"),
+ PLANE_STATE::flight => write!(f, "flight"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum VALVE_STATE {
- valve_open,
+ valve_open,
valve_closed
}
impl VALVE_STATE {
@@ -174,10 +174,10 @@ impl Default for VALVE_STATE {
}
impl fmt::Display for VALVE_STATE {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- VALVE_STATE::valve_open => write!(f, "valve_open"),
- VALVE_STATE::valve_closed => write!(f, "valve_closed"),
- }
+ match *self {
+ VALVE_STATE::valve_open => write!(f, "valve_open"),
+ VALVE_STATE::valve_closed => write!(f, "valve_closed"),
+ }
}
}
@@ -1365,44 +1365,44 @@ impl LandingGear_R6 {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_begin_flying" => {self._tr_begin_flying(false);},
- "_tr_land_plane" => {self._tr_land_plane(false);},
- "_tr_open_valve_door_open" => {self._tr_open_valve_door_open(false);},
- "_tr_close_valve_door_open" => {self._tr_close_valve_door_open(false);},
- "_tr_open_valve_door_close" => {self._tr_open_valve_door_close(false);},
- "_tr_close_valve_door_close" => {self._tr_close_valve_door_close(false);},
- "_tr_open_valve_retract_gear" => {self._tr_open_valve_retract_gear(false);},
- "_tr_close_valve_retract_gear" => {self._tr_close_valve_retract_gear(false);},
- "_tr_open_valve_extend_gear" => {self._tr_open_valve_extend_gear(false);},
- "_tr_close_valve_extend_gear" => {self._tr_close_valve_extend_gear(false);},
- "_tr_con_stimulate_open_door_valve" => {self._tr_con_stimulate_open_door_valve(false);},
- "_tr_con_stop_stimulate_open_door_valve" => {self._tr_con_stop_stimulate_open_door_valve(false);},
- "_tr_con_stimulate_close_door_valve" => {self._tr_con_stimulate_close_door_valve(false);},
- "_tr_con_stop_stimulate_close_door_valve" => {self._tr_con_stop_stimulate_close_door_valve(false);},
- "_tr_con_stimulate_retract_gear_valve" => {self._tr_con_stimulate_retract_gear_valve(false);},
- "_tr_con_stop_stimulate_retract_gear_valve" => {self._tr_con_stop_stimulate_retract_gear_valve(false);},
- "_tr_con_stimulate_extend_gear_valve" => {self._tr_con_stimulate_extend_gear_valve(false);},
- "_tr_con_stop_stimulate_extend_gear_valve" => {self._tr_con_stop_stimulate_extend_gear_valve(false);},
- "_tr_env_start_retracting_first" => {self._tr_env_start_retracting_first(false);},
- "_tr_env_retract_gear_skip" => {self._tr_env_retract_gear_skip(false);},
- "_tr_env_retract_gear_last" => {self._tr_env_retract_gear_last(false);},
- "_tr_env_start_extending" => {self._tr_env_start_extending(false);},
- "_tr_env_extend_gear_last" => {self._tr_env_extend_gear_last(false);},
- "_tr_env_extend_gear_skip" => {self._tr_env_extend_gear_skip(false);},
- "_tr_env_start_open_door" => {self._tr_env_start_open_door(false);},
- "_tr_env_open_door_last" => {self._tr_env_open_door_last(false);},
- "_tr_env_open_door_skip" => {self._tr_env_open_door_skip(false);},
- "_tr_env_start_close_door" => {self._tr_env_start_close_door(false);},
- "_tr_env_close_door" => {self._tr_env_close_door(false);},
- "_tr_env_close_door_skip" => {self._tr_env_close_door_skip(false);},
- "_tr_toggle_handle_up" => {self._tr_toggle_handle_up(false);},
- "_tr_toggle_handle_down" => {self._tr_toggle_handle_down(false);},
- "_tr_con_stimulate_general_valve" => {self._tr_con_stimulate_general_valve(false);},
- "_tr_con_stop_stimulate_general_valve" => {self._tr_con_stop_stimulate_general_valve(false);},
- "_tr_evn_open_general_valve" => {self._tr_evn_open_general_valve(false);},
- "_tr_evn_close_general_valve" => {self._tr_evn_close_general_valve(false);},
- "_tr_env_close_analogical_switch" => {self._tr_env_close_analogical_switch(false);},
- "_tr_env_open_analogical_switch" => {self._tr_env_open_analogical_switch(false);},
+ "_tr_begin_flying" => {self._tr_begin_flying(false);},
+ "_tr_land_plane" => {self._tr_land_plane(false);},
+ "_tr_open_valve_door_open" => {self._tr_open_valve_door_open(false);},
+ "_tr_close_valve_door_open" => {self._tr_close_valve_door_open(false);},
+ "_tr_open_valve_door_close" => {self._tr_open_valve_door_close(false);},
+ "_tr_close_valve_door_close" => {self._tr_close_valve_door_close(false);},
+ "_tr_open_valve_retract_gear" => {self._tr_open_valve_retract_gear(false);},
+ "_tr_close_valve_retract_gear" => {self._tr_close_valve_retract_gear(false);},
+ "_tr_open_valve_extend_gear" => {self._tr_open_valve_extend_gear(false);},
+ "_tr_close_valve_extend_gear" => {self._tr_close_valve_extend_gear(false);},
+ "_tr_con_stimulate_open_door_valve" => {self._tr_con_stimulate_open_door_valve(false);},
+ "_tr_con_stop_stimulate_open_door_valve" => {self._tr_con_stop_stimulate_open_door_valve(false);},
+ "_tr_con_stimulate_close_door_valve" => {self._tr_con_stimulate_close_door_valve(false);},
+ "_tr_con_stop_stimulate_close_door_valve" => {self._tr_con_stop_stimulate_close_door_valve(false);},
+ "_tr_con_stimulate_retract_gear_valve" => {self._tr_con_stimulate_retract_gear_valve(false);},
+ "_tr_con_stop_stimulate_retract_gear_valve" => {self._tr_con_stop_stimulate_retract_gear_valve(false);},
+ "_tr_con_stimulate_extend_gear_valve" => {self._tr_con_stimulate_extend_gear_valve(false);},
+ "_tr_con_stop_stimulate_extend_gear_valve" => {self._tr_con_stop_stimulate_extend_gear_valve(false);},
+ "_tr_env_start_retracting_first" => {self._tr_env_start_retracting_first(false);},
+ "_tr_env_retract_gear_skip" => {self._tr_env_retract_gear_skip(false);},
+ "_tr_env_retract_gear_last" => {self._tr_env_retract_gear_last(false);},
+ "_tr_env_start_extending" => {self._tr_env_start_extending(false);},
+ "_tr_env_extend_gear_last" => {self._tr_env_extend_gear_last(false);},
+ "_tr_env_extend_gear_skip" => {self._tr_env_extend_gear_skip(false);},
+ "_tr_env_start_open_door" => {self._tr_env_start_open_door(false);},
+ "_tr_env_open_door_last" => {self._tr_env_open_door_last(false);},
+ "_tr_env_open_door_skip" => {self._tr_env_open_door_skip(false);},
+ "_tr_env_start_close_door" => {self._tr_env_start_close_door(false);},
+ "_tr_env_close_door" => {self._tr_env_close_door(false);},
+ "_tr_env_close_door_skip" => {self._tr_env_close_door_skip(false);},
+ "_tr_toggle_handle_up" => {self._tr_toggle_handle_up(false);},
+ "_tr_toggle_handle_down" => {self._tr_toggle_handle_down(false);},
+ "_tr_con_stimulate_general_valve" => {self._tr_con_stimulate_general_valve(false);},
+ "_tr_con_stop_stimulate_general_valve" => {self._tr_con_stop_stimulate_general_valve(false);},
+ "_tr_evn_open_general_valve" => {self._tr_evn_open_general_valve(false);},
+ "_tr_evn_close_general_valve" => {self._tr_evn_close_general_valve(false);},
+ "_tr_env_close_analogical_switch" => {self._tr_env_close_analogical_switch(false);},
+ "_tr_env_open_analogical_switch" => {self._tr_env_open_analogical_switch(false);},
_ => {},
}
}
@@ -2983,10 +2983,10 @@ impl LandingGear_R6 {
fn next(collection_m: Arc<Mutex<LinkedList<LandingGear_R6>>>, mc_type: MC_TYPE) -> LandingGear_R6 {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -3178,11 +3178,11 @@ impl LandingGear_R6 {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -3217,7 +3217,7 @@ impl LandingGear_R6 {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() || !machine._check_inv_7() || !machine._check_inv_8() || !machine._check_inv_9() || !machine._check_inv_10() || !machine._check_inv_11() || !machine._check_inv_12() || !machine._check_inv_13() || !machine._check_inv_14() || !machine._check_inv_15() || !machine._check_inv_16() || !machine._check_inv_17() || !machine._check_inv_18() || !machine._check_inv_19() || !machine._check_inv_20() || !machine._check_inv_21() || !machine._check_inv_22() || !machine._check_inv_23() || !machine._check_inv_24() || !machine._check_inv_25() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<LandingGear_R6>::new()));
@@ -3421,14 +3421,14 @@ impl LandingGear_R6 {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/Lift_MC_Large.rs b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
index 6124243dc..7dd7d1805 100644
--- a/benchmarks/model_checking/Rust/Lift_MC_Large.rs
+++ b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
@@ -94,8 +94,8 @@ impl Lift_MC_Large {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_inc" => {self._tr_inc(false);},
- "_tr_dec" => {self._tr_dec(false);},
+ "_tr_inc" => {self._tr_inc(false);},
+ "_tr_dec" => {self._tr_dec(false);},
_ => {},
}
}
@@ -230,10 +230,10 @@ impl Lift_MC_Large {
fn next(collection_m: Arc<Mutex<LinkedList<Lift_MC_Large>>>, mc_type: MC_TYPE) -> Lift_MC_Large {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -281,11 +281,11 @@ impl Lift_MC_Large {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -320,7 +320,7 @@ impl Lift_MC_Large {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<Lift_MC_Large>::new()));
@@ -380,14 +380,14 @@ impl Lift_MC_Large {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/Makefile b/benchmarks/model_checking/Rust/Makefile
index 9cfaf0b48..16351e5c1 100644
--- a/benchmarks/model_checking/Rust/Makefile
+++ b/benchmarks/model_checking/Rust/Makefile
@@ -2,7 +2,7 @@
.PHONY: all clean
-all: CAN_BUS_tlc Cruise_finite1_deterministic_MC LandingGear_R6 Lift_MC_Large nota_v2 QueensWithEvents_4 QueensWithEvents_8 sort_m2_data1000_MC Train1_Lukas_POR_v3 Train_1_beebook_deterministic_MC_POR_v2
+all: CAN_BUS_tlc Cruise_finite1_deterministic_MC LandingGear_R6 Lift_MC_Large sort_m2_data1000_MC QueensWithEvents_4 Train1_Lukas_POR_v3 Train_1_beebook_deterministic_MC_POR_v2 nota_v2 QueensWithEvents_8
OUTPUT ?= runtimes.txt
diff --git a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
index 3efa82b75..3a5756de8 100644
--- a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
+++ b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
@@ -64,42 +64,56 @@ impl QueensWithEvents_4 {
}
pub fn Solve(&mut self, mut solution: BRelation<BInteger, BInteger>) -> () {
+ //quantified_predicate
let mut _ic_boolean_1 = BBoolean::new(true);
- for _ic_x_1 in self.interval.clone().iter().cloned() {
- for _ic_y_1 in self.interval.clone().iter().cloned() {
- let mut _ic_boolean_0 = BBoolean::new(true);
- for _ic_z_1 in self.interval.clone().iter().cloned() {
- if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
- _ic_boolean_0 = BBoolean::new(false);
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).booleanValue() {
+ for _ic_x_1 in self.interval.clone().iter().cloned() {
+ for _ic_y_1 in self.interval.clone().iter().cloned() {
+ //quantified_predicate
+ let mut _ic_boolean_0 = BBoolean::new(true);
+ for _ic_z_1 in self.interval.clone().iter().cloned() {
+ if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
+ _ic_boolean_0 = BBoolean::new(false);
+ break;
+ }
+
+ }
+
+ if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_0)).booleanValue() {
+ _ic_boolean_1 = BBoolean::new(false);
break;
}
}
- if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_0)).booleanValue() {
- _ic_boolean_1 = BBoolean::new(false);
- break;
- }
-
}
}
+
+ //quantified_predicate
let mut _ic_boolean_2 = BBoolean::new(true);
- for _ic_q1_1 in self.interval.clone().iter().cloned() {
- for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
- if !(_ic_q2_1.greater(&_ic_q1_1).implies(&solution.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1)).and(&solution.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1))))).booleanValue() {
- _ic_boolean_2 = BBoolean::new(false);
- break;
- }
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).booleanValue() {
+ for _ic_q1_1 in self.interval.clone().iter().cloned() {
+ for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
+ if !(_ic_q2_1.greater(&_ic_q1_1).implies(&solution.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1)).and(&solution.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1))))).booleanValue() {
+ _ic_boolean_2 = BBoolean::new(false);
+ break;
+ }
+ }
}
}
+
+ //quantified_predicate
let mut _ic_boolean_3 = BBoolean::new(true);
- for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
- if !(solution.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
- _ic_boolean_3 = BBoolean::new(false);
- break;
- }
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).and(&_ic_boolean_2).booleanValue() {
+ for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
+ if !(solution.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
+ _ic_boolean_3 = BBoolean::new(false);
+ break;
+ }
+ }
}
+
if (self.allFields.elementOf(&solution).and(&solution.domain().equal(&self.interval)).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).and(&_ic_boolean_2).and(&_ic_boolean_3)).booleanValue() {
self.queens = solution.clone().clone();
} else {
@@ -111,41 +125,56 @@ impl QueensWithEvents_4 {
//transition
if !is_caching || self._tr_cache_Solve.is_none() {
let mut _ic_set_4: BSet<BRelation<BInteger, BInteger>> = BSet::new(vec![]);
+ //transition, parameters, no condidtion
for _ic_solution_1 in self.allFields.clone().iter().cloned() {
+ //quantified_predicate
let mut _ic_boolean_5 = BBoolean::new(true);
- for _ic_x_1 in self.interval.clone().iter().cloned() {
- for _ic_y_1 in self.interval.clone().iter().cloned() {
- let mut _ic_boolean_4 = BBoolean::new(true);
- for _ic_z_1 in self.interval.clone().iter().cloned() {
- if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
- _ic_boolean_4 = BBoolean::new(false);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).booleanValue() {
+ for _ic_x_1 in self.interval.clone().iter().cloned() {
+ for _ic_y_1 in self.interval.clone().iter().cloned() {
+ //quantified_predicate
+ let mut _ic_boolean_4 = BBoolean::new(true);
+ for _ic_z_1 in self.interval.clone().iter().cloned() {
+ if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
+ _ic_boolean_4 = BBoolean::new(false);
+ break;
+ }
+
+ }
+
+ if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_4)).booleanValue() {
+ _ic_boolean_5 = BBoolean::new(false);
break;
}
}
- if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_4)).booleanValue() {
- _ic_boolean_5 = BBoolean::new(false);
- break;
- }
+ }
+ }
+ //quantified_predicate
+ let mut _ic_boolean_6 = BBoolean::new(true);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).booleanValue() {
+ for _ic_q1_1 in self.interval.clone().iter().cloned() {
+ for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
+ if !(_ic_q2_1.greater(&_ic_q1_1).implies(&_ic_solution_1.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1)).and(&_ic_solution_1.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1))))).booleanValue() {
+ _ic_boolean_6 = BBoolean::new(false);
+ break;
+ }
+ }
}
- }let mut _ic_boolean_6 = BBoolean::new(true);
- for _ic_q1_1 in self.interval.clone().iter().cloned() {
- for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
- if !(_ic_q2_1.greater(&_ic_q1_1).implies(&_ic_solution_1.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1)).and(&_ic_solution_1.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1))))).booleanValue() {
- _ic_boolean_6 = BBoolean::new(false);
+ }
+ //quantified_predicate
+ let mut _ic_boolean_7 = BBoolean::new(true);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).and(&_ic_boolean_6).booleanValue() {
+ for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
+ if !(_ic_solution_1.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
+ _ic_boolean_7 = BBoolean::new(false);
break;
}
}
- }let mut _ic_boolean_7 = BBoolean::new(true);
- for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
- if !(_ic_solution_1.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
- _ic_boolean_7 = BBoolean::new(false);
- break;
- }
-
}
+
if (_ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).and(&_ic_boolean_6).and(&_ic_boolean_7)).booleanValue() {
_ic_set_4 = _ic_set_4._union(&BSet::new(vec![_ic_solution_1]));
}
@@ -168,7 +197,7 @@ impl QueensWithEvents_4 {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_Solve" => {self._tr_Solve(false);},
+ "_tr_Solve" => {self._tr_Solve(false);},
_ => {},
}
}
@@ -270,10 +299,10 @@ impl QueensWithEvents_4 {
fn next(collection_m: Arc<Mutex<LinkedList<QueensWithEvents_4>>>, mc_type: MC_TYPE) -> QueensWithEvents_4 {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -317,11 +346,11 @@ impl QueensWithEvents_4 {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -356,7 +385,7 @@ impl QueensWithEvents_4 {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<QueensWithEvents_4>::new()));
@@ -412,14 +441,14 @@ impl QueensWithEvents_4 {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/QueensWithEvents_8.rs b/benchmarks/model_checking/Rust/QueensWithEvents_8.rs
index 707064e62..a4855dd4d 100644
--- a/benchmarks/model_checking/Rust/QueensWithEvents_8.rs
+++ b/benchmarks/model_checking/Rust/QueensWithEvents_8.rs
@@ -64,42 +64,56 @@ impl QueensWithEvents_8 {
}
pub fn Solve(&mut self, mut solution: BRelation<BInteger, BInteger>) -> () {
+ //quantified_predicate
let mut _ic_boolean_1 = BBoolean::new(true);
- for _ic_x_1 in self.interval.clone().iter().cloned() {
- for _ic_y_1 in self.interval.clone().iter().cloned() {
- let mut _ic_boolean_0 = BBoolean::new(true);
- for _ic_z_1 in self.interval.clone().iter().cloned() {
- if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
- _ic_boolean_0 = BBoolean::new(false);
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).booleanValue() {
+ for _ic_x_1 in self.interval.clone().iter().cloned() {
+ for _ic_y_1 in self.interval.clone().iter().cloned() {
+ //quantified_predicate
+ let mut _ic_boolean_0 = BBoolean::new(true);
+ for _ic_z_1 in self.interval.clone().iter().cloned() {
+ if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
+ _ic_boolean_0 = BBoolean::new(false);
+ break;
+ }
+
+ }
+
+ if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_0)).booleanValue() {
+ _ic_boolean_1 = BBoolean::new(false);
break;
}
}
- if !(solution.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_0)).booleanValue() {
- _ic_boolean_1 = BBoolean::new(false);
- break;
- }
-
}
}
+
+ //quantified_predicate
let mut _ic_boolean_2 = BBoolean::new(true);
- for _ic_q1_1 in self.interval.clone().iter().cloned() {
- for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
- if !(_ic_q2_1.greater(&_ic_q1_1).implies(&solution.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1)).and(&solution.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1))))).booleanValue() {
- _ic_boolean_2 = BBoolean::new(false);
- break;
- }
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).booleanValue() {
+ for _ic_q1_1 in self.interval.clone().iter().cloned() {
+ for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
+ if !(_ic_q2_1.greater(&_ic_q1_1).implies(&solution.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1)).and(&solution.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&solution.functionCall(&_ic_q2_1))))).booleanValue() {
+ _ic_boolean_2 = BBoolean::new(false);
+ break;
+ }
+ }
}
}
+
+ //quantified_predicate
let mut _ic_boolean_3 = BBoolean::new(true);
- for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
- if !(solution.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
- _ic_boolean_3 = BBoolean::new(false);
- break;
- }
+ if solution.domain().equal(&self.interval).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).and(&_ic_boolean_2).booleanValue() {
+ for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
+ if !(solution.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
+ _ic_boolean_3 = BBoolean::new(false);
+ break;
+ }
+ }
}
+
if (self.allFields.elementOf(&solution).and(&solution.domain().equal(&self.interval)).and(&solution.range().equal(&self.interval)).and(&_ic_boolean_1).and(&_ic_boolean_2).and(&_ic_boolean_3)).booleanValue() {
self.queens = solution.clone().clone();
} else {
@@ -111,41 +125,56 @@ impl QueensWithEvents_8 {
//transition
if !is_caching || self._tr_cache_Solve.is_none() {
let mut _ic_set_4: BSet<BRelation<BInteger, BInteger>> = BSet::new(vec![]);
+ //transition, parameters, no condidtion
for _ic_solution_1 in self.allFields.clone().iter().cloned() {
+ //quantified_predicate
let mut _ic_boolean_5 = BBoolean::new(true);
- for _ic_x_1 in self.interval.clone().iter().cloned() {
- for _ic_y_1 in self.interval.clone().iter().cloned() {
- let mut _ic_boolean_4 = BBoolean::new(true);
- for _ic_z_1 in self.interval.clone().iter().cloned() {
- if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
- _ic_boolean_4 = BBoolean::new(false);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).booleanValue() {
+ for _ic_x_1 in self.interval.clone().iter().cloned() {
+ for _ic_y_1 in self.interval.clone().iter().cloned() {
+ //quantified_predicate
+ let mut _ic_boolean_4 = BBoolean::new(true);
+ for _ic_z_1 in self.interval.clone().iter().cloned() {
+ if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_z_1)).implies(&_ic_y_1.equal(&_ic_z_1))).booleanValue() {
+ _ic_boolean_4 = BBoolean::new(false);
+ break;
+ }
+
+ }
+
+ if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_4)).booleanValue() {
+ _ic_boolean_5 = BBoolean::new(false);
break;
}
}
- if !(_ic_solution_1.elementOf(&BTuple::from_refs(&_ic_x_1, &_ic_y_1)).implies(&_ic_boolean_4)).booleanValue() {
- _ic_boolean_5 = BBoolean::new(false);
- break;
- }
+ }
+ }
+ //quantified_predicate
+ let mut _ic_boolean_6 = BBoolean::new(true);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).booleanValue() {
+ for _ic_q1_1 in self.interval.clone().iter().cloned() {
+ for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
+ if !(_ic_q2_1.greater(&_ic_q1_1).implies(&_ic_solution_1.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1)).and(&_ic_solution_1.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1))))).booleanValue() {
+ _ic_boolean_6 = BBoolean::new(false);
+ break;
+ }
+ }
}
- }let mut _ic_boolean_6 = BBoolean::new(true);
- for _ic_q1_1 in self.interval.clone().iter().cloned() {
- for _ic_q2_1 in self.interval.difference(&BSet::new(vec![BInteger::new(1)])).clone().iter().cloned() {
- if !(_ic_q2_1.greater(&_ic_q1_1).implies(&_ic_solution_1.functionCall(&_ic_q1_1).plus(&_ic_q2_1).minus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1)).and(&_ic_solution_1.functionCall(&_ic_q1_1).minus(&_ic_q2_1).plus(&_ic_q1_1).unequal(&_ic_solution_1.functionCall(&_ic_q2_1))))).booleanValue() {
- _ic_boolean_6 = BBoolean::new(false);
+ }
+ //quantified_predicate
+ let mut _ic_boolean_7 = BBoolean::new(true);
+ if _ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).and(&_ic_boolean_6).booleanValue() {
+ for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
+ if !(_ic_solution_1.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
+ _ic_boolean_7 = BBoolean::new(false);
break;
}
}
- }let mut _ic_boolean_7 = BBoolean::new(true);
- for _ic_x_1 in self.queens.domain().clone().iter().cloned() {
- if !(_ic_solution_1.functionCall(&_ic_x_1).equal(&self.queens.functionCall(&_ic_x_1))).booleanValue() {
- _ic_boolean_7 = BBoolean::new(false);
- break;
- }
-
}
+
if (_ic_solution_1.domain().equal(&self.interval).and(&_ic_solution_1.range().equal(&self.interval)).and(&_ic_boolean_5).and(&_ic_boolean_6).and(&_ic_boolean_7)).booleanValue() {
_ic_set_4 = _ic_set_4._union(&BSet::new(vec![_ic_solution_1]));
}
@@ -168,7 +197,7 @@ impl QueensWithEvents_8 {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_Solve" => {self._tr_Solve(false);},
+ "_tr_Solve" => {self._tr_Solve(false);},
_ => {},
}
}
@@ -270,10 +299,10 @@ impl QueensWithEvents_8 {
fn next(collection_m: Arc<Mutex<LinkedList<QueensWithEvents_8>>>, mc_type: MC_TYPE) -> QueensWithEvents_8 {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -317,11 +346,11 @@ impl QueensWithEvents_8 {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -356,7 +385,7 @@ impl QueensWithEvents_8 {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<QueensWithEvents_8>::new()));
@@ -412,14 +441,14 @@ impl QueensWithEvents_8 {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
index 6d25a7a9c..f0674fe69 100644
--- a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
+++ b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
@@ -23,14 +23,14 @@ pub enum MC_TYPE { BFS, DFS, MIXED }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum BLOCKS {
- A,
- B,
- C,
- D,
- E,
- F,
- G,
- H,
+ A,
+ B,
+ C,
+ D,
+ E,
+ F,
+ G,
+ H,
I
}
impl BLOCKS {
@@ -43,29 +43,29 @@ impl Default for BLOCKS {
}
impl fmt::Display for BLOCKS {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- BLOCKS::A => write!(f, "A"),
- BLOCKS::B => write!(f, "B"),
- BLOCKS::C => write!(f, "C"),
- BLOCKS::D => write!(f, "D"),
- BLOCKS::E => write!(f, "E"),
- BLOCKS::F => write!(f, "F"),
- BLOCKS::G => write!(f, "G"),
- BLOCKS::H => write!(f, "H"),
- BLOCKS::I => write!(f, "I"),
- }
+ match *self {
+ BLOCKS::A => write!(f, "A"),
+ BLOCKS::B => write!(f, "B"),
+ BLOCKS::C => write!(f, "C"),
+ BLOCKS::D => write!(f, "D"),
+ BLOCKS::E => write!(f, "E"),
+ BLOCKS::F => write!(f, "F"),
+ BLOCKS::G => write!(f, "G"),
+ BLOCKS::H => write!(f, "H"),
+ BLOCKS::I => write!(f, "I"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ROUTES {
- R1,
- R2,
- R3,
- R4,
- R5,
- R6,
- R7,
+ R1,
+ R2,
+ R3,
+ R4,
+ R5,
+ R6,
+ R7,
R8
}
impl ROUTES {
@@ -78,16 +78,16 @@ impl Default for ROUTES {
}
impl fmt::Display for ROUTES {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- ROUTES::R1 => write!(f, "R1"),
- ROUTES::R2 => write!(f, "R2"),
- ROUTES::R3 => write!(f, "R3"),
- ROUTES::R4 => write!(f, "R4"),
- ROUTES::R5 => write!(f, "R5"),
- ROUTES::R6 => write!(f, "R6"),
- ROUTES::R7 => write!(f, "R7"),
- ROUTES::R8 => write!(f, "R8"),
- }
+ match *self {
+ ROUTES::R1 => write!(f, "R1"),
+ ROUTES::R2 => write!(f, "R2"),
+ ROUTES::R3 => write!(f, "R3"),
+ ROUTES::R4 => write!(f, "R4"),
+ ROUTES::R5 => write!(f, "R5"),
+ ROUTES::R6 => write!(f, "R6"),
+ ROUTES::R7 => write!(f, "R7"),
+ ROUTES::R8 => write!(f, "R8"),
+ }
}
}
@@ -545,14 +545,14 @@ impl Train1_Lukas_POR_v3 {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_route_reservation" => {self._tr_route_reservation(false);},
- "_tr_route_freeing" => {self._tr_route_freeing(false);},
- "_tr_FRONT_MOVE_1" => {self._tr_FRONT_MOVE_1(false);},
- "_tr_FRONT_MOVE_2" => {self._tr_FRONT_MOVE_2(false);},
- "_tr_BACK_MOVE_1" => {self._tr_BACK_MOVE_1(false);},
- "_tr_BACK_MOVE_2" => {self._tr_BACK_MOVE_2(false);},
- "_tr_point_positionning" => {self._tr_point_positionning(false);},
- "_tr_route_formation" => {self._tr_route_formation(false);},
+ "_tr_route_reservation" => {self._tr_route_reservation(false);},
+ "_tr_route_freeing" => {self._tr_route_freeing(false);},
+ "_tr_FRONT_MOVE_1" => {self._tr_FRONT_MOVE_1(false);},
+ "_tr_FRONT_MOVE_2" => {self._tr_FRONT_MOVE_2(false);},
+ "_tr_BACK_MOVE_1" => {self._tr_BACK_MOVE_1(false);},
+ "_tr_BACK_MOVE_2" => {self._tr_BACK_MOVE_2(false);},
+ "_tr_point_positionning" => {self._tr_point_positionning(false);},
+ "_tr_route_formation" => {self._tr_route_formation(false);},
_ => {},
}
}
@@ -1007,10 +1007,10 @@ impl Train1_Lukas_POR_v3 {
fn next(collection_m: Arc<Mutex<LinkedList<Train1_Lukas_POR_v3>>>, mc_type: MC_TYPE) -> Train1_Lukas_POR_v3 {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -1082,11 +1082,11 @@ impl Train1_Lukas_POR_v3 {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -1121,7 +1121,7 @@ impl Train1_Lukas_POR_v3 {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() || !machine._check_inv_7() || !machine._check_inv_8() || !machine._check_inv_9() || !machine._check_inv_10() || !machine._check_inv_11() || !machine._check_inv_12() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<Train1_Lukas_POR_v3>::new()));
@@ -1205,14 +1205,14 @@ impl Train1_Lukas_POR_v3 {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
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 a1556c8b6..9460794f2 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
@@ -23,19 +23,19 @@ pub enum MC_TYPE { BFS, DFS, MIXED }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum BLOCKS {
- A,
- B,
- C,
- D,
- E,
- F,
- G,
- H,
- I,
- J,
- K,
- L,
- M,
+ A,
+ B,
+ C,
+ D,
+ E,
+ F,
+ G,
+ H,
+ I,
+ J,
+ K,
+ L,
+ M,
N
}
impl BLOCKS {
@@ -48,36 +48,36 @@ impl Default for BLOCKS {
}
impl fmt::Display for BLOCKS {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- BLOCKS::A => write!(f, "A"),
- BLOCKS::B => write!(f, "B"),
- BLOCKS::C => write!(f, "C"),
- BLOCKS::D => write!(f, "D"),
- BLOCKS::E => write!(f, "E"),
- BLOCKS::F => write!(f, "F"),
- BLOCKS::G => write!(f, "G"),
- BLOCKS::H => write!(f, "H"),
- BLOCKS::I => write!(f, "I"),
- BLOCKS::J => write!(f, "J"),
- BLOCKS::K => write!(f, "K"),
- BLOCKS::L => write!(f, "L"),
- BLOCKS::M => write!(f, "M"),
- BLOCKS::N => write!(f, "N"),
- }
+ match *self {
+ BLOCKS::A => write!(f, "A"),
+ BLOCKS::B => write!(f, "B"),
+ BLOCKS::C => write!(f, "C"),
+ BLOCKS::D => write!(f, "D"),
+ BLOCKS::E => write!(f, "E"),
+ BLOCKS::F => write!(f, "F"),
+ BLOCKS::G => write!(f, "G"),
+ BLOCKS::H => write!(f, "H"),
+ BLOCKS::I => write!(f, "I"),
+ BLOCKS::J => write!(f, "J"),
+ BLOCKS::K => write!(f, "K"),
+ BLOCKS::L => write!(f, "L"),
+ BLOCKS::M => write!(f, "M"),
+ BLOCKS::N => write!(f, "N"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ROUTES {
- R1,
- R2,
- R3,
- R4,
- R5,
- R6,
- R7,
- R8,
- R9,
+ R1,
+ R2,
+ R3,
+ R4,
+ R5,
+ R6,
+ R7,
+ R8,
+ R9,
R10
}
impl ROUTES {
@@ -90,18 +90,18 @@ impl Default for ROUTES {
}
impl fmt::Display for ROUTES {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- ROUTES::R1 => write!(f, "R1"),
- ROUTES::R2 => write!(f, "R2"),
- ROUTES::R3 => write!(f, "R3"),
- ROUTES::R4 => write!(f, "R4"),
- ROUTES::R5 => write!(f, "R5"),
- ROUTES::R6 => write!(f, "R6"),
- ROUTES::R7 => write!(f, "R7"),
- ROUTES::R8 => write!(f, "R8"),
- ROUTES::R9 => write!(f, "R9"),
- ROUTES::R10 => write!(f, "R10"),
- }
+ match *self {
+ ROUTES::R1 => write!(f, "R1"),
+ ROUTES::R2 => write!(f, "R2"),
+ ROUTES::R3 => write!(f, "R3"),
+ ROUTES::R4 => write!(f, "R4"),
+ ROUTES::R5 => write!(f, "R5"),
+ ROUTES::R6 => write!(f, "R6"),
+ ROUTES::R7 => write!(f, "R7"),
+ ROUTES::R8 => write!(f, "R8"),
+ ROUTES::R9 => write!(f, "R9"),
+ ROUTES::R10 => write!(f, "R10"),
+ }
}
}
@@ -568,14 +568,14 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_route_reservation" => {self._tr_route_reservation(false);},
- "_tr_route_freeing" => {self._tr_route_freeing(false);},
- "_tr_FRONT_MOVE_1" => {self._tr_FRONT_MOVE_1(false);},
- "_tr_FRONT_MOVE_2" => {self._tr_FRONT_MOVE_2(false);},
- "_tr_BACK_MOVE_1" => {self._tr_BACK_MOVE_1(false);},
- "_tr_BACK_MOVE_2" => {self._tr_BACK_MOVE_2(false);},
- "_tr_point_positionning" => {self._tr_point_positionning(false);},
- "_tr_route_formation" => {self._tr_route_formation(false);},
+ "_tr_route_reservation" => {self._tr_route_reservation(false);},
+ "_tr_route_freeing" => {self._tr_route_freeing(false);},
+ "_tr_FRONT_MOVE_1" => {self._tr_FRONT_MOVE_1(false);},
+ "_tr_FRONT_MOVE_2" => {self._tr_FRONT_MOVE_2(false);},
+ "_tr_BACK_MOVE_1" => {self._tr_BACK_MOVE_1(false);},
+ "_tr_BACK_MOVE_2" => {self._tr_BACK_MOVE_2(false);},
+ "_tr_point_positionning" => {self._tr_point_positionning(false);},
+ "_tr_route_formation" => {self._tr_route_formation(false);},
_ => {},
}
}
@@ -1030,10 +1030,10 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
fn next(collection_m: Arc<Mutex<LinkedList<Train_1_beebook_deterministic_MC_POR_v2>>>, mc_type: MC_TYPE) -> Train_1_beebook_deterministic_MC_POR_v2 {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -1105,11 +1105,11 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -1144,7 +1144,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() || !machine._check_inv_7() || !machine._check_inv_8() || !machine._check_inv_9() || !machine._check_inv_10() || !machine._check_inv_11() || !machine._check_inv_12() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<Train_1_beebook_deterministic_MC_POR_v2>::new()));
@@ -1228,14 +1228,14 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/benchmarks/model_checking/Rust/nota_v2.rs b/benchmarks/model_checking/Rust/nota_v2.rs
index 77355571f..326000b96 100644
--- a/benchmarks/model_checking/Rust/nota_v2.rs
+++ b/benchmarks/model_checking/Rust/nota_v2.rs
@@ -1,4 +1,4 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments, unused ) ]
use std::env;
use std::sync::atomic::{AtomicI32, AtomicI64, AtomicBool, Ordering};
use std::sync::{Arc, Mutex};
diff --git a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
index 9d56d0a11..0b8c31bc2 100644
--- a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
+++ b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
@@ -207,10 +207,10 @@ impl sort_m2_data1000_MC {
//if caching is enabled globally, this will just prefill those, if caching is
for trans in to_invalidate.iter() {
match *trans {
- "_tr_progress" => {self._tr_progress(false);},
- "_tr_prog1" => {self._tr_prog1(false);},
- "_tr_prog2" => {self._tr_prog2(false);},
- "_tr_final_evt" => {self._tr_final_evt(false);},
+ "_tr_progress" => {self._tr_progress(false);},
+ "_tr_prog1" => {self._tr_prog1(false);},
+ "_tr_prog2" => {self._tr_prog2(false);},
+ "_tr_final_evt" => {self._tr_final_evt(false);},
_ => {},
}
}
@@ -437,10 +437,10 @@ impl sort_m2_data1000_MC {
fn next(collection_m: Arc<Mutex<LinkedList<sort_m2_data1000_MC>>>, mc_type: MC_TYPE) -> sort_m2_data1000_MC {
let mut collection = collection_m.lock().unwrap();
return match mc_type {
- MC_TYPE::BFS => collection.pop_front().unwrap(),
- MC_TYPE::DFS => collection.pop_back().unwrap(),
- MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
- };
+ MC_TYPE::BFS => collection.pop_front().unwrap(),
+ MC_TYPE::DFS => collection.pop_back().unwrap(),
+ MC_TYPE::MIXED => if collection.len() % 2 == 0 { collection.pop_front().unwrap() } else { collection.pop_back().unwrap() }
+ };
}
fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
@@ -496,11 +496,11 @@ impl sort_m2_data1000_MC {
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));
- next_states.iter().for_each(|next_state| {
- if !states.contains(next_state) {
+ next_states.iter().cloned().for_each(|next_state| {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection_m.lock().unwrap().push_back(next_state.clone());
+ collection_m.lock().unwrap().push_back(next_state);
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
@@ -535,7 +535,7 @@ impl sort_m2_data1000_MC {
let possible_queue_changes_b = Arc::new(AtomicI32::new(0));
if !machine._check_inv_1() || !machine._check_inv_2() || !machine._check_inv_3() || !machine._check_inv_4() || !machine._check_inv_5() || !machine._check_inv_6() {
- invariant_violated_b.store(true, Ordering::Release);
+ invariant_violated_b.store(true, Ordering::Release);
}
let states_m = Arc::new(Mutex::new(HashSet::<sort_m2_data1000_MC>::new()));
@@ -603,14 +603,14 @@ impl sort_m2_data1000_MC {
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));
//println!("Thread {:?} executing", thread::current().id());
- next_states.iter().for_each(|next_state| {
+ next_states.iter().cloned().for_each(|next_state| {
{
let mut states = states_m2.lock().unwrap();
let mut collection = collection_m2.lock().unwrap();
- if !states.contains(next_state) {
+ if !states.contains(&next_state) {
let cnum_states = number_states.fetch_add(1, Ordering::AcqRel) + 1;
states.insert(next_state.clone());
- collection.push_back(next_state.clone());
+ collection.push_back(next_state);
//println!("Thread {:?}: states in collection {}", thread::current().id(), collection.len());
if cnum_states % 50000 == 0 {
println!("VISITED STATES: {}", cnum_states);
diff --git a/btypes_primitives/src/main/rust/btypes/src/bboolean.rs b/btypes_primitives/src/main/rust/btypes/src/bboolean.rs
index 3601f95c1..c38368610 100644
--- a/btypes_primitives/src/main/rust/btypes/src/bboolean.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/bboolean.rs
@@ -2,6 +2,17 @@ use std::hash::Hash;
use crate::bobject::BObject;
use std::fmt;
+pub trait IntoBool {
+ #![allow(non_snake_case)]
+ fn booleanValue(&self) -> bool;
+}
+
+impl IntoBool for bool {
+ fn booleanValue(&self) -> bool {
+ return *self;
+ }
+}
+
#[derive(Default, Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct BBoolean {
val: bool,
@@ -15,6 +26,12 @@ impl fmt::Display for BBoolean {
impl BObject for BBoolean {}
+impl IntoBool for BBoolean {
+ fn booleanValue(&self) -> bool {
+ return self.val;
+ }
+}
+
impl BBoolean {
#![allow(non_snake_case, dead_code)]
@@ -24,10 +41,6 @@ impl BBoolean {
}
}
- pub fn booleanValue(&self) -> bool {
- return self.val;
- }
-
pub fn or(&self, other: &BBoolean) -> BBoolean {
return BBoolean::new(self.val || other.val);
}
diff --git a/btypes_primitives/src/main/rust/btypes/src/bset.rs b/btypes_primitives/src/main/rust/btypes/src/bset.rs
index b84f2270f..042bf72d7 100644
--- a/btypes_primitives/src/main/rust/btypes/src/bset.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/bset.rs
@@ -1,6 +1,6 @@
#![ allow( dead_code, non_snake_case) ]
-use crate::bboolean::BBoolean;
+use crate::bboolean::{IntoBool, BBoolean};
use crate::binteger::{BInt, BInteger};
use crate::bstring::BString;
use crate::bobject::BObject;
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 5b709897e..9f6a0f91b 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -19,6 +19,7 @@ use derivative::Derivative;
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bboolean::IntoBool;
<imports; separator="\n">
<includedMachines; separator="\n">
@@ -533,11 +534,11 @@ binary(arg1,operator,arg2) ::= <<
>>
or(arg1, arg2) ::= <<
-<arg1>.or(&<arg2>)
+<arg1>.booleanValue() || <arg2>.booleanValue()
>>
and(arg1, arg2) ::= <<
-<arg1>.and(&<arg2>)
+<arg1>.booleanValue() && <arg2>.booleanValue()
>>
implies(arg1, arg2) ::= <<
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
index c823f401a..c9191f8df 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
@@ -36,7 +36,7 @@ public class TestMCBenchmarks extends TestRS {
@Test
public void testQueens8_MC() throws Exception {
- testRSMC("QueensWithEvents_8");
+ testRSMC("QueensWithEvents_8", false);
}
@Test
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Cruise_finite1_deterministic_MC.out b/src/test/resources/de/hhu/stups/codegenerator/Cruise_finite1_deterministic_MC.out
index db32d6ca1..929e4a6ff 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Cruise_finite1_deterministic_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/Cruise_finite1_deterministic_MC.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
Number of States: 1360
-Number of Transitions: 26149
\ No newline at end of file
+Number of Transitions: 26148
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Lift_MC_Large.out b/src/test/resources/de/hhu/stups/codegenerator/Lift_MC_Large.out
index 1c06af5a7..efe827164 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Lift_MC_Large.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/Lift_MC_Large.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
Number of States: 1000001
-Number of Transitions: 2000001
\ No newline at end of file
+Number of Transitions: 2000000
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8_MC.out b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8_MC.out
new file mode 100644
index 000000000..5c1ec216a
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 4
+Number of Transitions: 6
\ No newline at end of file
--
GitLab