From 8dfe81845925369569be394245e3c45a6aa37dd6 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Thu, 11 May 2023 14:34:35 +0200
Subject: [PATCH] updated rust modelchecking benchmarks
---
benchmarks/model_checking/Rust/CAN_BUS_tlc.rs | 57 +++--
.../Rust/Cruise_finite1_deterministic_MC.rs | 150 +++++++------
.../model_checking/Rust/LandingGear_R6.rs | 162 ++++++++------
.../model_checking/Rust/Lift_MC_Large.rs | 34 ++-
.../Rust/Train1_Lukas_POR_v3.rs | 120 ++++++-----
...Train_1_beebook_deterministic_MC_POR_v2.rs | 119 ++++++-----
benchmarks/model_checking/Rust/nota_v2.rs | 198 ++++++++++--------
7 files changed, 492 insertions(+), 348 deletions(-)
diff --git a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
index 66dffc50d..9fd5453a4 100644
--- a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
+++ b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::binteger::BInteger;
@@ -420,7 +421,7 @@ impl CAN_BUS_tlc {
pub fn T2ReleaseBus(&mut self, mut ppriority: BInteger) -> () {
//pre_assert
let mut _ld_BUSwrite = self.BUSwrite.clone();
- self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority])).clone().clone();
+ self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority.clone()])).clone().clone();
self.T2_state = T2state::T2_WAIT;
}
@@ -485,7 +486,7 @@ impl CAN_BUS_tlc {
pub fn T3ReleaseBus(&mut self, mut ppriority: BInteger) -> () {
//pre_assert
let mut _ld_BUSwrite = self.BUSwrite.clone();
- self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority])).clone().clone();
+ self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority.clone()])).clone().clone();
self.T3_state = T3state::T3_RELEASE;
}
@@ -534,6 +535,7 @@ impl CAN_BUS_tlc {
let mut _ic_set_1: BSet<BInteger> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_p_1 in BSet::<BInteger>::interval(&BInteger::new(1).negative(), &BInteger::new(3)).clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.T1_state.equal(&T1state::T1_CALC)).booleanValue() {
_ic_set_1 = _ic_set_1._union(&BSet::new(vec![_ic_p_1]));
}
@@ -555,6 +557,7 @@ impl CAN_BUS_tlc {
let mut _ic_ppriority_1 = BInteger::new(3);
{
let mut _ic_pv_1 = self.T1_writevalue;
+ //parameter_combination_predicate
if (self.T1_state.equal(&T1state::T1_SEND)).booleanValue() {
_ic_set_2 = _ic_set_2._union(&BSet::new(vec![BTuple::from_refs(&_ic_ppriority_1, &_ic_pv_1)]));
}
@@ -575,6 +578,7 @@ impl CAN_BUS_tlc {
//transition, parameters, no condidtion
{
let mut _ic_pt_1 = BInteger::new(2);
+ //parameter_combination_predicate
if (self.T1_state.equal(&T1state::T1_WAIT)).booleanValue() {
_ic_set_3 = _ic_set_3._union(&BSet::new(vec![_ic_pt_1]));
}
@@ -607,6 +611,7 @@ impl CAN_BUS_tlc {
let mut _ic_ppriority_1 = self.BUSpriority;
{
let mut _ic_pv_1 = self.BUSvalue;
+ //parameter_combination_predicate
if (self.T2_state.equal(&T2state::T2_RCV)).booleanValue() {
_ic_set_5 = _ic_set_5._union(&BSet::new(vec![BTuple::from_refs(&_ic_ppriority_1, &_ic_pv_1)]));
}
@@ -649,6 +654,7 @@ impl CAN_BUS_tlc {
//transition, parameters, no condidtion
{
let mut _ic_ppriority_1 = self.T2_readpriority;
+ //parameter_combination_predicate
if ((self.BUSwrite.domain().elementOf(&_ic_ppriority_1) && self.T2_state.equal(&T2state::T2_RELEASE))).booleanValue() {
_ic_set_8 = _ic_set_8._union(&BSet::new(vec![_ic_ppriority_1]));
}
@@ -681,6 +687,7 @@ impl CAN_BUS_tlc {
let mut _ic_ppriority_1 = BInteger::new(5);
{
let mut _ic_pv_1 = self.T2_writevalue;
+ //parameter_combination_predicate
if (self.T2_state.equal(&T2state::T2_SEND)).booleanValue() {
_ic_set_10 = _ic_set_10._union(&BSet::new(vec![BTuple::from_refs(&_ic_ppriority_1, &_ic_pv_1)]));
}
@@ -701,6 +708,7 @@ impl CAN_BUS_tlc {
//transition, parameters, no condidtion
{
let mut _ic_pt_1 = BInteger::new(3);
+ //parameter_combination_predicate
if (self.T2_state.equal(&T2state::T2_WAIT)).booleanValue() {
_ic_set_11 = _ic_set_11._union(&BSet::new(vec![_ic_pt_1]));
}
@@ -744,6 +752,7 @@ impl CAN_BUS_tlc {
let mut _ic_ppriority_1 = BInteger::new(4);
{
let mut _ic_pv_1 = BInteger::new(0);
+ //parameter_combination_predicate
if (self.T3_state.equal(&T3state::T3_WRITE)).booleanValue() {
_ic_set_14 = _ic_set_14._union(&BSet::new(vec![BTuple::from_refs(&_ic_ppriority_1, &_ic_pv_1)]));
}
@@ -766,6 +775,7 @@ impl CAN_BUS_tlc {
let mut _ic_ppriority_1 = self.BUSpriority;
{
let mut _ic_pv_1 = self.BUSvalue;
+ //parameter_combination_predicate
if (self.T3_state.equal(&T3state::T3_READ)).booleanValue() {
_ic_set_15 = _ic_set_15._union(&BSet::new(vec![BTuple::from_refs(&_ic_ppriority_1, &_ic_pv_1)]));
}
@@ -797,6 +807,7 @@ impl CAN_BUS_tlc {
//transition, parameters, no condidtion
{
let mut _ic_ppriority_1 = BInteger::new(4);
+ //parameter_combination_predicate
if ((self.T3_readpriority.equal(&BInteger::new(5)) && self.T3_state.equal(&T3state::T3_PROC))).booleanValue() {
_ic_set_17 = _ic_set_17._union(&BSet::new(vec![_ic_ppriority_1]));
}
@@ -838,6 +849,7 @@ impl CAN_BUS_tlc {
//transition, parameters, no condidtion
{
let mut _ic_pmax_1 = self.BUSwrite.domain()._max();
+ //parameter_combination_predicate
if (((self.T1_timer.greater(&BInteger::new(0)) && self.T2_timer.greater(&BInteger::new(0))) && (self.T3_enabled.equal(&BBoolean::new(true)) || self.T3_evaluated.equal(&BBoolean::new(true))))).booleanValue() {
_ic_set_20 = _ic_set_20._union(&BSet::new(vec![_ic_pmax_1]));
}
@@ -857,12 +869,12 @@ impl CAN_BUS_tlc {
pub fn _check_inv_2(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.T3_evaluated).booleanValue();
+ return (*butils::BOOL).elementOf(&self.T3_evaluated).booleanValue();
}
pub fn _check_inv_3(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.T3_enabled).booleanValue();
+ return (*butils::BOOL).elementOf(&self.T3_enabled).booleanValue();
}
pub fn _check_inv_4(&self) -> bool {
@@ -937,12 +949,12 @@ impl CAN_BUS_tlc {
pub fn _check_inv_18(&self) -> bool {
//invariant
- return self.BUSwrite.checkDomain(&self.NATSET).and(&self.BUSwrite.checkRangeInteger()).and(&self.BUSwrite.isFunction()).and(&self.BUSwrite.isPartial(&self.NATSET)).booleanValue();
+ return self.NATSET.check_domain_of(&self.BUSwrite).and(&self.BUSwrite.checkRangeInteger()).and(&self.BUSwrite.isFunction()).and(&self.NATSET.check_partial_of(&self.BUSwrite)).booleanValue();
}
pub fn _check_inv_19(&self) -> bool {
//invariant
- return self.BUSwrite.unequal(&BRelation::new(vec![])).booleanValue();
+ return self.BUSwrite.unequal(&BRelation::<BInteger, BInteger>::new(vec![])).booleanValue();
}
pub fn _check_inv_20(&self) -> bool {
@@ -1235,8 +1247,6 @@ impl CAN_BUS_tlc {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &CAN_BUS_tlc, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -1499,7 +1509,7 @@ impl CAN_BUS_tlc {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = CAN_BUS_tlc::new();
let mut all_states = HashSet::<CAN_BUS_tlc>::new();
@@ -1517,11 +1527,11 @@ impl CAN_BUS_tlc {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -1539,7 +1549,7 @@ impl CAN_BUS_tlc {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = CAN_BUS_tlc::new();
@@ -1568,14 +1578,14 @@ impl CAN_BUS_tlc {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -1610,7 +1620,7 @@ impl CAN_BUS_tlc {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -1623,9 +1633,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- CAN_BUS_tlc::model_check_single_threaded(mc_type, is_caching);
+ CAN_BUS_tlc::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- CAN_BUS_tlc::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ CAN_BUS_tlc::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
diff --git a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
index 54815c760..eab2b5014 100644
--- a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
+++ b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::binteger::BInteger;
@@ -323,7 +324,7 @@ impl Cruise_finite1_deterministic_MC {
}
pub fn CCInitialisationDelayFinished(&mut self) -> () {
- if ((((((self.CCInitialisationInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true))))).booleanValue() {
+ if ((((((self.CCInitialisationInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue()))).booleanValue() {
self.CCInitialisationInProgress = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -331,7 +332,7 @@ impl Cruise_finite1_deterministic_MC {
}
pub fn CruiseSpeedChangeFinished(&mut self, mut vtks: BBoolean, mut vtktg: BBoolean) -> () {
- if ((((((((((((butils::BOOL.elementOf(&vtks) && butils::BOOL.elementOf(&vtktg)) && (((vtks.equal(&BBoolean::new(true)) || vtktg.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&vtktg.equal(&BBoolean::new(false)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&vtks.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtks.equal(&BBoolean::new(true)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&vtktg.equal(&BBoolean::new(false)))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((((((((((((*butils::BOOL).elementOf(&vtks) && (*butils::BOOL).elementOf(&vtktg)) && (((vtks.equal(&BBoolean::new(true)) || vtktg.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| vtks.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| vtktg.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| vtktg.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| vtks.equal(&BBoolean::new(true)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).booleanValue() {
self.VehicleTryKeepTimeGap = vtktg;
self.VehicleTryKeepSpeed = vtks;
} else {
@@ -340,7 +341,7 @@ impl Cruise_finite1_deterministic_MC {
}
pub fn CruiseSpeedChangeDelayFinished(&mut self) -> () {
- if ((((((self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true))))).booleanValue() {
+ if ((((((self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue()))).booleanValue() {
self.CruiseSpeedChangeInProgress = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -527,7 +528,7 @@ impl Cruise_finite1_deterministic_MC {
}
pub fn VehicleManageObstacle(&mut self, mut vtks: BBoolean, mut vtktg: BBoolean) -> () {
- if ((((((((((((butils::BOOL.elementOf(&vtks) && butils::BOOL.elementOf(&vtktg)) && (((vtks.equal(&BBoolean::new(true)) || vtktg.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&vtktg.equal(&BBoolean::new(false)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&vtks.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtks.equal(&BBoolean::new(true)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&vtktg.equal(&BBoolean::new(false)))) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((((((((((((*butils::BOOL).elementOf(&vtks) && (*butils::BOOL).elementOf(&vtktg)) && (((vtks.equal(&BBoolean::new(true)) || vtktg.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| vtks.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| vtktg.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| vtktg.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| vtks.equal(&BBoolean::new(true)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| vtktg.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)))).booleanValue() {
self.VehicleTryKeepTimeGap = vtktg;
self.VehicleTryKeepSpeed = vtks;
} else {
@@ -536,7 +537,7 @@ impl Cruise_finite1_deterministic_MC {
}
pub fn ObstacleBecomesOld(&mut self) -> () {
- if ((((((self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true))))).booleanValue() {
+ if ((((((self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue()))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -570,8 +571,9 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_SetCruiseSpeed.is_none() {
let mut _ic_set_2: BSet<BTuple<BBoolean, BBoolean>> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_vcks_1 in butils::BOOL.clone().iter().cloned() {
- for _ic_csam_1 in butils::BOOL.clone().iter().cloned() {
+ for _ic_vcks_1 in (*butils::BOOL).clone().iter().cloned() {
+ for _ic_csam_1 in (*butils::BOOL).clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.CruiseAllowed.equal(&BBoolean::new(true))).booleanValue() {
_ic_set_2 = _ic_set_2._union(&BSet::new(vec![BTuple::from_refs(&_ic_vcks_1, &_ic_csam_1)]));
}
@@ -590,9 +592,10 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_CCInitialisationFinished.is_none() {
let mut _ic_set_3: BSet<BTuple<BBoolean, BBoolean>> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_vtks_1 in butils::BOOL.clone().iter().cloned() {
- for _ic_vtktg_1 in butils::BOOL.clone().iter().cloned() {
- if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.CCInitialisationInProgress.equal(&BBoolean::new(true)))).booleanValue() {
+ for _ic_vtks_1 in (*butils::BOOL).clone().iter().cloned() {
+ for _ic_vtktg_1 in (*butils::BOOL).clone().iter().cloned() {
+ //parameter_combination_predicate
+ if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.CCInitialisationInProgress.equal(&BBoolean::new(true)))).booleanValue() {
_ic_set_3 = _ic_set_3._union(&BSet::new(vec![BTuple::from_refs(&_ic_vtks_1, &_ic_vtktg_1)]));
}
@@ -608,7 +611,7 @@ impl Cruise_finite1_deterministic_MC {
pub fn _tr_CCInitialisationDelayFinished(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_CCInitialisationDelayFinished.is_none() {
- let mut __tmp__val__ = (((((self.CCInitialisationInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).booleanValue();
+ let mut __tmp__val__ = (((((self.CCInitialisationInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())).booleanValue();
self._tr_cache_CCInitialisationDelayFinished = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -621,9 +624,10 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_CruiseSpeedChangeFinished.is_none() {
let mut _ic_set_5: BSet<BTuple<BBoolean, BBoolean>> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_vtks_1 in butils::BOOL.clone().iter().cloned() {
- for _ic_vtktg_1 in butils::BOOL.clone().iter().cloned() {
- if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).booleanValue() {
+ for _ic_vtks_1 in (*butils::BOOL).clone().iter().cloned() {
+ for _ic_vtktg_1 in (*butils::BOOL).clone().iter().cloned() {
+ //parameter_combination_predicate
+ if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).booleanValue() {
_ic_set_5 = _ic_set_5._union(&BSet::new(vec![BTuple::from_refs(&_ic_vtks_1, &_ic_vtktg_1)]));
}
@@ -639,7 +643,7 @@ impl Cruise_finite1_deterministic_MC {
pub fn _tr_CruiseSpeedChangeDelayFinished(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_CruiseSpeedChangeDelayFinished.is_none() {
- let mut __tmp__val__ = (((((self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).booleanValue();
+ let mut __tmp__val__ = (((((self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())).booleanValue();
self._tr_cache_CruiseSpeedChangeDelayFinished = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -806,8 +810,9 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_ObstacleAppearsWhenCruiseActive.is_none() {
let mut _ic_set_21: BSet<BTuple<RSset, ODset>> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_ors_1 in self._RSset.difference(&BSet::new(vec![RSset::RSnone])).clone().iter().cloned() {
- for _ic_od_1 in self._ODset.difference(&BSet::new(vec![ODset::ODnone])).clone().iter().cloned() {
+ for _ic_ors_1 in self._RSset.difference(&BSet::new(vec![RSset::RSnone.clone()])).clone().iter().cloned() {
+ for _ic_od_1 in self._ODset.difference(&BSet::new(vec![ODset::ODnone.clone()])).clone().iter().cloned() {
+ //parameter_combination_predicate
if ((self.ObstaclePresent.equal(&BBoolean::new(false)) && self.CruiseActive.equal(&BBoolean::new(true)))).booleanValue() {
_ic_set_21 = _ic_set_21._union(&BSet::new(vec![BTuple::from_refs(&_ic_ors_1, &_ic_od_1)]));
}
@@ -826,7 +831,8 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_ObstacleAppearsWhenCruiseInactive.is_none() {
let mut _ic_set_22: BSet<RSset> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_ors_1 in self._RSset.difference(&BSet::new(vec![RSset::RSnone])).clone().iter().cloned() {
+ for _ic_ors_1 in self._RSset.difference(&BSet::new(vec![RSset::RSnone.clone()])).clone().iter().cloned() {
+ //parameter_combination_predicate
if ((self.ObstaclePresent.equal(&BBoolean::new(false)) && self.CruiseActive.equal(&BBoolean::new(false)))).booleanValue() {
_ic_set_22 = _ic_set_22._union(&BSet::new(vec![_ic_ors_1]));
}
@@ -855,9 +861,10 @@ impl Cruise_finite1_deterministic_MC {
if !is_caching || self._tr_cache_VehicleManageObstacle.is_none() {
let mut _ic_set_24: BSet<BTuple<BBoolean, BBoolean>> = BSet::new(vec![]);
//transition, parameters, no condidtion
- for _ic_vtks_1 in butils::BOOL.clone().iter().cloned() {
- for _ic_vtktg_1 in butils::BOOL.clone().iter().cloned() {
- if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtktg_1.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&_ic_vtks_1.equal(&BBoolean::new(true)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&_ic_vtktg_1.equal(&BBoolean::new(false)))) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)))).booleanValue() {
+ for _ic_vtks_1 in (*butils::BOOL).clone().iter().cloned() {
+ for _ic_vtktg_1 in (*butils::BOOL).clone().iter().cloned() {
+ //parameter_combination_predicate
+ if (((((((((((((_ic_vtks_1.equal(&BBoolean::new(true)) || _ic_vtktg_1.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true))) && self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtktg_1.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| _ic_vtks_1.equal(&BBoolean::new(true)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| _ic_vtktg_1.equal(&BBoolean::new(false)).booleanValue())) && self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)))).booleanValue() {
_ic_set_24 = _ic_set_24._union(&BSet::new(vec![BTuple::from_refs(&_ic_vtks_1, &_ic_vtktg_1)]));
}
@@ -873,7 +880,7 @@ impl Cruise_finite1_deterministic_MC {
pub fn _tr_ObstacleBecomesOld(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_ObstacleBecomesOld.is_none() {
- let mut __tmp__val__ = (((((self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).booleanValue();
+ let mut __tmp__val__ = (((((self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)) && (((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || self.CCInitialisationInProgress.equal(&BBoolean::new(true))) || self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))) && self.ObstacleDistance.equal(&ODset::ODnone).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue())) && (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue())).booleanValue();
self._tr_cache_ObstacleBecomesOld = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -883,42 +890,42 @@ impl Cruise_finite1_deterministic_MC {
pub fn _check_inv_1(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.CruiseAllowed).booleanValue();
+ return (*butils::BOOL).elementOf(&self.CruiseAllowed).booleanValue();
}
pub fn _check_inv_2(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.CruiseActive).booleanValue();
+ return (*butils::BOOL).elementOf(&self.CruiseActive).booleanValue();
}
pub fn _check_inv_3(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.VehicleAtCruiseSpeed).booleanValue();
+ return (*butils::BOOL).elementOf(&self.VehicleAtCruiseSpeed).booleanValue();
}
pub fn _check_inv_4(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.VehicleCanKeepSpeed).booleanValue();
+ return (*butils::BOOL).elementOf(&self.VehicleCanKeepSpeed).booleanValue();
}
pub fn _check_inv_5(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.VehicleTryKeepSpeed).booleanValue();
+ return (*butils::BOOL).elementOf(&self.VehicleTryKeepSpeed).booleanValue();
}
pub fn _check_inv_6(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.SpeedAboveMax).booleanValue();
+ return (*butils::BOOL).elementOf(&self.SpeedAboveMax).booleanValue();
}
pub fn _check_inv_7(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.VehicleTryKeepTimeGap).booleanValue();
+ return (*butils::BOOL).elementOf(&self.VehicleTryKeepTimeGap).booleanValue();
}
pub fn _check_inv_8(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.CruiseSpeedAtMax).booleanValue();
+ return (*butils::BOOL).elementOf(&self.CruiseSpeedAtMax).booleanValue();
}
pub fn _check_inv_9(&self) -> bool {
@@ -933,7 +940,7 @@ impl Cruise_finite1_deterministic_MC {
pub fn _check_inv_11(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.ObstaclePresent).booleanValue();
+ return (*butils::BOOL).elementOf(&self.ObstaclePresent).booleanValue();
}
pub fn _check_inv_12(&self) -> bool {
@@ -948,32 +955,32 @@ impl Cruise_finite1_deterministic_MC {
pub fn _check_inv_14(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.ObstacleStatusJustChanged).booleanValue();
+ return (*butils::BOOL).elementOf(&self.ObstacleStatusJustChanged).booleanValue();
}
pub fn _check_inv_15(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.CCInitialisationInProgress).booleanValue();
+ return (*butils::BOOL).elementOf(&self.CCInitialisationInProgress).booleanValue();
}
pub fn _check_inv_16(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.CruiseSpeedChangeInProgress).booleanValue();
+ return (*butils::BOOL).elementOf(&self.CruiseSpeedChangeInProgress).booleanValue();
}
pub fn _check_inv_17(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_18(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.VehicleCanKeepSpeed.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.VehicleCanKeepSpeed.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_19(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_20(&self) -> bool {
@@ -983,42 +990,42 @@ impl Cruise_finite1_deterministic_MC {
pub fn _check_inv_21(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_22(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.CruiseSpeedAtMax.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.CruiseSpeedAtMax.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_23(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.ObstacleDistance.equal(&ODset::ODnone)).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.ObstacleDistance.equal(&ODset::ODnone).booleanValue()).booleanValue();
}
pub fn _check_inv_24(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_25(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.CCInitialisationInProgress.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_26(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(false)).implies(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(false)).implies(|| self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_27(&self) -> bool {
//invariant
- return self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false))).booleanValue();
+ return self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_28(&self) -> bool {
//invariant
- return self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&self.ObstacleDistance.equal(&ODset::ODnone)).booleanValue();
+ return self.ObstaclePresent.equal(&BBoolean::new(false)).implies(|| self.ObstacleDistance.equal(&ODset::ODnone).booleanValue()).booleanValue();
}
pub fn _check_inv_29(&self) -> bool {
@@ -1028,52 +1035,52 @@ impl Cruise_finite1_deterministic_MC {
pub fn _check_inv_30(&self) -> bool {
//invariant
- return (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false))).booleanValue();
+ return (self.ObstacleRelativeSpeed.equal(&RSset::RSequal) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_31(&self) -> bool {
//invariant
- return (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false))).booleanValue();
+ return (self.ObstacleRelativeSpeed.equal(&RSset::RSneg) && self.ObstacleDistance.equal(&ODset::ODnone)).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_32(&self) -> bool {
//invariant
- return (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false))).booleanValue();
+ return (self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_33(&self) -> bool {
//invariant
- return self.CruiseAllowed.equal(&BBoolean::new(false)).implies(&self.CruiseActive.equal(&BBoolean::new(false))).booleanValue();
+ return self.CruiseAllowed.equal(&BBoolean::new(false)).implies(|| self.CruiseActive.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_34(&self) -> bool {
//invariant
- return self.SpeedAboveMax.equal(&BBoolean::new(true)).implies(&self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false))).booleanValue();
+ return self.SpeedAboveMax.equal(&BBoolean::new(true)).implies(|| self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false)).booleanValue()).booleanValue();
}
pub fn _check_inv_35(&self) -> bool {
//invariant
- return self.CruiseActive.equal(&BBoolean::new(true)).implies(&((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).not())).booleanValue();
+ return self.CruiseActive.equal(&BBoolean::new(true)).implies(|| ((self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)) || self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))) || ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).not()).booleanValue()).booleanValue();
}
pub fn _check_inv_36(&self) -> bool {
//invariant
- return ((self.ObstacleDistance.equal(&ODset::ODnone) && self.CruiseActive.equal(&BBoolean::new(true))) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true))).booleanValue();
+ return ((self.ObstacleDistance.equal(&ODset::ODnone) && self.CruiseActive.equal(&BBoolean::new(true))) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue()).booleanValue();
}
pub fn _check_inv_37(&self) -> bool {
//invariant
- return ((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))).booleanValue();
+ return ((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue()).booleanValue();
}
pub fn _check_inv_38(&self) -> bool {
//invariant
- return (self.ObstacleDistance.equal(&ODset::ODveryclose) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))).booleanValue();
+ return (self.ObstacleDistance.equal(&ODset::ODveryclose) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(|| self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)).booleanValue()).booleanValue();
}
pub fn _check_inv_39(&self) -> bool {
//invariant
- return (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CruiseActive.equal(&BBoolean::new(true))) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true))).booleanValue();
+ return (((self.ObstacleRelativeSpeed.equal(&RSset::RSpos) && self.ObstacleDistance.unequal(&ODset::ODveryclose)) && self.CruiseActive.equal(&BBoolean::new(true))) && ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false)))).implies(|| self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).booleanValue()).booleanValue();
}
fn invalidate_caches(&mut self, to_invalidate: Vec<&'static str>) {
@@ -1391,8 +1398,6 @@ impl Cruise_finite1_deterministic_MC {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &Cruise_finite1_deterministic_MC, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -1808,7 +1813,7 @@ impl Cruise_finite1_deterministic_MC {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = Cruise_finite1_deterministic_MC::new();
let mut all_states = HashSet::<Cruise_finite1_deterministic_MC>::new();
@@ -1826,11 +1831,11 @@ impl Cruise_finite1_deterministic_MC {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -1848,7 +1853,7 @@ impl Cruise_finite1_deterministic_MC {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = Cruise_finite1_deterministic_MC::new();
@@ -1877,14 +1882,14 @@ impl Cruise_finite1_deterministic_MC {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -1919,7 +1924,7 @@ impl Cruise_finite1_deterministic_MC {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -1932,9 +1937,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- Cruise_finite1_deterministic_MC::model_check_single_threaded(mc_type, is_caching);
+ Cruise_finite1_deterministic_MC::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- Cruise_finite1_deterministic_MC::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ Cruise_finite1_deterministic_MC::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
diff --git a/benchmarks/model_checking/Rust/LandingGear_R6.rs b/benchmarks/model_checking/Rust/LandingGear_R6.rs
index 016ef4e20..2732e15a2 100644
--- a/benchmarks/model_checking/Rust/LandingGear_R6.rs
+++ b/benchmarks/model_checking/Rust/LandingGear_R6.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::brelation::BRelation;
@@ -329,8 +330,8 @@ impl LandingGear_R6 {
self._SWITCH_STATE = BSet::new(vec![SWITCH_STATE::switch_open, SWITCH_STATE::switch_closed]);
self._PLANE_STATE = BSet::new(vec![PLANE_STATE::ground, PLANE_STATE::flight]);
self._VALVE_STATE = BSet::new(vec![VALVE_STATE::valve_open, VALVE_STATE::valve_closed]);
- self.gears = BRelation::cartesianProduct(&self._POSITION, &BSet::new(vec![GEAR_STATE::extended])).clone().clone();
- self.doors = BRelation::cartesianProduct(&self._POSITION, &BSet::new(vec![DOOR_STATE::closed])).clone().clone();
+ self.gears = BRelation::cartesianProduct(&self._POSITION, &BSet::new(vec![GEAR_STATE::extended.clone()])).clone().clone();
+ self.doors = BRelation::cartesianProduct(&self._POSITION, &BSet::new(vec![DOOR_STATE::closed.clone()])).clone().clone();
self.handle = HANDLE_STATE::down;
self.valve_extend_gear = VALVE_STATE::valve_closed;
self.valve_retract_gear = VALVE_STATE::valve_closed;
@@ -530,7 +531,7 @@ impl LandingGear_R6 {
}
pub fn con_stimulate_open_door_valve(&mut self) -> () {
- if ((((self.open_EV.equal(&BBoolean::new(false)) && self.close_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])).not()) || ((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])).not()) && (self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.shock_absorber.equal(&PLANE_STATE::ground)).not()))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if ((((self.open_EV.equal(&BBoolean::new(false)) && self.close_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])).not()) || ((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])).not()) && (self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.shock_absorber.equal(&PLANE_STATE::ground)).not()))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.open_EV = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -538,7 +539,7 @@ impl LandingGear_R6 {
}
pub fn con_stop_stimulate_open_door_valve(&mut self) -> () {
- if (((((self.open_EV.equal(&BBoolean::new(true)) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((((self.open_EV.equal(&BBoolean::new(true)) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.open_EV = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -546,7 +547,7 @@ impl LandingGear_R6 {
}
pub fn con_stimulate_close_door_valve(&mut self) -> () {
- if (((((((self.close_EV.equal(&BBoolean::new(false)) && self.open_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) || (self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed])).not()) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((((((self.close_EV.equal(&BBoolean::new(false)) && self.open_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()])).not()) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.close_EV = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -554,7 +555,7 @@ impl LandingGear_R6 {
}
pub fn con_stop_stimulate_close_door_valve(&mut self) -> () {
- if (((self.close_EV.equal(&BBoolean::new(true)) && (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((self.close_EV.equal(&BBoolean::new(true)) && (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.close_EV = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -562,7 +563,7 @@ impl LandingGear_R6 {
}
pub fn con_stimulate_retract_gear_valve(&mut self) -> () {
- if ((((((((self.retract_EV.equal(&BBoolean::new(false)) && self.extend_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])).not()) && self.shock_absorber.equal(&PLANE_STATE::flight)) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if ((((((((self.retract_EV.equal(&BBoolean::new(false)) && self.extend_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])).not()) && self.shock_absorber.equal(&PLANE_STATE::flight)) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.retract_EV = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -570,7 +571,7 @@ impl LandingGear_R6 {
}
pub fn con_stop_stimulate_retract_gear_valve(&mut self) -> () {
- if (((self.retract_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::down) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((self.retract_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::down) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.retract_EV = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -578,7 +579,7 @@ impl LandingGear_R6 {
}
pub fn con_stimulate_extend_gear_valve(&mut self) -> () {
- if (((((((self.extend_EV.equal(&BBoolean::new(false)) && self.retract_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])).not()) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((((((self.extend_EV.equal(&BBoolean::new(false)) && self.retract_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])).not()) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.extend_EV = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -586,7 +587,7 @@ impl LandingGear_R6 {
}
pub fn con_stop_stimulate_extend_gear_valve(&mut self) -> () {
- if (((self.extend_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::up) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
+ if (((self.extend_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::up) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) && self.general_EV.equal(&BBoolean::new(true)))).booleanValue() {
self.extend_EV = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -594,7 +595,7 @@ impl LandingGear_R6 {
}
pub fn env_start_retracting_first(&mut self, mut gr: POSITION) -> () {
- if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::extended)) && self.valve_retract_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::gear_moving]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::extended)) && self.valve_retract_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::gear_moving.clone()]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
let mut _ld_gears = self.gears.clone();
self.gears = _ld_gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::gear_moving)])).clone().clone();
self.gear = GEAR_STATE::gear_moving;
@@ -604,7 +605,7 @@ impl LandingGear_R6 {
}
pub fn env_retract_gear_skip(&mut self, mut gr: POSITION) -> () {
- if ((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).unequal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ if ((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).unequal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
self.gears = self.gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::retracted)])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -612,7 +613,7 @@ impl LandingGear_R6 {
}
pub fn env_retract_gear_last(&mut self, mut gr: POSITION) -> () {
- if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).equal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
let mut _ld_gears = self.gears.clone();
self.gears = _ld_gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::retracted)])).clone().clone();
self.gear = GEAR_STATE::retracted;
@@ -622,7 +623,7 @@ impl LandingGear_R6 {
}
pub fn env_start_extending(&mut self, mut gr: POSITION) -> () {
- if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::retracted)) && self.valve_extend_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::gear_moving, GEAR_STATE::retracted]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.functionCall(&gr).equal(&GEAR_STATE::retracted)) && self.valve_extend_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::gear_moving.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
let mut _ld_gears = self.gears.clone();
self.gears = _ld_gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::gear_moving)])).clone().clone();
self.gear = GEAR_STATE::gear_moving;
@@ -632,7 +633,7 @@ impl LandingGear_R6 {
}
pub fn env_extend_gear_last(&mut self, mut gr: POSITION) -> () {
- if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ if ((((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
let mut _ld_gears = self.gears.clone();
self.gears = _ld_gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::extended)])).clone().clone();
self.gear = GEAR_STATE::extended;
@@ -642,7 +643,7 @@ impl LandingGear_R6 {
}
pub fn env_extend_gear_skip(&mut self, mut gr: POSITION) -> () {
- if ((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).unequal(&BSet::new(vec![GEAR_STATE::extended]))) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ if ((((((self.gears.domain().elementOf(&gr) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).unequal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.gears.functionCall(&gr).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
self.gears = self.gears._override(&BRelation::new(vec![BTuple::from_refs(&gr, &GEAR_STATE::extended)])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -650,7 +651,7 @@ impl LandingGear_R6 {
}
pub fn env_start_open_door(&mut self, mut gr: POSITION) -> () {
- if ((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::closed)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::closed, DOOR_STATE::door_moving]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
+ if ((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::closed)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::closed.clone(), DOOR_STATE::door_moving.clone()]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
let mut _ld_doors = self.doors.clone();
self.doors = _ld_doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::door_moving)])).clone().clone();
self.door = DOOR_STATE::door_moving;
@@ -660,7 +661,7 @@ impl LandingGear_R6 {
}
pub fn env_open_door_last(&mut self, mut gr: POSITION) -> () {
- if (((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).equal(&BSet::new(vec![DOOR_STATE::open]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
+ if (((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
let mut _ld_doors = self.doors.clone();
self.doors = _ld_doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::open)])).clone().clone();
self.door = DOOR_STATE::open;
@@ -670,7 +671,7 @@ impl LandingGear_R6 {
}
pub fn env_open_door_skip(&mut self, mut gr: POSITION) -> () {
- if ((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).unequal(&BSet::new(vec![DOOR_STATE::open]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ if ((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).unequal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
self.doors = self.doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::open)])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -678,7 +679,7 @@ impl LandingGear_R6 {
}
pub fn env_start_close_door(&mut self, mut gr: POSITION) -> () {
- if (((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::open)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::door_moving, DOOR_STATE::open]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::retracted]).elementOf(&self.gear))))).booleanValue() {
+ if (((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::open)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::door_moving.clone(), DOOR_STATE::open.clone()]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear))))).booleanValue() {
let mut _ld_doors = self.doors.clone();
self.doors = _ld_doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::door_moving)])).clone().clone();
self.door = DOOR_STATE::door_moving;
@@ -688,7 +689,7 @@ impl LandingGear_R6 {
}
pub fn env_close_door(&mut self, mut gr: POSITION) -> () {
- if ((((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).equal(&BSet::new(vec![DOOR_STATE::closed]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))).implies(&self.shock_absorber.equal(&PLANE_STATE::ground))) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::retracted]).elementOf(&self.gear))))).booleanValue() {
+ if ((((((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))).implies(|| self.shock_absorber.equal(&PLANE_STATE::ground).booleanValue())) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear))))).booleanValue() {
let mut _ld_doors = self.doors.clone();
self.doors = _ld_doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::closed)])).clone().clone();
self.door = DOOR_STATE::closed;
@@ -698,7 +699,7 @@ impl LandingGear_R6 {
}
pub fn env_close_door_skip(&mut self, mut gr: POSITION) -> () {
- if (((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr]))).unequal(&BSet::new(vec![DOOR_STATE::closed]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))).implies(&self.shock_absorber.equal(&PLANE_STATE::ground))) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ if (((((((((self.gears.domain().elementOf(&gr) && self.doors.functionCall(&gr).equal(&DOOR_STATE::door_moving)) && self.gears.functionCall(&gr).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![gr.clone()]))).unequal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))).implies(|| self.shock_absorber.equal(&PLANE_STATE::ground).booleanValue())) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
self.doors = self.doors._override(&BRelation::new(vec![BTuple::from_refs(&gr, &DOOR_STATE::closed)])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -732,7 +733,7 @@ impl LandingGear_R6 {
}
pub fn con_stop_stimulate_general_valve(&mut self) -> () {
- if (((((((self.general_EV.equal(&BBoolean::new(true)) && self.open_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && (((((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false))) || (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false)))) || (((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false)))))).booleanValue() {
+ if (((((((self.general_EV.equal(&BBoolean::new(true)) && self.open_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && (((((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false))) || (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false)))) || (((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false)))))).booleanValue() {
self.general_EV = BBoolean::new(false);
self.handle_move = BBoolean::new(false);
} else {
@@ -885,7 +886,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stimulate_open_door_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stimulate_open_door_valve.is_none() {
- let mut __tmp__val__ = (((self.open_EV.equal(&BBoolean::new(false)) && self.close_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])).not()) || ((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])).not()) && (self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.shock_absorber.equal(&PLANE_STATE::ground)).not()))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = (((self.open_EV.equal(&BBoolean::new(false)) && self.close_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])).not()) || ((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])).not()) && (self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.shock_absorber.equal(&PLANE_STATE::ground)).not()))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stimulate_open_door_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -896,7 +897,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stop_stimulate_open_door_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stop_stimulate_open_door_valve.is_none() {
- let mut __tmp__val__ = ((((self.open_EV.equal(&BBoolean::new(true)) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((((self.open_EV.equal(&BBoolean::new(true)) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stop_stimulate_open_door_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -907,7 +908,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stimulate_close_door_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stimulate_close_door_valve.is_none() {
- let mut __tmp__val__ = ((((((self.close_EV.equal(&BBoolean::new(false)) && self.open_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) || (self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed])).not()) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((((((self.close_EV.equal(&BBoolean::new(false)) && self.open_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()])).not()) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stimulate_close_door_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -918,7 +919,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stop_stimulate_close_door_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stop_stimulate_close_door_valve.is_none() {
- let mut __tmp__val__ = ((self.close_EV.equal(&BBoolean::new(true)) && (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((self.close_EV.equal(&BBoolean::new(true)) && (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) || ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.shock_absorber.equal(&PLANE_STATE::ground))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stop_stimulate_close_door_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -929,7 +930,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stimulate_retract_gear_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stimulate_retract_gear_valve.is_none() {
- let mut __tmp__val__ = (((((((self.retract_EV.equal(&BBoolean::new(false)) && self.extend_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])).not()) && self.shock_absorber.equal(&PLANE_STATE::flight)) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = (((((((self.retract_EV.equal(&BBoolean::new(false)) && self.extend_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])).not()) && self.shock_absorber.equal(&PLANE_STATE::flight)) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stimulate_retract_gear_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -940,7 +941,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stop_stimulate_retract_gear_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stop_stimulate_retract_gear_valve.is_none() {
- let mut __tmp__val__ = ((self.retract_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::down) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((self.retract_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::down) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stop_stimulate_retract_gear_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -951,7 +952,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stimulate_extend_gear_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stimulate_extend_gear_valve.is_none() {
- let mut __tmp__val__ = ((((((self.extend_EV.equal(&BBoolean::new(false)) && self.retract_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])).not()) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((((((self.extend_EV.equal(&BBoolean::new(false)) && self.retract_EV.equal(&BBoolean::new(false))) && self.open_EV.equal(&BBoolean::new(true))) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])).not()) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stimulate_extend_gear_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -962,7 +963,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stop_stimulate_extend_gear_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stop_stimulate_extend_gear_valve.is_none() {
- let mut __tmp__val__ = ((self.extend_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::up) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ let mut __tmp__val__ = ((self.extend_EV.equal(&BBoolean::new(true)) && (self.handle.equal(&HANDLE_STATE::up) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) && self.general_EV.equal(&BBoolean::new(true))).booleanValue();
self._tr_cache_con_stop_stimulate_extend_gear_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -976,7 +977,8 @@ impl LandingGear_R6 {
let mut _ic_set_18: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::extended)) && self.valve_retract_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::gear_moving]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::extended)) && self.valve_retract_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::gear_moving.clone()]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
_ic_set_18 = _ic_set_18._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -994,7 +996,8 @@ impl LandingGear_R6 {
let mut _ic_set_19: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).unequal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).unequal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
_ic_set_19 = _ic_set_19._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1012,7 +1015,8 @@ impl LandingGear_R6 {
let mut _ic_set_20: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).equal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.handle.equal(&HANDLE_STATE::up)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
_ic_set_20 = _ic_set_20._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1030,7 +1034,8 @@ impl LandingGear_R6 {
let mut _ic_set_21: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::retracted)) && self.valve_extend_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::gear_moving, GEAR_STATE::retracted]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::retracted)) && self.valve_extend_gear.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![GEAR_STATE::gear_moving.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
_ic_set_21 = _ic_set_21._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1048,7 +1053,8 @@ impl LandingGear_R6 {
let mut _ic_set_22: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.gear.equal(&GEAR_STATE::gear_moving)) && self.door.equal(&DOOR_STATE::open))).booleanValue() {
_ic_set_22 = _ic_set_22._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1066,7 +1072,8 @@ impl LandingGear_R6 {
let mut _ic_set_23: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).unequal(&BSet::new(vec![GEAR_STATE::extended]))) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()])) && self.handle.equal(&HANDLE_STATE::down)) && self.gears.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).unequal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.gears.functionCall(&_ic_gr_1).equal(&GEAR_STATE::gear_moving)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
_ic_set_23 = _ic_set_23._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1084,7 +1091,8 @@ impl LandingGear_R6 {
let mut _ic_set_24: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::closed) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::closed, DOOR_STATE::door_moving]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::closed) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::closed.clone(), DOOR_STATE::door_moving.clone()]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
_ic_set_24 = _ic_set_24._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1102,7 +1110,8 @@ impl LandingGear_R6 {
let mut _ic_set_25: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if ((((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).equal(&BSet::new(vec![DOOR_STATE::open]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
+ //parameter_combination_predicate
+ if ((((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).equal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::retracted)) || (self.handle.equal(&HANDLE_STATE::up) && self.gear.equal(&GEAR_STATE::extended))))).booleanValue() {
_ic_set_25 = _ic_set_25._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1120,7 +1129,8 @@ impl LandingGear_R6 {
let mut _ic_set_26: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).unequal(&BSet::new(vec![DOOR_STATE::open]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).unequal(&BSet::new(vec![DOOR_STATE::open.clone()]))) && ((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) || (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_open_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
_ic_set_26 = _ic_set_26._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1138,7 +1148,8 @@ impl LandingGear_R6 {
let mut _ic_set_27: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if ((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::open) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::door_moving, DOOR_STATE::open]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::retracted]).elementOf(&self.gear))))).booleanValue() {
+ //parameter_combination_predicate
+ if ((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::open) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && self.general_valve.equal(&VALVE_STATE::valve_open)) && BSet::new(vec![DOOR_STATE::door_moving.clone(), DOOR_STATE::open.clone()]).elementOf(&self.door)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear))))).booleanValue() {
_ic_set_27 = _ic_set_27._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1156,7 +1167,8 @@ impl LandingGear_R6 {
let mut _ic_set_28: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if (((((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).equal(&BSet::new(vec![DOOR_STATE::closed]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))).implies(&self.shock_absorber.equal(&PLANE_STATE::ground))) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended, GEAR_STATE::retracted]).elementOf(&self.gear))))).booleanValue() {
+ //parameter_combination_predicate
+ if (((((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))).implies(|| self.shock_absorber.equal(&PLANE_STATE::ground).booleanValue())) && self.general_valve.equal(&VALVE_STATE::valve_open)) && self.door.equal(&DOOR_STATE::door_moving)) && self.gear.unequal(&GEAR_STATE::gear_moving)) && ((self.handle.equal(&HANDLE_STATE::down) && self.gear.equal(&GEAR_STATE::extended)) || (self.handle.equal(&HANDLE_STATE::up) && BSet::new(vec![GEAR_STATE::extended.clone(), GEAR_STATE::retracted.clone()]).elementOf(&self.gear))))).booleanValue() {
_ic_set_28 = _ic_set_28._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1174,7 +1186,8 @@ impl LandingGear_R6 {
let mut _ic_set_29: BSet<POSITION> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_gr_1 in self.gears.domain().clone().iter().cloned() {
- if ((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1]))).unequal(&BSet::new(vec![DOOR_STATE::closed]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))).implies(&self.shock_absorber.equal(&PLANE_STATE::ground))) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
+ //parameter_combination_predicate
+ if ((((((((self.doors.functionCall(&_ic_gr_1).equal(&DOOR_STATE::door_moving) && self.gears.functionCall(&_ic_gr_1).unequal(&GEAR_STATE::gear_moving)) && self.gears.range().notElementOf(&GEAR_STATE::gear_moving)) && self.doors.relationImage(&self._POSITION.difference(&BSet::new(vec![_ic_gr_1.clone()]))).unequal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && ((self.handle.equal(&HANDLE_STATE::up) && (self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()])) || self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()])))) || (self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))))) && self.valve_close_door.equal(&VALVE_STATE::valve_open)) && (self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))).implies(|| self.shock_absorber.equal(&PLANE_STATE::ground).booleanValue())) && self.general_valve.equal(&VALVE_STATE::valve_open))).booleanValue() {
_ic_set_29 = _ic_set_29._union(&BSet::new(vec![_ic_gr_1]));
}
@@ -1222,7 +1235,7 @@ impl LandingGear_R6 {
pub fn _tr_con_stop_stimulate_general_valve(&mut self, is_caching: bool) -> bool {
//transition
if !is_caching || self._tr_cache_con_stop_stimulate_general_valve.is_none() {
- let mut __tmp__val__ = ((((((self.general_EV.equal(&BBoolean::new(true)) && self.open_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && (((((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false))) || (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false)))) || (((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))) && self.open_EV.equal(&BBoolean::new(false))))).booleanValue();
+ let mut __tmp__val__ = ((((((self.general_EV.equal(&BBoolean::new(true)) && self.open_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && self.retract_EV.equal(&BBoolean::new(false))) && self.extend_EV.equal(&BBoolean::new(false))) && self.close_EV.equal(&BBoolean::new(false))) && (((((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false))) || (((self.handle.equal(&HANDLE_STATE::down) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false)))) || (((self.handle.equal(&HANDLE_STATE::up) && self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))) && self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))) && self.open_EV.equal(&BBoolean::new(false))))).booleanValue();
self._tr_cache_con_stop_stimulate_general_valve = Option::Some(__tmp__val__);
return __tmp__val__;
} else {
@@ -1281,7 +1294,7 @@ impl LandingGear_R6 {
pub fn _check_inv_2(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.general_EV).booleanValue();
+ return (*butils::BOOL).elementOf(&self.general_EV).booleanValue();
}
pub fn _check_inv_3(&self) -> bool {
@@ -1291,27 +1304,27 @@ impl LandingGear_R6 {
pub fn _check_inv_4(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.handle_move).booleanValue();
+ return (*butils::BOOL).elementOf(&self.handle_move).booleanValue();
}
pub fn _check_inv_5(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.close_EV).booleanValue();
+ return (*butils::BOOL).elementOf(&self.close_EV).booleanValue();
}
pub fn _check_inv_6(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.extend_EV).booleanValue();
+ return (*butils::BOOL).elementOf(&self.extend_EV).booleanValue();
}
pub fn _check_inv_7(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.open_EV).booleanValue();
+ return (*butils::BOOL).elementOf(&self.open_EV).booleanValue();
}
pub fn _check_inv_8(&self) -> bool {
//invariant
- return butils::BOOL.elementOf(&self.retract_EV).booleanValue();
+ return (*butils::BOOL).elementOf(&self.retract_EV).booleanValue();
}
pub fn _check_inv_9(&self) -> bool {
@@ -1356,7 +1369,7 @@ impl LandingGear_R6 {
pub fn _check_inv_17(&self) -> bool {
//invariant
- return (((self.open_EV.equal(&BBoolean::new(true)) || self.close_EV.equal(&BBoolean::new(true))) || self.retract_EV.equal(&BBoolean::new(true))) || self.extend_EV.equal(&BBoolean::new(true))).implies(&self.general_EV.equal(&BBoolean::new(true))).booleanValue();
+ return (((self.open_EV.equal(&BBoolean::new(true)) || self.close_EV.equal(&BBoolean::new(true))) || self.retract_EV.equal(&BBoolean::new(true))) || self.extend_EV.equal(&BBoolean::new(true))).implies(|| self.general_EV.equal(&BBoolean::new(true)).booleanValue()).booleanValue();
}
pub fn _check_inv_18(&self) -> bool {
@@ -1366,37 +1379,37 @@ impl LandingGear_R6 {
pub fn _check_inv_19(&self) -> bool {
//invariant
- return self.gears.checkDomain(&self._POSITION).and(&self.gears.checkRange(&self._GEAR_STATE)).and(&self.gears.isFunction()).and(&self.gears.isTotal(&self._POSITION)).booleanValue();
+ return self._POSITION.check_domain_of(&self.gears).and(&self._GEAR_STATE.check_range_of(&self.gears)).and(&self.gears.isFunction()).and(&self._POSITION.check_total_of(&self.gears)).booleanValue();
}
pub fn _check_inv_20(&self) -> bool {
//invariant
- return self.doors.checkDomain(&self._POSITION).and(&self.doors.checkRange(&self._DOOR_STATE)).and(&self.doors.isFunction()).and(&self.doors.isTotal(&self._POSITION)).booleanValue();
+ return self._POSITION.check_domain_of(&self.doors).and(&self._DOOR_STATE.check_range_of(&self.doors)).and(&self.doors.isFunction()).and(&self._POSITION.check_total_of(&self.doors)).booleanValue();
}
pub fn _check_inv_21(&self) -> bool {
//invariant
- return self.door.equal(&DOOR_STATE::closed).equivalent(&self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed]))).booleanValue();
+ return self.door.equal(&DOOR_STATE::closed).equivalent(&self.doors.range().equal(&BSet::new(vec![DOOR_STATE::closed.clone()]))).booleanValue();
}
pub fn _check_inv_22(&self) -> bool {
//invariant
- return self.door.equal(&DOOR_STATE::open).equivalent(&self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open]))).booleanValue();
+ return self.door.equal(&DOOR_STATE::open).equivalent(&self.doors.range().equal(&BSet::new(vec![DOOR_STATE::open.clone()]))).booleanValue();
}
pub fn _check_inv_23(&self) -> bool {
//invariant
- return self.gear.equal(&GEAR_STATE::extended).equivalent(&self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended]))).booleanValue();
+ return self.gear.equal(&GEAR_STATE::extended).equivalent(&self.gears.range().equal(&BSet::new(vec![GEAR_STATE::extended.clone()]))).booleanValue();
}
pub fn _check_inv_24(&self) -> bool {
//invariant
- return self.gear.equal(&GEAR_STATE::retracted).equivalent(&self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted]))).booleanValue();
+ return self.gear.equal(&GEAR_STATE::retracted).equivalent(&self.gears.range().equal(&BSet::new(vec![GEAR_STATE::retracted.clone()]))).booleanValue();
}
pub fn _check_inv_25(&self) -> bool {
//invariant
- return self.gear.equal(&GEAR_STATE::gear_moving).implies(&self.door.equal(&DOOR_STATE::open)).booleanValue();
+ return self.gear.equal(&GEAR_STATE::gear_moving).implies(|| self.door.equal(&DOOR_STATE::open).booleanValue()).booleanValue();
}
fn invalidate_caches(&mut self, to_invalidate: Vec<&'static str>) {
@@ -1848,8 +1861,6 @@ impl LandingGear_R6 {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &LandingGear_R6, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -2215,7 +2226,7 @@ impl LandingGear_R6 {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = LandingGear_R6::new();
let mut all_states = HashSet::<LandingGear_R6>::new();
@@ -2233,11 +2244,11 @@ impl LandingGear_R6 {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -2255,7 +2266,7 @@ impl LandingGear_R6 {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = LandingGear_R6::new();
@@ -2284,14 +2295,14 @@ impl LandingGear_R6 {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -2326,7 +2337,7 @@ impl LandingGear_R6 {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -2339,9 +2350,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- LandingGear_R6::model_check_single_threaded(mc_type, is_caching);
+ LandingGear_R6::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- LandingGear_R6::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ LandingGear_R6::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
diff --git a/benchmarks/model_checking/Rust/Lift_MC_Large.rs b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
index a6d2852de..b98c9052d 100644
--- a/benchmarks/model_checking/Rust/Lift_MC_Large.rs
+++ b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
@@ -140,8 +141,6 @@ impl Lift_MC_Large {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &Lift_MC_Large, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -202,7 +201,7 @@ impl Lift_MC_Large {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = Lift_MC_Large::new();
let mut all_states = HashSet::<Lift_MC_Large>::new();
@@ -220,11 +219,11 @@ impl Lift_MC_Large {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -242,7 +241,7 @@ impl Lift_MC_Large {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = Lift_MC_Large::new();
@@ -271,14 +270,14 @@ impl Lift_MC_Large {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -313,7 +312,7 @@ impl Lift_MC_Large {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -326,9 +325,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- Lift_MC_Large::model_check_single_threaded(mc_type, is_caching);
+ Lift_MC_Large::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- Lift_MC_Large::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ Lift_MC_Large::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
diff --git a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
index f601ad28f..68408ed45 100644
--- a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
+++ b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::brelation::BRelation;
@@ -155,13 +156,13 @@ impl Train1_Lukas_POR_v3 {
self.fst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::A), BTuple::from_refs(&ROUTES::R2, &BLOCKS::A), BTuple::from_refs(&ROUTES::R3, &BLOCKS::H), BTuple::from_refs(&ROUTES::R4, &BLOCKS::I), BTuple::from_refs(&ROUTES::R5, &BLOCKS::C), BTuple::from_refs(&ROUTES::R6, &BLOCKS::F), BTuple::from_refs(&ROUTES::R7, &BLOCKS::F), BTuple::from_refs(&ROUTES::R8, &BLOCKS::F)]);
self.lst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::C), BTuple::from_refs(&ROUTES::R2, &BLOCKS::F), BTuple::from_refs(&ROUTES::R3, &BLOCKS::F), BTuple::from_refs(&ROUTES::R4, &BLOCKS::F), BTuple::from_refs(&ROUTES::R5, &BLOCKS::A), BTuple::from_refs(&ROUTES::R6, &BLOCKS::A), BTuple::from_refs(&ROUTES::R7, &BLOCKS::H), BTuple::from_refs(&ROUTES::R8, &BLOCKS::I)]);
self.rtbl = BRelation::new(vec![BTuple::from_refs(&BLOCKS::A, &ROUTES::R1), BTuple::from_refs(&BLOCKS::A, &ROUTES::R2), BTuple::from_refs(&BLOCKS::A, &ROUTES::R5), BTuple::from_refs(&BLOCKS::A, &ROUTES::R6), BTuple::from_refs(&BLOCKS::B, &ROUTES::R1), BTuple::from_refs(&BLOCKS::B, &ROUTES::R2), BTuple::from_refs(&BLOCKS::B, &ROUTES::R5), BTuple::from_refs(&BLOCKS::B, &ROUTES::R6), BTuple::from_refs(&BLOCKS::C, &ROUTES::R1), BTuple::from_refs(&BLOCKS::C, &ROUTES::R5), BTuple::from_refs(&BLOCKS::D, &ROUTES::R2), BTuple::from_refs(&BLOCKS::D, &ROUTES::R6), BTuple::from_refs(&BLOCKS::E, &ROUTES::R2), BTuple::from_refs(&BLOCKS::E, &ROUTES::R3), BTuple::from_refs(&BLOCKS::E, &ROUTES::R4), BTuple::from_refs(&BLOCKS::E, &ROUTES::R6), BTuple::from_refs(&BLOCKS::E, &ROUTES::R7), BTuple::from_refs(&BLOCKS::E, &ROUTES::R8), BTuple::from_refs(&BLOCKS::F, &ROUTES::R2), BTuple::from_refs(&BLOCKS::F, &ROUTES::R3), BTuple::from_refs(&BLOCKS::F, &ROUTES::R4), BTuple::from_refs(&BLOCKS::F, &ROUTES::R6), BTuple::from_refs(&BLOCKS::F, &ROUTES::R7), BTuple::from_refs(&BLOCKS::F, &ROUTES::R8), BTuple::from_refs(&BLOCKS::G, &ROUTES::R3), BTuple::from_refs(&BLOCKS::G, &ROUTES::R4), BTuple::from_refs(&BLOCKS::G, &ROUTES::R4), BTuple::from_refs(&BLOCKS::G, &ROUTES::R7), BTuple::from_refs(&BLOCKS::G, &ROUTES::R8), BTuple::from_refs(&BLOCKS::H, &ROUTES::R3), BTuple::from_refs(&BLOCKS::H, &ROUTES::R7), BTuple::from_refs(&BLOCKS::I, &ROUTES::R4), BTuple::from_refs(&BLOCKS::I, &ROUTES::R8)]);
- self.resrt = BSet::new(vec![]).clone().clone();
- self.resbl = BSet::new(vec![]).clone().clone();
- self.rsrtbl = BRelation::new(vec![]).clone().clone();
- self.OCC = BSet::new(vec![]).clone().clone();
- self.TRK = BRelation::new(vec![]).clone().clone();
- self.frm = BSet::new(vec![]).clone().clone();
- self.LBT = BSet::new(vec![]).clone().clone();
+ self.resrt = BSet::<ROUTES>::new(vec![]).clone().clone();
+ self.resbl = BSet::<BLOCKS>::new(vec![]).clone().clone();
+ self.rsrtbl = BRelation::<BLOCKS, ROUTES>::new(vec![]).clone().clone();
+ self.OCC = BSet::<BLOCKS>::new(vec![]).clone().clone();
+ self.TRK = BRelation::<BLOCKS, BLOCKS>::new(vec![]).clone().clone();
+ self.frm = BSet::<ROUTES>::new(vec![]).clone().clone();
+ self.LBT = BSet::<BLOCKS>::new(vec![]).clone().clone();
}
pub fn _get_fst(&self) -> BRelation<ROUTES, BLOCKS> {
@@ -221,9 +222,9 @@ impl Train1_Lukas_POR_v3 {
let mut _ld_resrt = self.resrt.clone();
let mut _ld_rsrtbl = self.rsrtbl.clone();
let mut _ld_resbl = self.resbl.clone();
- self.resrt = _ld_resrt._union(&BSet::new(vec![r])).clone().clone();
- self.rsrtbl = _ld_rsrtbl._union(&self.rtbl.rangeRestriction(&BSet::new(vec![r]))).clone().clone();
- self.resbl = _ld_resbl._union(&self.rtbl.inverse().relationImage(&BSet::new(vec![r]))).clone().clone();
+ self.resrt = _ld_resrt._union(&BSet::new(vec![r.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl._union(&self.rtbl.rangeRestriction(&BSet::new(vec![r.clone()]))).clone().clone();
+ self.resbl = _ld_resbl._union(&self.rtbl.inverse().relationImage(&BSet::new(vec![r.clone()]))).clone().clone();
}
@@ -231,8 +232,8 @@ impl Train1_Lukas_POR_v3 {
//pre_assert
let mut _ld_frm = self.frm.clone();
let mut _ld_resrt = self.resrt.clone();
- self.resrt = _ld_resrt.difference(&BSet::new(vec![r])).clone().clone();
- self.frm = _ld_frm.difference(&BSet::new(vec![r])).clone().clone();
+ self.resrt = _ld_resrt.difference(&BSet::new(vec![r.clone()])).clone().clone();
+ self.frm = _ld_frm.difference(&BSet::new(vec![r.clone()])).clone().clone();
}
@@ -240,14 +241,14 @@ impl Train1_Lukas_POR_v3 {
//pre_assert
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
- self.LBT = _ld_LBT._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
+ self.OCC = _ld_OCC._union(&BSet::new(vec![self.fst.functionCall(&r).clone()])).clone().clone();
+ self.LBT = _ld_LBT._union(&BSet::new(vec![self.fst.functionCall(&r).clone()])).clone().clone();
}
pub fn FRONT_MOVE_2(&mut self, mut b: BLOCKS) -> () {
//pre_assert
- self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
+ self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b).clone()])).clone().clone();
}
@@ -257,10 +258,10 @@ impl Train1_Lukas_POR_v3 {
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
- self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
- self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
- self.LBT = _ld_LBT.difference(&BSet::new(vec![b])).clone().clone();
+ self.OCC = _ld_OCC.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b.clone()])).clone().clone();
+ self.resbl = _ld_resbl.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.LBT = _ld_LBT.difference(&BSet::new(vec![b.clone()])).clone().clone();
}
@@ -270,10 +271,10 @@ impl Train1_Lukas_POR_v3 {
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
- self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
- self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
- self.LBT = _ld_LBT.difference(&BSet::new(vec![b]))._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
+ self.OCC = _ld_OCC.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b.clone()])).clone().clone();
+ self.resbl = _ld_resbl.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.LBT = _ld_LBT.difference(&BSet::new(vec![b.clone()]))._union(&BSet::new(vec![self.TRK.functionCall(&b).clone()])).clone().clone();
}
@@ -285,7 +286,7 @@ impl Train1_Lukas_POR_v3 {
pub fn route_formation(&mut self, mut r: ROUTES) -> () {
//pre_assert
- self.frm = self.frm._union(&BSet::new(vec![r])).clone().clone();
+ self.frm = self.frm._union(&BSet::new(vec![r.clone()])).clone().clone();
}
@@ -295,7 +296,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_0: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self._ROUTES.difference(&self.resrt).clone().iter().cloned() {
- if ((self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])).intersect(&self.resbl).equal(&BSet::new(vec![])) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])).intersect(&self.resbl).equal(&BSet::<BLOCKS>::new(vec![])) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_0 = _ic_set_0._union(&BSet::new(vec![_ic_r_1]));
}
@@ -313,6 +315,7 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_1: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.rsrtbl.range()).clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_1 = _ic_set_1._union(&BSet::new(vec![_ic_r_1]));
}
@@ -329,7 +332,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_2: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.frm.clone().iter().cloned() {
- if (((self.resbl.difference(&self.OCC).elementOf(&self.fst.functionCall(&_ic_r_1)) && _ic_r_1.equal(&self.rsrtbl.functionCall(&self.fst.functionCall(&_ic_r_1)))) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if (((self.resbl.difference(&self.OCC).elementOf(&self.fst.functionCall(&_ic_r_1)) && _ic_r_1.equal(&self.rsrtbl.functionCall(&self.fst.functionCall(&_ic_r_1)))) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_2 = _ic_set_2._union(&BSet::new(vec![_ic_r_1]));
}
@@ -347,7 +351,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_3: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.OCC.intersect(&self.TRK.domain()).clone().iter().cloned() {
- if ((self.OCC.notElementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.OCC.notElementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_3 = _ic_set_3._union(&BSet::new(vec![_ic_b_1]));
}
@@ -365,7 +370,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_4: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.LBT.difference(&self.TRK.domain()).clone().iter().cloned() {
- if (BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
+ //parameter_combination_predicate
+ if (BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
_ic_set_4 = _ic_set_4._union(&BSet::new(vec![_ic_b_1]));
}
@@ -383,7 +389,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_5: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.LBT.intersect(&self.TRK.domain()).clone().iter().cloned() {
- if ((self.OCC.elementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.OCC.elementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_5 = _ic_set_5._union(&BSet::new(vec![_ic_b_1]));
}
@@ -401,7 +408,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_6: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
- if (BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
+ //parameter_combination_predicate
+ if (BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
_ic_set_6 = _ic_set_6._union(&BSet::new(vec![_ic_r_1]));
}
@@ -419,7 +427,8 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_set_7: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
- if ((self.nxt.functionCall(&_ic_r_1).domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]))).equal(&self.TRK.domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])))) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.nxt.functionCall(&_ic_r_1).domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]))).equal(&self.TRK.domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])))) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_7 = _ic_set_7._union(&BSet::new(vec![_ic_r_1]));
}
@@ -433,7 +442,7 @@ impl Train1_Lukas_POR_v3 {
pub fn _check_inv_1(&self) -> bool {
//invariant
- return self.TRK.checkDomain(&self._BLOCKS).and(&self.TRK.checkRange(&self._BLOCKS)).and(&self.TRK.isFunction()).and(&self.TRK.isPartial(&self._BLOCKS)).and(&self.TRK.isInjection()).booleanValue();
+ return self._BLOCKS.check_domain_of(&self.TRK).and(&self._BLOCKS.check_range_of(&self.TRK)).and(&self.TRK.isFunction()).and(&self._BLOCKS.check_partial_of(&self.TRK)).and(&self.TRK.isInjection()).booleanValue();
}
pub fn _check_inv_2(&self) -> bool {
@@ -442,7 +451,7 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_boolean_8 = BBoolean::new(true);
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
{
- let mut _ic_a_1 = BSet::new(vec![_ic_r_1]);
+ let mut _ic_a_1 = BSet::new(vec![_ic_r_1.clone()]);
if !(self.rtbl.rangeRestriction(&_ic_a_1).equal(&self.rsrtbl.rangeRestriction(&_ic_a_1))).booleanValue() {
_ic_boolean_8 = BBoolean::new(false);
break;
@@ -459,7 +468,7 @@ impl Train1_Lukas_POR_v3 {
//quantified_predicate
let mut _ic_boolean_10 = BBoolean::new(true);
for _ic_x_1 in self.TRK.domain().clone().iter().cloned() {
- for _ic_y_1 in self.TRK.relationImage(&BSet::new(vec![_ic_x_1])).clone().iter().cloned() {
+ for _ic_y_1 in self.TRK.relationImage(&BSet::new(vec![_ic_x_1.clone()])).clone().iter().cloned() {
//quantified_predicate
let mut _ic_boolean_9 = BBoolean::new(false);
for _ic_r_1 in self._ROUTES.clone().iter().cloned() {
@@ -487,7 +496,7 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_boolean_11 = BBoolean::new(true);
for _ic_r_1 in self.frm.clone().iter().cloned() {
{
- let mut _ic_a_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]));
+ let mut _ic_a_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]));
if !(self.nxt.functionCall(&_ic_r_1).domainRestriction(&_ic_a_1).equal(&self.TRK.domainRestriction(&_ic_a_1))).booleanValue() {
_ic_boolean_11 = BBoolean::new(false);
break;
@@ -514,7 +523,7 @@ impl Train1_Lukas_POR_v3 {
let mut _ic_c_1 = self.rsrtbl.functionCall(&_ic_b_1);
{
let mut _ic_d_1 = self.nxt.functionCall(&_ic_c_1);
- if !((_ic_d_1.range().elementOf(&_ic_b_1) && _ic_a_1.equal(&_ic_d_1.inverse().functionCall(&_ic_b_1))).implies(&self.rsrtbl.functionCall(&_ic_a_1).unequal(&_ic_c_1))).booleanValue() {
+ if !((_ic_d_1.range().elementOf(&_ic_b_1) && _ic_a_1.equal(&_ic_d_1.inverse().functionCall(&_ic_b_1))).implies(|| self.rsrtbl.functionCall(&_ic_a_1).unequal(&_ic_c_1).booleanValue())).booleanValue() {
_ic_boolean_12 = BBoolean::new(false);
break;
}
@@ -529,7 +538,7 @@ impl Train1_Lukas_POR_v3 {
pub fn _check_inv_7(&self) -> bool {
//invariant
- return self.rsrtbl.checkDomain(&self.resbl).and(&self.rsrtbl.checkRange(&self.resrt)).and(&self.rsrtbl.isFunction()).and(&self.rsrtbl.isTotal(&self.resbl)).booleanValue();
+ return self.resbl.check_domain_of(&self.rsrtbl).and(&self.resrt.check_range_of(&self.rsrtbl)).and(&self.rsrtbl.isFunction()).and(&self.resbl.check_total_of(&self.rsrtbl)).booleanValue();
}
pub fn _check_inv_8(&self) -> bool {
@@ -550,10 +559,10 @@ impl Train1_Lukas_POR_v3 {
{
let mut _ic_a_1 = self.nxt.functionCall(&_ic_r_1);
{
- let mut _ic_b_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]));
+ let mut _ic_b_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]));
{
let mut _ic_c_1 = _ic_b_1.difference(&self.OCC);
- if !(((_ic_a_1.relationImage(&self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])).difference(&_ic_b_1)).intersect(&_ic_c_1).equal(&BSet::new(vec![])) && _ic_a_1.relationImage(&_ic_b_1).subset(&_ic_b_1)) && _ic_a_1.relationImage(&_ic_c_1).subset(&_ic_c_1))).booleanValue() {
+ if !(((_ic_a_1.relationImage(&self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])).difference(&_ic_b_1)).intersect(&_ic_c_1).equal(&BSet::<BLOCKS>::new(vec![])) && _ic_a_1.relationImage(&_ic_b_1).subset(&_ic_b_1)) && _ic_a_1.relationImage(&_ic_c_1).subset(&_ic_c_1))).booleanValue() {
_ic_boolean_13 = BBoolean::new(false);
break;
}
@@ -709,8 +718,6 @@ impl Train1_Lukas_POR_v3 {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &Train1_Lukas_POR_v3, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -865,7 +872,7 @@ impl Train1_Lukas_POR_v3 {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = Train1_Lukas_POR_v3::new();
let mut all_states = HashSet::<Train1_Lukas_POR_v3>::new();
@@ -883,11 +890,11 @@ impl Train1_Lukas_POR_v3 {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -905,7 +912,7 @@ impl Train1_Lukas_POR_v3 {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = Train1_Lukas_POR_v3::new();
@@ -934,14 +941,14 @@ impl Train1_Lukas_POR_v3 {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -976,7 +983,7 @@ impl Train1_Lukas_POR_v3 {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -989,9 +996,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- Train1_Lukas_POR_v3::model_check_single_threaded(mc_type, is_caching);
+ Train1_Lukas_POR_v3::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- Train1_Lukas_POR_v3::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ Train1_Lukas_POR_v3::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
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 a9a40e693..98aba015e 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
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::brelation::BRelation;
@@ -171,6 +172,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_0 = BRelation::<BLOCKS, ROUTES>::new(vec![]);
for _ic_b_1 in self._BLOCKS.clone().iter().cloned() {
for _ic_r_1 in self._ROUTES.clone().iter().cloned() {
+ //set_comprehension_predicate
if ((self.nxt.domain().elementOf(&_ic_r_1) && (self.nxt.functionCall(&_ic_r_1).domain().elementOf(&_ic_b_1) || self.nxt.functionCall(&_ic_r_1).range().elementOf(&_ic_b_1)))).booleanValue() {
_ic_set_0 = _ic_set_0._union(&BRelation::<BLOCKS, ROUTES>::new(vec![BTuple::from_refs(&_ic_b_1, &_ic_r_1)]));
}
@@ -178,13 +180,13 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
}
}
self.rtbl = _ic_set_0;
- self.resrt = BSet::new(vec![]).clone().clone();
- self.resbl = BSet::new(vec![]).clone().clone();
- self.rsrtbl = BRelation::new(vec![]).clone().clone();
- self.OCC = BSet::new(vec![]).clone().clone();
- self.TRK = BRelation::new(vec![]).clone().clone();
- self.frm = BSet::new(vec![]).clone().clone();
- self.LBT = BSet::new(vec![]).clone().clone();
+ self.resrt = BSet::<ROUTES>::new(vec![]).clone().clone();
+ self.resbl = BSet::<BLOCKS>::new(vec![]).clone().clone();
+ self.rsrtbl = BRelation::<BLOCKS, ROUTES>::new(vec![]).clone().clone();
+ self.OCC = BSet::<BLOCKS>::new(vec![]).clone().clone();
+ self.TRK = BRelation::<BLOCKS, BLOCKS>::new(vec![]).clone().clone();
+ self.frm = BSet::<ROUTES>::new(vec![]).clone().clone();
+ self.LBT = BSet::<BLOCKS>::new(vec![]).clone().clone();
}
pub fn _get_fst(&self) -> BRelation<ROUTES, BLOCKS> {
@@ -244,9 +246,9 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ld_resrt = self.resrt.clone();
let mut _ld_rsrtbl = self.rsrtbl.clone();
let mut _ld_resbl = self.resbl.clone();
- self.resrt = _ld_resrt._union(&BSet::new(vec![r])).clone().clone();
- self.rsrtbl = _ld_rsrtbl._union(&self.rtbl.rangeRestriction(&BSet::new(vec![r]))).clone().clone();
- self.resbl = _ld_resbl._union(&self.rtbl.inverse().relationImage(&BSet::new(vec![r]))).clone().clone();
+ self.resrt = _ld_resrt._union(&BSet::new(vec![r.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl._union(&self.rtbl.rangeRestriction(&BSet::new(vec![r.clone()]))).clone().clone();
+ self.resbl = _ld_resbl._union(&self.rtbl.inverse().relationImage(&BSet::new(vec![r.clone()]))).clone().clone();
}
@@ -254,8 +256,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
//pre_assert
let mut _ld_frm = self.frm.clone();
let mut _ld_resrt = self.resrt.clone();
- self.resrt = _ld_resrt.difference(&BSet::new(vec![r])).clone().clone();
- self.frm = _ld_frm.difference(&BSet::new(vec![r])).clone().clone();
+ self.resrt = _ld_resrt.difference(&BSet::new(vec![r.clone()])).clone().clone();
+ self.frm = _ld_frm.difference(&BSet::new(vec![r.clone()])).clone().clone();
}
@@ -263,14 +265,14 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
//pre_assert
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
- self.LBT = _ld_LBT._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
+ self.OCC = _ld_OCC._union(&BSet::new(vec![self.fst.functionCall(&r).clone()])).clone().clone();
+ self.LBT = _ld_LBT._union(&BSet::new(vec![self.fst.functionCall(&r).clone()])).clone().clone();
}
pub fn FRONT_MOVE_2(&mut self, mut b: BLOCKS) -> () {
//pre_assert
- self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
+ self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b).clone()])).clone().clone();
}
@@ -280,10 +282,10 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
- self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
- self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
- self.LBT = _ld_LBT.difference(&BSet::new(vec![b])).clone().clone();
+ self.OCC = _ld_OCC.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b.clone()])).clone().clone();
+ self.resbl = _ld_resbl.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.LBT = _ld_LBT.difference(&BSet::new(vec![b.clone()])).clone().clone();
}
@@ -293,10 +295,10 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
- self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
- self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
- self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
- self.LBT = _ld_LBT.difference(&BSet::new(vec![b]))._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
+ self.OCC = _ld_OCC.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b.clone()])).clone().clone();
+ self.resbl = _ld_resbl.difference(&BSet::new(vec![b.clone()])).clone().clone();
+ self.LBT = _ld_LBT.difference(&BSet::new(vec![b.clone()]))._union(&BSet::new(vec![self.TRK.functionCall(&b).clone()])).clone().clone();
}
@@ -308,7 +310,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
pub fn route_formation(&mut self, mut r: ROUTES) -> () {
//pre_assert
- self.frm = self.frm._union(&BSet::new(vec![r])).clone().clone();
+ self.frm = self.frm._union(&BSet::new(vec![r.clone()])).clone().clone();
}
@@ -318,7 +320,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_1: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self._ROUTES.difference(&self.resrt).clone().iter().cloned() {
- if ((self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])).intersect(&self.resbl).equal(&BSet::new(vec![])) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])).intersect(&self.resbl).equal(&BSet::<BLOCKS>::new(vec![])) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_1 = _ic_set_1._union(&BSet::new(vec![_ic_r_1]));
}
@@ -336,6 +339,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_2: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.rsrtbl.range()).clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_2 = _ic_set_2._union(&BSet::new(vec![_ic_r_1]));
}
@@ -352,7 +356,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_3: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.frm.clone().iter().cloned() {
- if (((self.resbl.difference(&self.OCC).elementOf(&self.fst.functionCall(&_ic_r_1)) && _ic_r_1.equal(&self.rsrtbl.functionCall(&self.fst.functionCall(&_ic_r_1)))) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if (((self.resbl.difference(&self.OCC).elementOf(&self.fst.functionCall(&_ic_r_1)) && _ic_r_1.equal(&self.rsrtbl.functionCall(&self.fst.functionCall(&_ic_r_1)))) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_3 = _ic_set_3._union(&BSet::new(vec![_ic_r_1]));
}
@@ -370,6 +375,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_4: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.OCC.intersect(&self.TRK.domain()).clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.OCC.notElementOf(&self.TRK.functionCall(&_ic_b_1))).booleanValue() {
_ic_set_4 = _ic_set_4._union(&BSet::new(vec![_ic_b_1]));
}
@@ -388,7 +394,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_5: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.LBT.difference(&self.TRK.domain()).clone().iter().cloned() {
- if (BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
+ //parameter_combination_predicate
+ if (BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
_ic_set_5 = _ic_set_5._union(&BSet::new(vec![_ic_b_1]));
}
@@ -406,7 +413,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_6: BSet<BLOCKS> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_b_1 in self.LBT.intersect(&self.TRK.domain()).clone().iter().cloned() {
- if ((self.OCC.elementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.OCC.elementOf(&self.TRK.functionCall(&_ic_b_1)) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_6 = _ic_set_6._union(&BSet::new(vec![_ic_b_1]));
}
@@ -424,7 +432,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_7: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
- if (BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
+ //parameter_combination_predicate
+ if (BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range()))).booleanValue() {
_ic_set_7 = _ic_set_7._union(&BSet::new(vec![_ic_r_1]));
}
@@ -442,7 +451,8 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_set_8: BSet<ROUTES> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
- if ((self.nxt.functionCall(&_ic_r_1).domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]))).equal(&self.TRK.domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])))) && BSet::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.nxt.functionCall(&_ic_r_1).domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]))).equal(&self.TRK.domainRestriction(&self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])))) && BSet::<ROUTES>::new(vec![]).equal(&self.resrt.difference(&self.rsrtbl.range())))).booleanValue() {
_ic_set_8 = _ic_set_8._union(&BSet::new(vec![_ic_r_1]));
}
@@ -456,7 +466,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
pub fn _check_inv_1(&self) -> bool {
//invariant
- return self.TRK.checkDomain(&self._BLOCKS).and(&self.TRK.checkRange(&self._BLOCKS)).and(&self.TRK.isFunction()).and(&self.TRK.isPartial(&self._BLOCKS)).and(&self.TRK.isInjection()).booleanValue();
+ return self._BLOCKS.check_domain_of(&self.TRK).and(&self._BLOCKS.check_range_of(&self.TRK)).and(&self.TRK.isFunction()).and(&self._BLOCKS.check_partial_of(&self.TRK)).and(&self.TRK.isInjection()).booleanValue();
}
pub fn _check_inv_2(&self) -> bool {
@@ -465,7 +475,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_boolean_9 = BBoolean::new(true);
for _ic_r_1 in self.resrt.difference(&self.frm).clone().iter().cloned() {
{
- let mut _ic_a_1 = BSet::new(vec![_ic_r_1]);
+ let mut _ic_a_1 = BSet::new(vec![_ic_r_1.clone()]);
if !(self.rtbl.rangeRestriction(&_ic_a_1).equal(&self.rsrtbl.rangeRestriction(&_ic_a_1))).booleanValue() {
_ic_boolean_9 = BBoolean::new(false);
break;
@@ -482,7 +492,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
//quantified_predicate
let mut _ic_boolean_11 = BBoolean::new(true);
for _ic_x_1 in self.TRK.domain().clone().iter().cloned() {
- for _ic_y_1 in self.TRK.relationImage(&BSet::new(vec![_ic_x_1])).clone().iter().cloned() {
+ for _ic_y_1 in self.TRK.relationImage(&BSet::new(vec![_ic_x_1.clone()])).clone().iter().cloned() {
//quantified_predicate
let mut _ic_boolean_10 = BBoolean::new(false);
for _ic_r_1 in self._ROUTES.clone().iter().cloned() {
@@ -510,7 +520,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_boolean_12 = BBoolean::new(true);
for _ic_r_1 in self.frm.clone().iter().cloned() {
{
- let mut _ic_a_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]));
+ let mut _ic_a_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]));
if !(self.nxt.functionCall(&_ic_r_1).domainRestriction(&_ic_a_1).equal(&self.TRK.domainRestriction(&_ic_a_1))).booleanValue() {
_ic_boolean_12 = BBoolean::new(false);
break;
@@ -537,7 +547,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let mut _ic_c_1 = self.rsrtbl.functionCall(&_ic_b_1);
{
let mut _ic_d_1 = self.nxt.functionCall(&_ic_c_1);
- if !((_ic_d_1.range().elementOf(&_ic_b_1) && _ic_a_1.equal(&_ic_d_1.inverse().functionCall(&_ic_b_1))).implies(&self.rsrtbl.functionCall(&_ic_a_1).unequal(&_ic_c_1))).booleanValue() {
+ if !((_ic_d_1.range().elementOf(&_ic_b_1) && _ic_a_1.equal(&_ic_d_1.inverse().functionCall(&_ic_b_1))).implies(|| self.rsrtbl.functionCall(&_ic_a_1).unequal(&_ic_c_1).booleanValue())).booleanValue() {
_ic_boolean_13 = BBoolean::new(false);
break;
}
@@ -552,7 +562,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
pub fn _check_inv_7(&self) -> bool {
//invariant
- return self.rsrtbl.checkDomain(&self.resbl).and(&self.rsrtbl.checkRange(&self.resrt)).and(&self.rsrtbl.isFunction()).and(&self.rsrtbl.isTotal(&self.resbl)).booleanValue();
+ return self.resbl.check_domain_of(&self.rsrtbl).and(&self.resrt.check_range_of(&self.rsrtbl)).and(&self.rsrtbl.isFunction()).and(&self.resbl.check_total_of(&self.rsrtbl)).booleanValue();
}
pub fn _check_inv_8(&self) -> bool {
@@ -573,10 +583,10 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
{
let mut _ic_a_1 = self.nxt.functionCall(&_ic_r_1);
{
- let mut _ic_b_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1]));
+ let mut _ic_b_1 = self.rsrtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()]));
{
let mut _ic_c_1 = _ic_b_1.difference(&self.OCC);
- if !(((_ic_a_1.relationImage(&self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1])).difference(&_ic_b_1)).intersect(&_ic_c_1).equal(&BSet::new(vec![])) && _ic_a_1.relationImage(&_ic_b_1).subset(&_ic_b_1)) && _ic_a_1.relationImage(&_ic_c_1).subset(&_ic_c_1))).booleanValue() {
+ if !(((_ic_a_1.relationImage(&self.rtbl.inverse().relationImage(&BSet::new(vec![_ic_r_1.clone()])).difference(&_ic_b_1)).intersect(&_ic_c_1).equal(&BSet::<BLOCKS>::new(vec![])) && _ic_a_1.relationImage(&_ic_b_1).subset(&_ic_b_1)) && _ic_a_1.relationImage(&_ic_c_1).subset(&_ic_c_1))).booleanValue() {
_ic_boolean_14 = BBoolean::new(false);
break;
}
@@ -732,8 +742,6 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: &Train_1_beebook_deterministic_MC_POR_v2, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -888,7 +896,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = Train_1_beebook_deterministic_MC_POR_v2::new();
let mut all_states = HashSet::<Train_1_beebook_deterministic_MC_POR_v2>::new();
@@ -906,11 +914,11 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -928,7 +936,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = Train_1_beebook_deterministic_MC_POR_v2::new();
@@ -957,14 +965,14 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -999,7 +1007,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -1012,9 +1020,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- Train_1_beebook_deterministic_MC_POR_v2::model_check_single_threaded(mc_type, is_caching);
+ Train_1_beebook_deterministic_MC_POR_v2::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- Train_1_beebook_deterministic_MC_POR_v2::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ Train_1_beebook_deterministic_MC_POR_v2::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
diff --git a/benchmarks/model_checking/Rust/nota_v2.rs b/benchmarks/model_checking/Rust/nota_v2.rs
index a52fae3f4..14f8137f1 100644
--- a/benchmarks/model_checking/Rust/nota_v2.rs
+++ b/benchmarks/model_checking/Rust/nota_v2.rs
@@ -11,6 +11,7 @@ use std::time::{Duration};
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
+use btypes::bobject;
use btypes::bboolean::{IntoBool, BBooleanT};
use btypes::bboolean::BBoolean;
use btypes::binteger::BInteger;
@@ -75,23 +76,23 @@ impl _Struct5 {
}
#[derive(Default, Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub struct _Struct1 {
+pub struct _Struct3 {
sid: BSet<SID>,
- err: RM_ERROR_CODES,
+ err: IN_ERROR_CODES,
}
-impl fmt::Display for _Struct1 {
+impl fmt::Display for _Struct3 {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "sid: {},err: {}", self.sid ,self.err)
}
}
-impl BObject for _Struct1 {}
-impl BStruct for _Struct1 {}
+impl BObject for _Struct3 {}
+impl BStruct for _Struct3 {}
-impl _Struct1 {
- pub fn new(mut sid: BSet<SID>, mut err: RM_ERROR_CODES) -> _Struct1 {
- let mut m: _Struct1 = Default::default();
+impl _Struct3 {
+ pub fn new(mut sid: BSet<SID>, mut err: IN_ERROR_CODES) -> _Struct3 {
+ let mut m: _Struct3 = Default::default();
m.sid = sid;m.err = err;
return m;
}
@@ -100,49 +101,49 @@ impl _Struct1 {
return self.sid.clone();
}
- pub fn get_err(&self) -> RM_ERROR_CODES {
+ pub fn get_err(&self) -> IN_ERROR_CODES {
return self.err.clone();
}
- pub fn override_sid(&self, sid: BSet<SID>) -> _Struct1 {
- return _Struct1::new(sid.clone(), self.err.clone());
+ pub fn override_sid(&self, sid: BSet<SID>) -> _Struct3 {
+ return _Struct3::new(sid.clone(), self.err.clone());
}
- pub fn override_err(&self, err: RM_ERROR_CODES) -> _Struct1 {
- return _Struct1::new(self.sid.clone(), err.clone());
+ pub fn override_err(&self, err: IN_ERROR_CODES) -> _Struct3 {
+ return _Struct3::new(self.sid.clone(), err.clone());
}
pub fn equal(
- &self, other: &_Struct1) -> BBoolean {
+ &self, other: &_Struct3) -> BBoolean {
return BBoolean::new(self.sid == other.sid && self.err == other.err);
}
- pub fn unequal(&self, other: &_Struct1) -> BBoolean {
+ pub fn unequal(&self, other: &_Struct3) -> BBoolean {
return BBoolean::new(self.sid != other.sid || self.err != other.err);
}
}
#[derive(Default, Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub struct _Struct3 {
+pub struct _Struct1 {
sid: BSet<SID>,
- err: IN_ERROR_CODES,
+ err: RM_ERROR_CODES,
}
-impl fmt::Display for _Struct3 {
+impl fmt::Display for _Struct1 {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "sid: {},err: {}", self.sid ,self.err)
}
}
-impl BObject for _Struct3 {}
-impl BStruct for _Struct3 {}
+impl BObject for _Struct1 {}
+impl BStruct for _Struct1 {}
-impl _Struct3 {
- pub fn new(mut sid: BSet<SID>, mut err: IN_ERROR_CODES) -> _Struct3 {
- let mut m: _Struct3 = Default::default();
+impl _Struct1 {
+ pub fn new(mut sid: BSet<SID>, mut err: RM_ERROR_CODES) -> _Struct1 {
+ let mut m: _Struct1 = Default::default();
m.sid = sid;m.err = err;
return m;
}
@@ -151,26 +152,26 @@ impl _Struct3 {
return self.sid.clone();
}
- pub fn get_err(&self) -> IN_ERROR_CODES {
+ pub fn get_err(&self) -> RM_ERROR_CODES {
return self.err.clone();
}
- pub fn override_sid(&self, sid: BSet<SID>) -> _Struct3 {
- return _Struct3::new(sid.clone(), self.err.clone());
+ pub fn override_sid(&self, sid: BSet<SID>) -> _Struct1 {
+ return _Struct1::new(sid.clone(), self.err.clone());
}
- pub fn override_err(&self, err: IN_ERROR_CODES) -> _Struct3 {
- return _Struct3::new(self.sid.clone(), err.clone());
+ pub fn override_err(&self, err: RM_ERROR_CODES) -> _Struct1 {
+ return _Struct1::new(self.sid.clone(), err.clone());
}
pub fn equal(
- &self, other: &_Struct3) -> BBoolean {
+ &self, other: &_Struct1) -> BBoolean {
return BBoolean::new(self.sid == other.sid && self.err == other.err);
}
- pub fn unequal(&self, other: &_Struct3) -> BBoolean {
+ pub fn unequal(&self, other: &_Struct1) -> BBoolean {
return BBoolean::new(self.sid != other.sid || self.err != other.err);
}
@@ -441,22 +442,22 @@ impl nota_v2 {
self._SID = BSet::new(vec![SID::SID1, SID::SID2]);
self._RM_ERROR_CODES = BSet::new(vec![RM_ERROR_CODES::RM_SERVICE_FOUND, RM_ERROR_CODES::RM_SERVICE_NOT_FOUND]);
self._IN_ERROR_CODES = BSet::new(vec![IN_ERROR_CODES::IN_REGISTRATION_OK, IN_ERROR_CODES::IN_REGISTRATION_FAILED, IN_ERROR_CODES::IN_DEREGISTRATION_OK, IN_ERROR_CODES::IN_DEREGISTRATION_FAILED, IN_ERROR_CODES::IN_NO_SOCKET_CONNECTION, IN_ERROR_CODES::IN_SOCKET_CONNECTION_OK, IN_ERROR_CODES::IN_NO_AVAILABLE_SERVICE, IN_ERROR_CODES::IN_SERVICE_AVAILABLE, IN_ERROR_CODES::IN_TARGET_SOCKET_GRANTED, IN_ERROR_CODES::IN_TARGET_SOCKET_NOT_GRANTED]);
- self.interconnectNodes = BSet::new(vec![]).clone().clone();
- self.sockets = BSet::new(vec![]).clone().clone();
- self.services = BSet::new(vec![]).clone().clone();
- self.resourceManagers = BSet::new(vec![]).clone().clone();
- self.sids = BSet::new(vec![]).clone().clone();
- self.rm_services = BRelation::new(vec![]).clone().clone();
- self.rm_sids = BRelation::new(vec![]).clone().clone();
- self.in_localServices = BRelation::new(vec![]).clone().clone();
- self.in_sockets = BRelation::new(vec![]).clone().clone();
- self.in_resourceManager = BRelation::new(vec![]).clone().clone();
- self.soc_to = BRelation::new(vec![]).clone().clone();
- self.soc_from = BRelation::new(vec![]).clone().clone();
- self.svc_serviceID = BRelation::new(vec![]).clone().clone();
- self.svc_sockets = BRelation::new(vec![]).clone().clone();
- self.svc_ICNode = BRelation::new(vec![]).clone().clone();
- self.svc_registered = BRelation::new(vec![]).clone().clone();
+ self.interconnectNodes = BSet::<INTERCONNECTNODE>::new(vec![]).clone().clone();
+ self.sockets = BSet::<SOCKET>::new(vec![]).clone().clone();
+ self.services = BSet::<SERVICE>::new(vec![]).clone().clone();
+ self.resourceManagers = BSet::<RESOURCEMANAGER>::new(vec![]).clone().clone();
+ self.sids = BSet::<SID>::new(vec![]).clone().clone();
+ self.rm_services = BRelation::<RESOURCEMANAGER, BSet<SERVICE>>::new(vec![]).clone().clone();
+ self.rm_sids = BRelation::<SERVICE, SID>::new(vec![]).clone().clone();
+ self.in_localServices = BRelation::<SID, INTERCONNECTNODE>::new(vec![]).clone().clone();
+ self.in_sockets = BRelation::<SOCKET, INTERCONNECTNODE>::new(vec![]).clone().clone();
+ self.in_resourceManager = BRelation::<INTERCONNECTNODE, BSet<RESOURCEMANAGER>>::new(vec![]).clone().clone();
+ self.soc_to = BRelation::<SOCKET, SID>::new(vec![]).clone().clone();
+ self.soc_from = BRelation::<SOCKET, SID>::new(vec![]).clone().clone();
+ self.svc_serviceID = BRelation::<SERVICE, SID>::new(vec![]).clone().clone();
+ self.svc_sockets = BRelation::<SERVICE, BSet<SOCKET>>::new(vec![]).clone().clone();
+ self.svc_ICNode = BRelation::<SERVICE, INTERCONNECTNODE>::new(vec![]).clone().clone();
+ self.svc_registered = BRelation::<SERVICE, BBoolean>::new(vec![]).clone().clone();
}
pub fn _get_interconnectNodes(&self) -> BSet<INTERCONNECTNODE> {
@@ -555,8 +556,8 @@ impl nota_v2 {
let mut oid: Option<INTERCONNECTNODE> = Option::None;
if (self._INTERCONNECTNODE.difference(&self.interconnectNodes).elementOf(&newic)).booleanValue() {
let mut _ld_interconnectNodes = self.interconnectNodes.clone();
- self.interconnectNodes = _ld_interconnectNodes._union(&BSet::new(vec![newic])).clone().clone();
- self.in_resourceManager = self.in_resourceManager._override(&BRelation::<INTERCONNECTNODE, BSet<RESOURCEMANAGER>>::new(vec![BTuple::new(newic,BSet::new(vec![]))]));
+ self.interconnectNodes = _ld_interconnectNodes._union(&BSet::new(vec![newic.clone()])).clone().clone();
+ self.in_resourceManager = self.in_resourceManager._override(&BRelation::<INTERCONNECTNODE, BSet<RESOURCEMANAGER>>::new(vec![BTuple::new(newic,BSet::<RESOURCEMANAGER>::new(vec![]))]));
oid = Option::Some(newic);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -568,8 +569,8 @@ impl nota_v2 {
let mut oid: Option<RESOURCEMANAGER> = Option::None;
//pre_assert
let mut _ld_resourceManagers = self.resourceManagers.clone();
- self.resourceManagers = _ld_resourceManagers._union(&BSet::new(vec![newrm])).clone().clone();
- self.rm_services = self.rm_services._override(&BRelation::<RESOURCEMANAGER, BSet<SERVICE>>::new(vec![BTuple::new(newrm,BSet::new(vec![]))]));
+ self.resourceManagers = _ld_resourceManagers._union(&BSet::new(vec![newrm.clone()])).clone().clone();
+ self.rm_services = self.rm_services._override(&BRelation::<RESOURCEMANAGER, BSet<SERVICE>>::new(vec![BTuple::new(newrm,BSet::<SERVICE>::new(vec![]))]));
oid = Option::Some(newrm);
return oid.unwrap();
@@ -579,11 +580,11 @@ impl nota_v2 {
let mut oid: Option<SERVICE> = Option::None;
//pre_assert
let mut _ld_services = self.services.clone();
- self.services = _ld_services._union(&BSet::new(vec![newsvc])).clone().clone();
+ self.services = _ld_services._union(&BSet::new(vec![newsvc.clone()])).clone().clone();
self.svc_registered = self.svc_registered._override(&BRelation::<SERVICE, BBoolean>::new(vec![BTuple::new(newsvc,BBoolean::new(false))]));
- self.svc_sockets = self.svc_sockets._override(&BRelation::<SERVICE, BSet<SOCKET>>::new(vec![BTuple::new(newsvc,BSet::new(vec![]))]));
+ self.svc_sockets = self.svc_sockets._override(&BRelation::<SERVICE, BSet<SOCKET>>::new(vec![BTuple::new(newsvc,BSet::<SOCKET>::new(vec![]))]));
self.svc_ICNode = self.svc_ICNode._override(&BRelation::<SERVICE, INTERCONNECTNODE>::new(vec![BTuple::new(newsvc,ii)]));
- self.svc_serviceID = BRelation::new(vec![]).clone().clone();
+ self.svc_serviceID = BRelation::<SERVICE, SID>::new(vec![]).clone().clone();
oid = Option::Some(newsvc);
return oid.unwrap();
@@ -593,7 +594,7 @@ impl nota_v2 {
let mut oid: Option<SOCKET> = Option::None;
//pre_assert
let mut _ld_sockets = self.sockets.clone();
- self.sockets = _ld_sockets._union(&BSet::new(vec![newsoc])).clone().clone();
+ self.sockets = _ld_sockets._union(&BSet::new(vec![newsoc.clone()])).clone().clone();
oid = Option::Some(newsoc);
self.in_sockets = self.in_sockets._override(&BRelation::<SOCKET, INTERCONNECTNODE>::new(vec![BTuple::new(newsoc,ii)]));
self.soc_to = self.soc_to._override(&BRelation::<SOCKET, SID>::new(vec![BTuple::new(newsoc,srcsid)]));
@@ -617,7 +618,7 @@ impl nota_v2 {
let mut err: Option<RM_ERROR_CODES> = Option::None;
//pre_assert
err = Option::Some(RM_ERROR_CODES::RM_SERVICE_FOUND);
- sid = Option::Some(BSet::new(vec![self.rm_sids.functionCall(&ss)]).clone()).clone();
+ sid = Option::Some(BSet::new(vec![self.rm_sids.functionCall(&ss).clone()]).clone()).clone();
return _Struct1::new(sid.unwrap(), err.unwrap());
}
@@ -634,7 +635,7 @@ impl nota_v2 {
pub fn in_announceResourceManager(&mut self, mut _self: INTERCONNECTNODE, mut rm: RESOURCEMANAGER) -> () {
//pre_assert
- self.in_resourceManager = self.in_resourceManager._override(&BRelation::<INTERCONNECTNODE, BSet<RESOURCEMANAGER>>::new(vec![BTuple::new(_self,self.in_resourceManager.functionCall(&_self)._union(&BSet::new(vec![rm])))]));
+ self.in_resourceManager = self.in_resourceManager._override(&BRelation::<INTERCONNECTNODE, BSet<RESOURCEMANAGER>>::new(vec![BTuple::new(_self,self.in_resourceManager.functionCall(&_self)._union(&BSet::new(vec![rm.clone()])))]));
}
@@ -645,10 +646,10 @@ impl nota_v2 {
let mut _ld_sids = self.sids.clone();
let mut _ld_in_localServices = self.in_localServices.clone();
- self.sids = _ld_sids._union(&BSet::new(vec![si])).clone().clone();
+ self.sids = _ld_sids._union(&BSet::new(vec![si.clone()])).clone().clone();
self.in_localServices = _ld_in_localServices._union(&BRelation::new(vec![BTuple::from_refs(&si, &_self)])).clone().clone();
err = Option::Some(IN_ERROR_CODES::IN_REGISTRATION_OK);
- sid = Option::Some(BSet::new(vec![si]).clone()).clone();
+ sid = Option::Some(BSet::new(vec![si.clone()]).clone()).clone();
return _Struct3::new(sid.unwrap(), err.unwrap());
}
@@ -669,8 +670,8 @@ impl nota_v2 {
//pre_assert
let mut _ld_sockets = self.sockets.clone();
let mut _ld_in_sockets = self.in_sockets.clone();
- self.sockets = _ld_sockets._union(&BSet::new(vec![newsoc])).clone().clone();
- soc = Option::Some(BSet::new(vec![newsoc]).clone()).clone();
+ self.sockets = _ld_sockets._union(&BSet::new(vec![newsoc.clone()])).clone().clone();
+ soc = Option::Some(BSet::new(vec![newsoc.clone()]).clone()).clone();
err = Option::Some(IN_ERROR_CODES::IN_TARGET_SOCKET_GRANTED);
self.in_sockets = _ld_in_sockets._union(&BRelation::new(vec![BTuple::from_refs(&newsoc, &_self)])).clone().clone();
self.soc_to = self.soc_to._override(&BRelation::<SOCKET, SID>::new(vec![BTuple::new(newsoc,srcsid)]));
@@ -701,6 +702,7 @@ impl nota_v2 {
let mut _ic_set_0: BSet<INTERCONNECTNODE> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_newic_1 in self._INTERCONNECTNODE.difference(&self.interconnectNodes).clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_0 = _ic_set_0._union(&BSet::new(vec![_ic_newic_1]));
}
@@ -717,7 +719,8 @@ impl nota_v2 {
let mut _ic_set_1: BSet<RESOURCEMANAGER> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_newrm_1 in self._RESOURCEMANAGER.difference(&self.resourceManagers).clone().iter().cloned() {
- if ((self.rm_services.domain().notElementOf(&_ic_newrm_1) && self.resourceManagers.equal(&BSet::new(vec![])))).booleanValue() {
+ //parameter_combination_predicate
+ if ((self.rm_services.domain().notElementOf(&_ic_newrm_1) && self.resourceManagers.equal(&BSet::<RESOURCEMANAGER>::new(vec![])))).booleanValue() {
_ic_set_1 = _ic_set_1._union(&BSet::new(vec![_ic_newrm_1]));
}
@@ -736,6 +739,7 @@ impl nota_v2 {
//transition, parameters, no condidtion
for _ic_ii_1 in self.interconnectNodes.clone().iter().cloned() {
for _ic_newsvc_1 in self._SERVICE.difference(&self.services).clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_2 = _ic_set_2._union(&BSet::new(vec![BTuple::from_refs(&_ic_ii_1, &_ic_newsvc_1)]));
}
@@ -756,6 +760,7 @@ impl nota_v2 {
for _ic_srcsid_1 in self.sids.clone().iter().cloned() {
for _ic_targsid_1 in self.sids.clone().iter().cloned() {
for _ic_newsoc_1 in self._SOCKET.difference(&self.sockets).clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_3 = _ic_set_3._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&_ic_ii_1, &_ic_srcsid_1), &_ic_targsid_1), &_ic_newsoc_1)]));
}
@@ -777,6 +782,7 @@ impl nota_v2 {
for _ic_self_1 in self.resourceManagers.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
for _ic_ii_1 in self.interconnectNodes.clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_4 = _ic_set_4._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&_ic_self_1, &_ic_ss_1), &_ic_ii_1)]));
}
@@ -797,6 +803,7 @@ impl nota_v2 {
for _ic_self_1 in self.resourceManagers.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
for _ic_ii_1 in self.interconnectNodes.clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_5 = _ic_set_5._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&_ic_self_1, &_ic_ss_1), &_ic_ii_1)]));
}
@@ -816,6 +823,7 @@ impl nota_v2 {
//transition, parameters, no condidtion
for _ic_self_1 in self.resourceManagers.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.rm_sids.domain().elementOf(&_ic_ss_1)).booleanValue() {
_ic_set_6 = _ic_set_6._union(&BSet::new(vec![BTuple::from_refs(&_ic_self_1, &_ic_ss_1)]));
}
@@ -836,6 +844,7 @@ impl nota_v2 {
//transition, parameters, no condidtion
for _ic_self_1 in self.resourceManagers.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_7 = _ic_set_7._union(&BSet::new(vec![BTuple::from_refs(&_ic_self_1, &_ic_ss_1)]));
}
@@ -854,7 +863,8 @@ impl nota_v2 {
//transition, parameters, no condidtion
for _ic_self_1 in self.interconnectNodes.clone().iter().cloned() {
for _ic_rm_1 in self.resourceManagers.clone().iter().cloned() {
- if (self.in_resourceManager.functionCall(&_ic_self_1).equal(&BSet::new(vec![]))).booleanValue() {
+ //parameter_combination_predicate
+ if (self.in_resourceManager.functionCall(&_ic_self_1).equal(&BSet::<RESOURCEMANAGER>::new(vec![]))).booleanValue() {
_ic_set_8 = _ic_set_8._union(&BSet::new(vec![BTuple::from_refs(&_ic_self_1, &_ic_rm_1)]));
}
@@ -875,6 +885,7 @@ impl nota_v2 {
for _ic_self_1 in self.interconnectNodes.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
for _ic_si_1 in self._SID.difference(&self.sids).clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.in_localServices.domain().elementOf(&_ic_si_1).not()).booleanValue() {
_ic_set_9 = _ic_set_9._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&_ic_self_1, &_ic_ss_1), &_ic_si_1)]));
}
@@ -896,6 +907,7 @@ impl nota_v2 {
//transition, parameters, no condidtion
for _ic_self_1 in self.interconnectNodes.clone().iter().cloned() {
for _ic_ss_1 in self.services.clone().iter().cloned() {
+ //parameter_combination_predicate
_ic_set_10 = _ic_set_10._union(&BSet::new(vec![BTuple::from_refs(&_ic_self_1, &_ic_ss_1)]));
}
@@ -918,6 +930,7 @@ impl nota_v2 {
for _ic_srcsid_1 in self.sids.clone().iter().cloned() {
for _ic_targsid_1 in self.sids.clone().iter().cloned() {
for _ic_newsoc_1 in self._SOCKET.difference(&self.sockets).clone().iter().cloned() {
+ //parameter_combination_predicate
if ((_ic_self_1.unequal(&_ic_ii_1) && self.in_sockets.functionCall(&_ic_srcsoc_1).equal(&_ic_ii_1))).booleanValue() {
_ic_set_11 = _ic_set_11._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&_ic_self_1, &_ic_ii_1), &_ic_srcsoc_1), &_ic_srcsid_1), &_ic_targsid_1), &_ic_newsoc_1)]));
}
@@ -945,6 +958,7 @@ impl nota_v2 {
for _ic_srcsoc_1 in self.sockets.clone().iter().cloned() {
for _ic_srcsid_1 in self.sids.clone().iter().cloned() {
for _ic_targsid_1 in self.sids.clone().iter().cloned() {
+ //parameter_combination_predicate
if ((_ic_self_1.unequal(&_ic_ii_1) && self.in_sockets.functionCall(&_ic_srcsoc_1).equal(&_ic_ii_1))).booleanValue() {
_ic_set_12 = _ic_set_12._union(&BSet::new(vec![BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&BTuple::from_refs(&_ic_self_1, &_ic_ii_1), &_ic_srcsoc_1), &_ic_srcsid_1), &_ic_targsid_1)]));
}
@@ -967,6 +981,7 @@ impl nota_v2 {
let mut _ic_set_13: BSet<SERVICE> = BSet::new(vec![]);
//transition, parameters, no condidtion
for _ic_self_1 in self.services.clone().iter().cloned() {
+ //parameter_combination_predicate
if (self.svc_registered.functionCall(&_ic_self_1).equal(&BBoolean::new(false))).booleanValue() {
_ic_set_13 = _ic_set_13._union(&BSet::new(vec![_ic_self_1]));
}
@@ -1006,7 +1021,7 @@ impl nota_v2 {
pub fn _check_inv_6(&self) -> bool {
//invariant
- return self.rm_services.checkDomain(&self.resourceManagers).and(&self.rm_services.checkRange(&self.services.pow())).and(&self.rm_services.isFunction()).and(&self.rm_services.isTotal(&self.resourceManagers)).booleanValue();
+ return self.resourceManagers.check_domain_of(&self.rm_services).and(&self.services.pow().check_range_of(&self.rm_services)).and(&self.rm_services.isFunction()).and(&self.resourceManagers.check_total_of(&self.rm_services)).booleanValue();
}
pub fn _check_inv_7(&self) -> bool {
@@ -1015,7 +1030,7 @@ impl nota_v2 {
let mut _ic_boolean_14 = BBoolean::new(true);
for _ic_a1_1 in self.rm_services.domain().clone().iter().cloned() {
for _ic_a2_1 in self.rm_services.domain().clone().iter().cloned() {
- if !(_ic_a1_1.unequal(&_ic_a2_1).implies(&self.rm_services.functionCall(&_ic_a1_1).intersect(&self.rm_services.functionCall(&_ic_a2_1)).equal(&BSet::new(vec![])))).booleanValue() {
+ if !(_ic_a1_1.unequal(&_ic_a2_1).implies(|| self.rm_services.functionCall(&_ic_a1_1).intersect(&self.rm_services.functionCall(&_ic_a2_1)).equal(&BSet::<SERVICE>::new(vec![])).booleanValue())).booleanValue() {
_ic_boolean_14 = BBoolean::new(false);
break;
}
@@ -1028,57 +1043,57 @@ impl nota_v2 {
pub fn _check_inv_8(&self) -> bool {
//invariant
- return self.rm_sids.checkDomain(&self.services).and(&self.rm_sids.checkRange(&self.sids)).and(&self.rm_sids.isFunction()).and(&self.rm_sids.isPartial(&self.services)).and(&self.rm_sids.isInjection()).booleanValue();
+ return self.services.check_domain_of(&self.rm_sids).and(&self.sids.check_range_of(&self.rm_sids)).and(&self.rm_sids.isFunction()).and(&self.services.check_partial_of(&self.rm_sids)).and(&self.rm_sids.isInjection()).booleanValue();
}
pub fn _check_inv_9(&self) -> bool {
//invariant
- return self.in_localServices.checkDomain(&self.sids).and(&self.in_localServices.checkRange(&self.interconnectNodes)).and(&self.in_localServices.isFunction()).and(&self.in_localServices.isTotal(&self.sids)).booleanValue();
+ return self.sids.check_domain_of(&self.in_localServices).and(&self.interconnectNodes.check_range_of(&self.in_localServices)).and(&self.in_localServices.isFunction()).and(&self.sids.check_total_of(&self.in_localServices)).booleanValue();
}
pub fn _check_inv_10(&self) -> bool {
//invariant
- return self.in_sockets.checkDomain(&self.sockets).and(&self.in_sockets.checkRange(&self.interconnectNodes)).and(&self.in_sockets.isFunction()).and(&self.in_sockets.isTotal(&self.sockets)).booleanValue();
+ return self.sockets.check_domain_of(&self.in_sockets).and(&self.interconnectNodes.check_range_of(&self.in_sockets)).and(&self.in_sockets.isFunction()).and(&self.sockets.check_total_of(&self.in_sockets)).booleanValue();
}
pub fn _check_inv_11(&self) -> bool {
//invariant
- return self.in_resourceManager.checkDomain(&self.interconnectNodes).and(&self.in_resourceManager.checkRange(&self.resourceManagers.pow())).and(&self.in_resourceManager.isFunction()).and(&self.in_resourceManager.isTotal(&self.interconnectNodes)).booleanValue();
+ return self.interconnectNodes.check_domain_of(&self.in_resourceManager).and(&self.resourceManagers.pow().check_range_of(&self.in_resourceManager)).and(&self.in_resourceManager.isFunction()).and(&self.interconnectNodes.check_total_of(&self.in_resourceManager)).booleanValue();
}
pub fn _check_inv_12(&self) -> bool {
//invariant
- return self.soc_to.checkDomain(&self.sockets).and(&self.soc_to.checkRange(&self.sids)).and(&self.soc_to.isFunction()).and(&self.soc_to.isTotal(&self.sockets)).booleanValue();
+ return self.sockets.check_domain_of(&self.soc_to).and(&self.sids.check_range_of(&self.soc_to)).and(&self.soc_to.isFunction()).and(&self.sockets.check_total_of(&self.soc_to)).booleanValue();
}
pub fn _check_inv_13(&self) -> bool {
//invariant
- return self.soc_from.checkDomain(&self.sockets).and(&self.soc_from.checkRange(&self.sids)).and(&self.soc_from.isFunction()).and(&self.soc_from.isTotal(&self.sockets)).booleanValue();
+ return self.sockets.check_domain_of(&self.soc_from).and(&self.sids.check_range_of(&self.soc_from)).and(&self.soc_from.isFunction()).and(&self.sockets.check_total_of(&self.soc_from)).booleanValue();
}
pub fn _check_inv_14(&self) -> bool {
//invariant
- return self.svc_serviceID.checkDomain(&self.services).and(&self.svc_serviceID.checkRange(&self.sids)).and(&self.svc_serviceID.isFunction()).and(&self.svc_serviceID.isPartial(&self.services)).booleanValue();
+ return self.services.check_domain_of(&self.svc_serviceID).and(&self.sids.check_range_of(&self.svc_serviceID)).and(&self.svc_serviceID.isFunction()).and(&self.services.check_partial_of(&self.svc_serviceID)).booleanValue();
}
pub fn _check_inv_15(&self) -> bool {
//invariant
- return self.svc_sockets.checkDomain(&self.services).and(&self.svc_sockets.checkRange(&self.sockets.pow())).and(&self.svc_sockets.isFunction()).and(&self.svc_sockets.isTotal(&self.services)).booleanValue();
+ return self.services.check_domain_of(&self.svc_sockets).and(&self.sockets.pow().check_range_of(&self.svc_sockets)).and(&self.svc_sockets.isFunction()).and(&self.services.check_total_of(&self.svc_sockets)).booleanValue();
}
pub fn _check_inv_16(&self) -> bool {
//invariant
- return self.svc_ICNode.checkDomain(&self.services).and(&self.svc_ICNode.checkRange(&self.interconnectNodes)).and(&self.svc_ICNode.isFunction()).and(&self.svc_ICNode.isTotal(&self.services)).booleanValue();
+ return self.services.check_domain_of(&self.svc_ICNode).and(&self.interconnectNodes.check_range_of(&self.svc_ICNode)).and(&self.svc_ICNode.isFunction()).and(&self.services.check_total_of(&self.svc_ICNode)).booleanValue();
}
pub fn _check_inv_17(&self) -> bool {
//invariant
- return self.svc_registered.checkDomain(&self.services).and(&self.svc_registered.checkRange(&butils::BOOL)).and(&self.svc_registered.isFunction()).and(&self.svc_registered.isTotal(&self.services)).booleanValue();
+ return self.services.check_domain_of(&self.svc_registered).and(&(*butils::BOOL).check_range_of(&self.svc_registered)).and(&self.svc_registered.isFunction()).and(&self.services.check_total_of(&self.svc_registered)).booleanValue();
}
pub fn _check_inv_18(&self) -> bool {
//invariant
- return self.resourceManagers.equal(&BSet::new(vec![])).not().implies(&self.resourceManagers.card().equal(&BInteger::new(1))).booleanValue();
+ return self.resourceManagers.equal(&BSet::<RESOURCEMANAGER>::new(vec![])).not().implies(|| self.resourceManagers.card().equal(&BInteger::new(1)).booleanValue()).booleanValue();
}
fn invalidate_caches(&mut self, to_invalidate: Vec<&'static str>) {
@@ -1368,8 +1383,6 @@ impl nota_v2 {
return result;
}
- //model_check_evaluate_state
-
//model_check_invariants
pub fn checkInvariants(state: ¬a_v2, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
@@ -1590,7 +1603,7 @@ impl nota_v2 {
}
}
- fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = nota_v2::new();
let mut all_states = HashSet::<nota_v2>::new();
@@ -1608,11 +1621,11 @@ impl nota_v2 {
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
- if next_states.is_empty() {
+ if !no_dead && next_states.is_empty() {
print!("DEADLOCK DETECTED");
stop_threads = true;
}
@@ -1630,7 +1643,7 @@ impl nota_v2 {
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
- fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = nota_v2::new();
@@ -1659,14 +1672,14 @@ impl nota_v2 {
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
- if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+ if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
//println!("Thread {:?} executing", thread::current().id());
next_states.into_iter()
.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) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -1701,7 +1714,7 @@ impl nota_v2 {
fn main() {
let args: Vec<String> = env::args().collect();
- if args.len() != 4 { panic!("Number of arguments errorneous"); }
+ if args.len() < 4 { panic!("Number of arguments errorneous"); }
let threads = args.get(2).unwrap().parse::<usize>().unwrap();
if threads <= 0 { panic!("Input for number of threads is wrong."); }
@@ -1714,9 +1727,22 @@ fn main() {
_ => panic!("Input for strategy is wrong.")
};
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
if threads == 1 {
- nota_v2::model_check_single_threaded(mc_type, is_caching);
+ nota_v2::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- nota_v2::modelCheckMultiThreaded(mc_type, threads, is_caching);
+ nota_v2::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
--
GitLab