diff --git a/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc.rs b/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc.rs
index 31088acc5b0615d0729a690f416a34bd01fc9045..62cc67ae559c84aaea3a7f074b831ae0e7d7a552 100644
--- a/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc.rs
+++ b/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::brelation::BRelation;
@@ -12,9 +14,9 @@ use btypes::btuple::BTuple;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T1state {
- T1_EN,
- T1_CALC,
- T1_SEND,
+ T1_EN,
+ T1_CALC,
+ T1_SEND,
T1_WAIT
}
impl T1state {
@@ -27,19 +29,19 @@ impl Default for T1state {
}
impl fmt::Display for T1state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T1state::T1_EN => write!(f, "T1_EN"),
- T1state::T1_CALC => write!(f, "T1_CALC"),
- T1state::T1_SEND => write!(f, "T1_SEND"),
- T1state::T1_WAIT => write!(f, "T1_WAIT"),
- }
+ match *self {
+ T1state::T1_EN => write!(f, "T1_EN"),
+ T1state::T1_CALC => write!(f, "T1_CALC"),
+ T1state::T1_SEND => write!(f, "T1_SEND"),
+ T1state::T1_WAIT => write!(f, "T1_WAIT"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2mode {
- T2MODE_SENSE,
- T2MODE_TRANSMIT,
+ T2MODE_SENSE,
+ T2MODE_TRANSMIT,
T2MODE_RELEASE
}
impl T2mode {
@@ -52,22 +54,22 @@ impl Default for T2mode {
}
impl fmt::Display for T2mode {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T2mode::T2MODE_SENSE => write!(f, "T2MODE_SENSE"),
- T2mode::T2MODE_TRANSMIT => write!(f, "T2MODE_TRANSMIT"),
- T2mode::T2MODE_RELEASE => write!(f, "T2MODE_RELEASE"),
- }
+ match *self {
+ T2mode::T2MODE_SENSE => write!(f, "T2MODE_SENSE"),
+ T2mode::T2MODE_TRANSMIT => write!(f, "T2MODE_TRANSMIT"),
+ T2mode::T2MODE_RELEASE => write!(f, "T2MODE_RELEASE"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2state {
- T2_EN,
- T2_RCV,
- T2_PROC,
- T2_CALC,
- T2_SEND,
- T2_WAIT,
+ T2_EN,
+ T2_RCV,
+ T2_PROC,
+ T2_CALC,
+ T2_SEND,
+ T2_WAIT,
T2_RELEASE
}
impl T2state {
@@ -80,25 +82,25 @@ impl Default for T2state {
}
impl fmt::Display for T2state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T2state::T2_EN => write!(f, "T2_EN"),
- T2state::T2_RCV => write!(f, "T2_RCV"),
- T2state::T2_PROC => write!(f, "T2_PROC"),
- T2state::T2_CALC => write!(f, "T2_CALC"),
- T2state::T2_SEND => write!(f, "T2_SEND"),
- T2state::T2_WAIT => write!(f, "T2_WAIT"),
- T2state::T2_RELEASE => write!(f, "T2_RELEASE"),
- }
+ match *self {
+ T2state::T2_EN => write!(f, "T2_EN"),
+ T2state::T2_RCV => write!(f, "T2_RCV"),
+ T2state::T2_PROC => write!(f, "T2_PROC"),
+ T2state::T2_CALC => write!(f, "T2_CALC"),
+ T2state::T2_SEND => write!(f, "T2_SEND"),
+ T2state::T2_WAIT => write!(f, "T2_WAIT"),
+ T2state::T2_RELEASE => write!(f, "T2_RELEASE"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T3state {
- T3_READY,
- T3_WRITE,
- T3_RELEASE,
- T3_READ,
- T3_PROC,
+ T3_READY,
+ T3_WRITE,
+ T3_RELEASE,
+ T3_READ,
+ T3_PROC,
T3_WAIT
}
impl T3state {
@@ -111,18 +113,18 @@ impl Default for T3state {
}
impl fmt::Display for T3state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- T3state::T3_READY => write!(f, "T3_READY"),
- T3state::T3_WRITE => write!(f, "T3_WRITE"),
- T3state::T3_RELEASE => write!(f, "T3_RELEASE"),
- T3state::T3_READ => write!(f, "T3_READ"),
- T3state::T3_PROC => write!(f, "T3_PROC"),
- T3state::T3_WAIT => write!(f, "T3_WAIT"),
- }
+ match *self {
+ T3state::T3_READY => write!(f, "T3_READY"),
+ T3state::T3_WRITE => write!(f, "T3_WRITE"),
+ T3state::T3_RELEASE => write!(f, "T3_RELEASE"),
+ T3state::T3_READ => write!(f, "T3_READ"),
+ T3state::T3_PROC => write!(f, "T3_PROC"),
+ T3state::T3_WAIT => write!(f, "T3_WAIT"),
+ }
}
}
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct CAN_BUS_tlc {
BUSpriority: BInteger,
BUSvalue: BInteger,
@@ -149,6 +151,32 @@ pub struct CAN_BUS_tlc {
_T3state: BSet<T3state>,
}
+impl fmt::Display for CAN_BUS_tlc {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "CAN_BUS_tlc: (".to_owned();
+ result += &format!("_get_BUSpriority: {}, ", self._get_BUSpriority());
+ result += &format!("_get_BUSvalue: {}, ", self._get_BUSvalue());
+ result += &format!("_get_BUSwrite: {}, ", self._get_BUSwrite());
+ result += &format!("_get_T1_state: {}, ", self._get_T1_state());
+ result += &format!("_get_T1_timer: {}, ", self._get_T1_timer());
+ result += &format!("_get_T1_writevalue: {}, ", self._get_T1_writevalue());
+ result += &format!("_get_T2_mode: {}, ", self._get_T2_mode());
+ result += &format!("_get_T2_readpriority: {}, ", self._get_T2_readpriority());
+ result += &format!("_get_T2_readvalue: {}, ", self._get_T2_readvalue());
+ result += &format!("_get_T2_state: {}, ", self._get_T2_state());
+ result += &format!("_get_T2_timer: {}, ", self._get_T2_timer());
+ result += &format!("_get_T2_writevalue: {}, ", self._get_T2_writevalue());
+ result += &format!("_get_T2v: {}, ", self._get_T2v());
+ result += &format!("_get_T3_enabled: {}, ", self._get_T3_enabled());
+ result += &format!("_get_T3_evaluated: {}, ", self._get_T3_evaluated());
+ result += &format!("_get_T3_readpriority: {}, ", self._get_T3_readpriority());
+ result += &format!("_get_T3_readvalue: {}, ", self._get_T3_readvalue());
+ result += &format!("_get_T3_state: {}, ", self._get_T3_state());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl CAN_BUS_tlc {
pub fn new() -> CAN_BUS_tlc {
@@ -158,6 +186,11 @@ impl CAN_BUS_tlc {
return m;
}
fn init(&mut self) {
+ self._T1state = BSet::new(vec![T1state::T1_EN, T1state::T1_CALC, T1state::T1_SEND, T1state::T1_WAIT]);
+ self._T2mode = BSet::new(vec![T2mode::T2MODE_SENSE, T2mode::T2MODE_TRANSMIT, T2mode::T2MODE_RELEASE]);
+ self._T2state = BSet::new(vec![T2state::T2_EN, T2state::T2_RCV, T2state::T2_PROC, T2state::T2_CALC, T2state::T2_SEND, T2state::T2_WAIT, T2state::T2_RELEASE]);
+ self._T3state = BSet::new(vec![T3state::T3_READY, T3state::T3_WRITE, T3state::T3_RELEASE, T3state::T3_READ, T3state::T3_PROC, T3state::T3_WAIT]);
+ self.NATSET = BSet::<BInteger>::interval(&BInteger::new(0), &BInteger::new(5));
self.T2v = BInteger::new(0);
self.T3_evaluated = BBoolean::new(true);
self.T3_enabled = BBoolean::new(true);
@@ -176,215 +209,251 @@ impl CAN_BUS_tlc {
self.BUSvalue = BInteger::new(0);
self.BUSpriority = BInteger::new(0);
self.T2_mode = T2mode::T2MODE_SENSE;
- self._T1state = BSet::new(vec![T1state::T1_EN, T1state::T1_CALC, T1state::T1_SEND, T1state::T1_WAIT]);
- self._T2mode = BSet::new(vec![T2mode::T2MODE_SENSE, T2mode::T2MODE_TRANSMIT, T2mode::T2MODE_RELEASE]);
- self._T2state = BSet::new(vec![T2state::T2_EN, T2state::T2_RCV, T2state::T2_PROC, T2state::T2_CALC, T2state::T2_SEND, T2state::T2_WAIT, T2state::T2_RELEASE]);
- self._T3state = BSet::new(vec![T3state::T3_READY, T3state::T3_WRITE, T3state::T3_RELEASE, T3state::T3_READ, T3state::T3_PROC, T3state::T3_WAIT]);
- self.NATSET = BSet::<BInteger>::interval(&BInteger::new(0), &BInteger::new(5));
}
- pub fn get_NATSET(&self) -> BSet<BInteger> {
+ pub fn _get_NATSET(&self) -> BSet<BInteger> {
return self.NATSET.clone();
}
- pub fn get_BUSpriority(&self) -> BInteger {
+ pub fn _get_BUSpriority(&self) -> BInteger {
return self.BUSpriority.clone();
}
- pub fn get_BUSvalue(&self) -> BInteger {
+ pub fn _get_BUSvalue(&self) -> BInteger {
return self.BUSvalue.clone();
}
- pub fn get_BUSwrite(&self) -> BRelation<BInteger, BInteger> {
+ pub fn _get_BUSwrite(&self) -> BRelation<BInteger, BInteger> {
return self.BUSwrite.clone();
}
- pub fn get_T1_state(&self) -> T1state {
+ pub fn _get_T1_state(&self) -> T1state {
return self.T1_state.clone();
}
- pub fn get_T1_timer(&self) -> BInteger {
+ pub fn _get_T1_timer(&self) -> BInteger {
return self.T1_timer.clone();
}
- pub fn get_T1_writevalue(&self) -> BInteger {
+ pub fn _get_T1_writevalue(&self) -> BInteger {
return self.T1_writevalue.clone();
}
- pub fn get_T2_mode(&self) -> T2mode {
+ pub fn _get_T2_mode(&self) -> T2mode {
return self.T2_mode.clone();
}
- pub fn get_T2_readpriority(&self) -> BInteger {
+ pub fn _get_T2_readpriority(&self) -> BInteger {
return self.T2_readpriority.clone();
}
- pub fn get_T2_readvalue(&self) -> BInteger {
+ pub fn _get_T2_readvalue(&self) -> BInteger {
return self.T2_readvalue.clone();
}
- pub fn get_T2_state(&self) -> T2state {
+ pub fn _get_T2_state(&self) -> T2state {
return self.T2_state.clone();
}
- pub fn get_T2_timer(&self) -> BInteger {
+ pub fn _get_T2_timer(&self) -> BInteger {
return self.T2_timer.clone();
}
- pub fn get_T2_writevalue(&self) -> BInteger {
+ pub fn _get_T2_writevalue(&self) -> BInteger {
return self.T2_writevalue.clone();
}
- pub fn get_T2v(&self) -> BInteger {
+ pub fn _get_T2v(&self) -> BInteger {
return self.T2v.clone();
}
- pub fn get_T3_enabled(&self) -> BBoolean {
+ pub fn _get_T3_enabled(&self) -> BBoolean {
return self.T3_enabled.clone();
}
- pub fn get_T3_evaluated(&self) -> BBoolean {
+ pub fn _get_T3_evaluated(&self) -> BBoolean {
return self.T3_evaluated.clone();
}
- pub fn get_T3_readpriority(&self) -> BInteger {
+ pub fn _get_T3_readpriority(&self) -> BInteger {
return self.T3_readpriority.clone();
}
- pub fn get_T3_readvalue(&self) -> BInteger {
+ pub fn _get_T3_readvalue(&self) -> BInteger {
return self.T3_readvalue.clone();
}
- pub fn get_T3_state(&self) -> T3state {
+ pub fn _get_T3_state(&self) -> T3state {
return self.T3_state.clone();
}
- pub fn get__T1state(&self) -> BSet<T1state> {
+ pub fn _get__T1state(&self) -> BSet<T1state> {
return self._T1state.clone();
}
- pub fn get__T2mode(&self) -> BSet<T2mode> {
+ pub fn _get__T2mode(&self) -> BSet<T2mode> {
return self._T2mode.clone();
}
- pub fn get__T2state(&self) -> BSet<T2state> {
+ pub fn _get__T2state(&self) -> BSet<T2state> {
return self._T2state.clone();
}
- pub fn get__T3state(&self) -> BSet<T3state> {
+ pub fn _get__T3state(&self) -> BSet<T3state> {
return self._T3state.clone();
}
pub fn T1Evaluate(&mut self) -> () {
+ //pre_assert
self.T1_timer = BInteger::new(0);
self.T1_state = T1state::T1_CALC;
+
}
pub fn T1Calculate(&mut self, mut p: BInteger) -> () {
+ //pre_assert
self.T1_writevalue = p;
self.T1_state = T1state::T1_SEND;
+
}
pub fn T1SendResult(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
+ //pre_assert
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T1_state = T1state::T1_WAIT;
+
}
pub fn T1Wait(&mut self, mut pt: BInteger) -> () {
+ //pre_assert
self.T1_timer = pt;
self.T1_state = T1state::T1_EN;
+
}
pub fn T2Evaluate(&mut self) -> () {
+ //pre_assert
self.T2_timer = BInteger::new(0);
self.T2_state = T2state::T2_RCV;
+
}
pub fn T2ReadBus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
+ //pre_assert
self.T2_readvalue = pv;
self.T2_readpriority = ppriority;
self.T2_state = T2state::T2_PROC;
+
}
pub fn T2Reset(&mut self) -> () {
+ //pre_assert
let mut _ld_T2v = self.T2v.clone();
self.T2_writevalue = _ld_T2v;
self.T2v = BInteger::new(0);
self.T2_state = T2state::T2_SEND;
self.T2_mode = T2mode::T2MODE_TRANSMIT;
+
}
pub fn T2Complete(&mut self) -> () {
+ //pre_assert
self.T2_state = T2state::T2_RELEASE;
self.T2_mode = T2mode::T2MODE_SENSE;
+
}
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;
+
}
pub fn T2Calculate(&mut self) -> () {
+ //pre_assert
self.T2v = self.T2_readvalue;
self.T2_state = T2state::T2_WAIT;
+
}
pub fn T2WriteBus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
+ //pre_assert
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T2_state = T2state::T2_WAIT;
+
}
pub fn T2Wait(&mut self, mut pt: BInteger) -> () {
+ //pre_assert
self.T2_timer = pt;
self.T2_state = T2state::T2_EN;
+
}
pub fn T3Initiate(&mut self) -> () {
+ //pre_assert
self.T3_state = T3state::T3_WRITE;
self.T3_enabled = BBoolean::new(false);
+
}
pub fn T3Evaluate(&mut self) -> () {
+ //pre_assert
self.T3_state = T3state::T3_READ;
+
}
pub fn T3writebus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
+ //pre_assert
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T3_state = T3state::T3_WAIT;
+
}
pub fn T3Read(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
+ //pre_assert
self.T3_readvalue = pv;
self.T3_readpriority = ppriority;
self.T3_state = T3state::T3_PROC;
+
}
pub fn T3Poll(&mut self) -> () {
+ //pre_assert
self.T3_state = T3state::T3_WAIT;
+
}
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;
+
}
pub fn T3Wait(&mut self) -> () {
+ //pre_assert
self.T3_state = T3state::T3_READY;
self.T3_evaluated = BBoolean::new(true);
+
}
pub fn T3ReEnableWait(&mut self) -> () {
+ //pre_assert
self.T3_state = T3state::T3_READY;
self.T3_evaluated = BBoolean::new(true);
self.T3_enabled = BBoolean::new(true);
+
}
pub fn Update(&mut self, mut pmax: BInteger) -> () {
+ //pre_assert
let mut _ld_T1_timer = self.T1_timer.clone();
let mut _ld_T2_timer = self.T2_timer.clone();
self.BUSvalue = self.BUSwrite.functionCall(&pmax);
diff --git a/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc_exec.rs b/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc_exec.rs
index 73c436304e506c64131b87c184dcb34df6055c20..71f62247e3b3fdcef740cf0f42f881e14b8177ab 100644
--- a/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc_exec.rs
+++ b/benchmarks/execution/Rust_Primitives/CAN_BUS_tlc_exec.rs
@@ -1,19 +1,30 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
mod CAN_BUS_tlc;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct CAN_BUS_tlc_exec {
counter: BInteger,
_CAN_BUS_tlc: CAN_BUS_tlc::CAN_BUS_tlc,
}
+impl fmt::Display for CAN_BUS_tlc_exec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "CAN_BUS_tlc_exec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl CAN_BUS_tlc_exec {
pub fn new() -> CAN_BUS_tlc_exec {
@@ -27,7 +38,7 @@ impl CAN_BUS_tlc_exec {
self._CAN_BUS_tlc = CAN_BUS_tlc::CAN_BUS_tlc::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic.rs b/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic.rs
index 339667893bf3354cf3780f6e44f9b8e492498a33..4a76b168d759289f4f904b6b3a5e4247a67f53f1 100644
--- a/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic.rs
+++ b/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bset::BSet;
@@ -10,9 +12,9 @@ use btypes::bobject::BObject;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum RSset {
- RSnone,
- RSpos,
- RSneg,
+ RSnone,
+ RSpos,
+ RSneg,
RSequal
}
impl RSset {
@@ -25,19 +27,19 @@ impl Default for RSset {
}
impl fmt::Display for RSset {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- RSset::RSnone => write!(f, "RSnone"),
- RSset::RSpos => write!(f, "RSpos"),
- RSset::RSneg => write!(f, "RSneg"),
- RSset::RSequal => write!(f, "RSequal"),
- }
+ match *self {
+ RSset::RSnone => write!(f, "RSnone"),
+ RSset::RSpos => write!(f, "RSpos"),
+ RSset::RSneg => write!(f, "RSneg"),
+ RSset::RSequal => write!(f, "RSequal"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ODset {
- ODnone,
- ODclose,
+ ODnone,
+ ODclose,
ODveryclose
}
impl ODset {
@@ -50,15 +52,15 @@ impl Default for ODset {
}
impl fmt::Display for ODset {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- ODset::ODnone => write!(f, "ODnone"),
- ODset::ODclose => write!(f, "ODclose"),
- ODset::ODveryclose => write!(f, "ODveryclose"),
- }
+ match *self {
+ ODset::ODnone => write!(f, "ODnone"),
+ ODset::ODclose => write!(f, "ODclose"),
+ ODset::ODveryclose => write!(f, "ODveryclose"),
+ }
}
}
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Cruise_finite1_deterministic {
CruiseAllowed: BBoolean,
CruiseActive: BBoolean,
@@ -79,6 +81,29 @@ pub struct Cruise_finite1_deterministic {
_ODset: BSet<ODset>,
}
+impl fmt::Display for Cruise_finite1_deterministic {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Cruise_finite1_deterministic: (".to_owned();
+ result += &format!("_get_CruiseAllowed: {}, ", self._get_CruiseAllowed());
+ result += &format!("_get_CruiseActive: {}, ", self._get_CruiseActive());
+ result += &format!("_get_VehicleAtCruiseSpeed: {}, ", self._get_VehicleAtCruiseSpeed());
+ result += &format!("_get_VehicleCanKeepSpeed: {}, ", self._get_VehicleCanKeepSpeed());
+ result += &format!("_get_VehicleTryKeepSpeed: {}, ", self._get_VehicleTryKeepSpeed());
+ result += &format!("_get_SpeedAboveMax: {}, ", self._get_SpeedAboveMax());
+ result += &format!("_get_VehicleTryKeepTimeGap: {}, ", self._get_VehicleTryKeepTimeGap());
+ result += &format!("_get_CruiseSpeedAtMax: {}, ", self._get_CruiseSpeedAtMax());
+ result += &format!("_get_ObstaclePresent: {}, ", self._get_ObstaclePresent());
+ result += &format!("_get_ObstacleDistance: {}, ", self._get_ObstacleDistance());
+ result += &format!("_get_ObstacleRelativeSpeed: {}, ", self._get_ObstacleRelativeSpeed());
+ result += &format!("_get_ObstacleStatusJustChanged: {}, ", self._get_ObstacleStatusJustChanged());
+ result += &format!("_get_CCInitialisationInProgress: {}, ", self._get_CCInitialisationInProgress());
+ result += &format!("_get_CruiseSpeedChangeInProgress: {}, ", self._get_CruiseSpeedChangeInProgress());
+ result += &format!("_get_NumberOfSetCruise: {}, ", self._get_NumberOfSetCruise());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Cruise_finite1_deterministic {
pub fn new() -> Cruise_finite1_deterministic {
@@ -88,6 +113,8 @@ impl Cruise_finite1_deterministic {
return m;
}
fn init(&mut self) {
+ self._RSset = BSet::new(vec![RSset::RSnone, RSset::RSpos, RSset::RSneg, RSset::RSequal]);
+ self._ODset = BSet::new(vec![ODset::ODnone, ODset::ODclose, ODset::ODveryclose]);
self.CruiseAllowed = BBoolean::new(false);
self.CruiseActive = BBoolean::new(false);
self.VehicleAtCruiseSpeed = BBoolean::new(false);
@@ -103,75 +130,73 @@ impl Cruise_finite1_deterministic {
self.CruiseSpeedChangeInProgress = BBoolean::new(false);
self.ObstaclePresent = BBoolean::new(false);
self.ObstacleRelativeSpeed = RSset::RSnone;
- self._RSset = BSet::new(vec![RSset::RSnone, RSset::RSpos, RSset::RSneg, RSset::RSequal]);
- self._ODset = BSet::new(vec![ODset::ODnone, ODset::ODclose, ODset::ODveryclose]);
}
- pub fn get_CruiseAllowed(&self) -> BBoolean {
+ pub fn _get_CruiseAllowed(&self) -> BBoolean {
return self.CruiseAllowed.clone();
}
- pub fn get_CruiseActive(&self) -> BBoolean {
+ pub fn _get_CruiseActive(&self) -> BBoolean {
return self.CruiseActive.clone();
}
- pub fn get_VehicleAtCruiseSpeed(&self) -> BBoolean {
+ pub fn _get_VehicleAtCruiseSpeed(&self) -> BBoolean {
return self.VehicleAtCruiseSpeed.clone();
}
- pub fn get_VehicleCanKeepSpeed(&self) -> BBoolean {
+ pub fn _get_VehicleCanKeepSpeed(&self) -> BBoolean {
return self.VehicleCanKeepSpeed.clone();
}
- pub fn get_VehicleTryKeepSpeed(&self) -> BBoolean {
+ pub fn _get_VehicleTryKeepSpeed(&self) -> BBoolean {
return self.VehicleTryKeepSpeed.clone();
}
- pub fn get_SpeedAboveMax(&self) -> BBoolean {
+ pub fn _get_SpeedAboveMax(&self) -> BBoolean {
return self.SpeedAboveMax.clone();
}
- pub fn get_VehicleTryKeepTimeGap(&self) -> BBoolean {
+ pub fn _get_VehicleTryKeepTimeGap(&self) -> BBoolean {
return self.VehicleTryKeepTimeGap.clone();
}
- pub fn get_CruiseSpeedAtMax(&self) -> BBoolean {
+ pub fn _get_CruiseSpeedAtMax(&self) -> BBoolean {
return self.CruiseSpeedAtMax.clone();
}
- pub fn get_ObstaclePresent(&self) -> BBoolean {
+ pub fn _get_ObstaclePresent(&self) -> BBoolean {
return self.ObstaclePresent.clone();
}
- pub fn get_ObstacleDistance(&self) -> ODset {
+ pub fn _get_ObstacleDistance(&self) -> ODset {
return self.ObstacleDistance.clone();
}
- pub fn get_ObstacleRelativeSpeed(&self) -> RSset {
+ pub fn _get_ObstacleRelativeSpeed(&self) -> RSset {
return self.ObstacleRelativeSpeed.clone();
}
- pub fn get_ObstacleStatusJustChanged(&self) -> BBoolean {
+ pub fn _get_ObstacleStatusJustChanged(&self) -> BBoolean {
return self.ObstacleStatusJustChanged.clone();
}
- pub fn get_CCInitialisationInProgress(&self) -> BBoolean {
+ pub fn _get_CCInitialisationInProgress(&self) -> BBoolean {
return self.CCInitialisationInProgress.clone();
}
- pub fn get_CruiseSpeedChangeInProgress(&self) -> BBoolean {
+ pub fn _get_CruiseSpeedChangeInProgress(&self) -> BBoolean {
return self.CruiseSpeedChangeInProgress.clone();
}
- pub fn get_NumberOfSetCruise(&self) -> BInteger {
+ pub fn _get_NumberOfSetCruise(&self) -> BInteger {
return self.NumberOfSetCruise.clone();
}
- pub fn get__RSset(&self) -> BSet<RSset> {
+ pub fn _get__RSset(&self) -> BSet<RSset> {
return self._RSset.clone();
}
- pub fn get__ODset(&self) -> BSet<ODset> {
+ pub fn _get__ODset(&self) -> BSet<ODset> {
return self._ODset.clone();
}
@@ -203,6 +228,7 @@ impl Cruise_finite1_deterministic {
}
pub fn SetCruiseSpeed(&mut self, mut vcks: BBoolean, mut csam: BBoolean) -> () {
+ //pre_assert
if (self.CruiseAllowed.equal(&BBoolean::new(true))).booleanValue() {
let mut _ld_NumberOfSetCruise = self.NumberOfSetCruise.clone();
let mut _ld_CruiseActive = self.CruiseActive.clone();
@@ -222,23 +248,26 @@ impl Cruise_finite1_deterministic {
}
if (_ld_NumberOfSetCruise.less(&BInteger::new(1))).booleanValue() {
self.NumberOfSetCruise = _ld_NumberOfSetCruise.plus(&BInteger::new(1));
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
+
}
pub fn CCInitialisationFinished(&mut self, mut vtks: BBoolean, mut vtktg: BBoolean) -> () {
+ //pre_assert
if (self.CCInitialisationInProgress.equal(&BBoolean::new(true))).booleanValue() {
self.VehicleTryKeepTimeGap = vtktg;
self.VehicleTryKeepSpeed = vtks;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
+
}
pub fn CCInitialisationDelayFinished(&mut self) -> () {
- if (self.CCInitialisationInProgress.equal(&BBoolean::new(true)).and(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).or(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))).or(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))).or(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&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!");
@@ -246,7 +275,7 @@ impl Cruise_finite1_deterministic {
}
pub fn CruiseSpeedChangeFinished(&mut self, mut vtks: BBoolean, mut vtktg: BBoolean) -> () {
- if (butils::BOOL.elementOf(&vtks).and(&butils::BOOL.elementOf(&vtktg)).and(&vtks.equal(&BBoolean::new(true)).or(&vtktg.equal(&BBoolean::new(true))).or(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))).or(&self.CCInitialisationInProgress.equal(&BBoolean::new(true)))).and(&self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleDistance.equal(&ODset::ODnone).implies(&vtks.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&vtks.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSequal).and(&self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSneg).and(&self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&vtktg.equal(&BBoolean::new(false))))).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()))).booleanValue() {
if (self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true))).booleanValue() {
self.VehicleTryKeepTimeGap = vtktg;
self.VehicleTryKeepSpeed = vtks;
@@ -259,7 +288,7 @@ impl Cruise_finite1_deterministic {
}
pub fn CruiseSpeedChangeDelayFinished(&mut self) -> () {
- if (self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)).and(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).or(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))).or(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))).or(&self.CCInitialisationInProgress.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).and(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false))).and(&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!");
@@ -293,7 +322,7 @@ impl Cruise_finite1_deterministic {
}
pub fn ExternalForcesBecomesNormal(&mut self) -> () {
- if (self.CruiseActive.equal(&BBoolean::new(true)).and(&self.VehicleCanKeepSpeed.equal(&BBoolean::new(false)))).booleanValue() {
+ if ((self.CruiseActive.equal(&BBoolean::new(true)) && self.VehicleCanKeepSpeed.equal(&BBoolean::new(false)))).booleanValue() {
self.VehicleCanKeepSpeed = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -301,7 +330,7 @@ impl Cruise_finite1_deterministic {
}
pub fn VehicleLeavesCruiseSpeed(&mut self) -> () {
- if (self.VehicleAtCruiseSpeed.equal(&BBoolean::new(true)).and(&self.VehicleCanKeepSpeed.equal(&BBoolean::new(false)).and(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).or(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(false)))).booleanValue() {
+ if (((self.VehicleAtCruiseSpeed.equal(&BBoolean::new(true)) && (self.VehicleCanKeepSpeed.equal(&BBoolean::new(false)) && self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))) || self.VehicleTryKeepSpeed.equal(&BBoolean::new(false)))).booleanValue() {
self.VehicleAtCruiseSpeed = BBoolean::new(false);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -309,7 +338,7 @@ impl Cruise_finite1_deterministic {
}
pub fn VehicleReachesCruiseSpeed(&mut self) -> () {
- if (self.CruiseActive.equal(&BBoolean::new(true)).and(&self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false))).and(&self.SpeedAboveMax.equal(&BBoolean::new(false)))).booleanValue() {
+ if (((self.CruiseActive.equal(&BBoolean::new(true)) && self.VehicleAtCruiseSpeed.equal(&BBoolean::new(false))) && self.SpeedAboveMax.equal(&BBoolean::new(false)))).booleanValue() {
self.VehicleAtCruiseSpeed = BBoolean::new(true);
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -317,7 +346,7 @@ impl Cruise_finite1_deterministic {
}
pub fn VehicleExceedsMaxCruiseSpeed(&mut self) -> () {
- if (self.SpeedAboveMax.equal(&BBoolean::new(false)).and(&self.CruiseActive.equal(&BBoolean::new(false)).or(&self.VehicleCanKeepSpeed.equal(&BBoolean::new(false))).or(&self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).not()))).booleanValue() {
+ if ((self.SpeedAboveMax.equal(&BBoolean::new(false)) && ((self.CruiseActive.equal(&BBoolean::new(false)) || self.VehicleCanKeepSpeed.equal(&BBoolean::new(false))) || ((self.ObstacleStatusJustChanged.equal(&BBoolean::new(false)) && self.CCInitialisationInProgress.equal(&BBoolean::new(false))) && self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).not()))).booleanValue() {
self.SpeedAboveMax = BBoolean::new(true);
self.VehicleAtCruiseSpeed = BBoolean::new(false);
} else {
@@ -328,16 +357,16 @@ impl Cruise_finite1_deterministic {
pub fn VehicleFallsBelowMaxCruiseSpeed(&mut self) -> () {
if (self.SpeedAboveMax.equal(&BBoolean::new(true))).booleanValue() {
self.SpeedAboveMax = BBoolean::new(false);
- if (self.CruiseActive.equal(&BBoolean::new(true)).and(&self.CruiseSpeedAtMax.equal(&BBoolean::new(true)))).booleanValue() {
+ if ((self.CruiseActive.equal(&BBoolean::new(true)) && self.CruiseSpeedAtMax.equal(&BBoolean::new(true)))).booleanValue() {
self.VehicleAtCruiseSpeed = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn ObstacleDistanceBecomesVeryClose(&mut self) -> () {
- if (self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSneg))).booleanValue() {
+ if ((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.equal(&RSset::RSneg))).booleanValue() {
self.ObstacleDistance = ODset::ODveryclose;
self.ObstacleStatusJustChanged = BBoolean::new(true);
} else {
@@ -346,19 +375,19 @@ impl Cruise_finite1_deterministic {
}
pub fn ObstacleDistanceBecomesClose(&mut self) -> () {
- if (self.ObstaclePresent.equal(&BBoolean::new(true)).and(&self.CruiseActive.equal(&BBoolean::new(true))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos)).or(&self.ObstacleDistance.equal(&ODset::ODnone).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSneg))))).booleanValue() {
+ if (((self.ObstaclePresent.equal(&BBoolean::new(true)) && self.CruiseActive.equal(&BBoolean::new(true))) && ((self.ObstacleDistance.equal(&ODset::ODveryclose) && self.ObstacleRelativeSpeed.equal(&RSset::RSpos)) || (self.ObstacleDistance.equal(&ODset::ODnone) && self.ObstacleRelativeSpeed.equal(&RSset::RSneg))))).booleanValue() {
self.ObstacleDistance = ODset::ODclose;
self.ObstacleStatusJustChanged = BBoolean::new(true);
if (self.ObstacleRelativeSpeed.equal(&RSset::RSpos)).booleanValue() {
self.VehicleTryKeepTimeGap = BBoolean::new(false);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn ObstacleDistanceBecomesBig(&mut self) -> () {
- if (self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos))).booleanValue() {
+ if ((self.ObstacleDistance.equal(&ODset::ODclose) && self.ObstacleRelativeSpeed.equal(&RSset::RSpos))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
self.ObstacleDistance = ODset::ODnone;
self.VehicleTryKeepTimeGap = BBoolean::new(false);
@@ -368,14 +397,14 @@ impl Cruise_finite1_deterministic {
}
pub fn ObstacleStartsTravelFaster(&mut self) -> () {
- if (self.ObstaclePresent.equal(&BBoolean::new(true)).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSequal))).booleanValue() {
+ if ((self.ObstaclePresent.equal(&BBoolean::new(true)) && self.ObstacleRelativeSpeed.equal(&RSset::RSequal))).booleanValue() {
self.ObstacleRelativeSpeed = RSset::RSpos;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
if (self.ObstacleDistance.unequal(&ODset::ODveryclose)).booleanValue() {
self.VehicleTryKeepTimeGap = BBoolean::new(false);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -386,7 +415,7 @@ impl Cruise_finite1_deterministic {
self.ObstacleRelativeSpeed = RSset::RSequal;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -397,7 +426,7 @@ impl Cruise_finite1_deterministic {
self.ObstacleRelativeSpeed = RSset::RSneg;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -408,14 +437,15 @@ impl Cruise_finite1_deterministic {
self.ObstacleRelativeSpeed = RSset::RSequal;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn ObstacleAppearsWhenCruiseActive(&mut self, mut ors: RSset, mut od: ODset) -> () {
- if (self.ObstaclePresent.equal(&BBoolean::new(false)).and(&self.CruiseActive.equal(&BBoolean::new(true)))).booleanValue() {
+ //pre_assert
+ if ((self.ObstaclePresent.equal(&BBoolean::new(false)) && self.CruiseActive.equal(&BBoolean::new(true)))).booleanValue() {
self.ObstaclePresent = BBoolean::new(true);
self.ObstacleStatusJustChanged = BBoolean::new(true);
self.ObstacleRelativeSpeed = ors;
@@ -426,7 +456,8 @@ impl Cruise_finite1_deterministic {
}
pub fn ObstacleAppearsWhenCruiseInactive(&mut self, mut ors: RSset) -> () {
- if (self.ObstaclePresent.equal(&BBoolean::new(false)).and(&self.CruiseActive.equal(&BBoolean::new(false)))).booleanValue() {
+ //pre_assert
+ if ((self.ObstaclePresent.equal(&BBoolean::new(false)) && self.CruiseActive.equal(&BBoolean::new(false)))).booleanValue() {
self.ObstaclePresent = BBoolean::new(true);
self.ObstacleRelativeSpeed = ors;
self.ObstacleDistance = ODset::ODnone;
@@ -441,7 +472,7 @@ impl Cruise_finite1_deterministic {
self.ObstacleRelativeSpeed = RSset::RSnone;
if (self.CruiseActive.equal(&BBoolean::new(true))).booleanValue() {
self.ObstacleStatusJustChanged = BBoolean::new(true);
- }
+ }
self.ObstacleDistance = ODset::ODnone;
self.VehicleTryKeepTimeGap = BBoolean::new(false);
} else {
@@ -450,7 +481,7 @@ impl Cruise_finite1_deterministic {
}
pub fn VehicleManageObstacle(&mut self, mut vtks: BBoolean, mut vtktg: BBoolean) -> () {
- if (butils::BOOL.elementOf(&vtks).and(&butils::BOOL.elementOf(&vtktg)).and(&vtks.equal(&BBoolean::new(true)).or(&vtktg.equal(&BBoolean::new(true))).or(&self.CCInitialisationInProgress.equal(&BBoolean::new(true))).or(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).and(&self.ObstaclePresent.equal(&BBoolean::new(false)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleDistance.equal(&ODset::ODnone).implies(&vtks.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtktg.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&vtks.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSequal).and(&self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSneg).and(&self.ObstacleDistance.equal(&ODset::ODnone)).implies(&vtktg.equal(&BBoolean::new(false)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).implies(&vtktg.equal(&BBoolean::new(false))))).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()))).booleanValue() {
if (self.ObstacleStatusJustChanged.equal(&BBoolean::new(true))).booleanValue() {
self.VehicleTryKeepTimeGap = vtktg;
self.VehicleTryKeepSpeed = vtks;
@@ -463,7 +494,7 @@ impl Cruise_finite1_deterministic {
}
pub fn ObstacleBecomesOld(&mut self) -> () {
- if (self.ObstacleStatusJustChanged.equal(&BBoolean::new(true)).and(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)).or(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true))).or(&self.CCInitialisationInProgress.equal(&BBoolean::new(true))).or(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODnone).implies(&self.VehicleTryKeepSpeed.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODclose).and(&self.ObstacleRelativeSpeed.unequal(&RSset::RSpos)).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleDistance.equal(&ODset::ODveryclose).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&self.CruiseSpeedChangeInProgress.equal(&BBoolean::new(false))).implies(&self.VehicleTryKeepTimeGap.equal(&BBoolean::new(true)))).and(&self.ObstacleRelativeSpeed.equal(&RSset::RSpos).and(&self.ObstacleDistance.unequal(&ODset::ODveryclose)).and(&self.CCInitialisationInProgress.equal(&BBoolean::new(false))).and(&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!");
diff --git a/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic_exec.rs b/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic_exec.rs
index 12ca1fe5b0387f03203be95113ae0b1b2c1c5f93..acae0bf504e16f67b38b3b7444c4ed05bdeb094a 100644
--- a/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic_exec.rs
+++ b/benchmarks/execution/Rust_Primitives/Cruise_finite1_deterministic_exec.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bobject::BObject;
@@ -9,12 +11,21 @@ mod Cruise_finite1_deterministic;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Cruise_finite1_deterministic_exec {
counter: BInteger,
_Cruise_finite1_deterministic: Cruise_finite1_deterministic::Cruise_finite1_deterministic,
}
+impl fmt::Display for Cruise_finite1_deterministic_exec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Cruise_finite1_deterministic_exec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Cruise_finite1_deterministic_exec {
pub fn new() -> Cruise_finite1_deterministic_exec {
@@ -28,7 +39,7 @@ impl Cruise_finite1_deterministic_exec {
self._Cruise_finite1_deterministic = Cruise_finite1_deterministic::Cruise_finite1_deterministic::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/Lift.rs b/benchmarks/execution/Rust_Primitives/Lift.rs
index d8971ceb5ef8627dad6f7c9d22322e6e8bdcfef9..67cc96450ad6aeeba7c858a1bf0f1dcbfe387866 100644
--- a/benchmarks/execution/Rust_Primitives/Lift.rs
+++ b/benchmarks/execution/Rust_Primitives/Lift.rs
@@ -1,16 +1,28 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Lift {
floor: BInteger,
}
+impl fmt::Display for Lift {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Lift: (".to_owned();
+ result += &format!("_get_floor: {}, ", self._get_floor());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Lift {
pub fn new() -> Lift {
@@ -23,16 +35,21 @@ impl Lift {
self.floor = BInteger::new(0);
}
- pub fn get_floor(&self) -> BInteger {
+ pub fn _get_floor(&self) -> BInteger {
return self.floor.clone();
}
pub fn inc(&mut self) -> () {
+ //pre_assert
self.floor = self.floor.plus(&BInteger::new(1));
+
}
pub fn dec(&mut self) -> () {
+ //pre_assert
self.floor = self.floor.minus(&BInteger::new(1));
+
}
}
+
diff --git a/benchmarks/execution/Rust_Primitives/LiftExec.rs b/benchmarks/execution/Rust_Primitives/LiftExec.rs
index 0006c0f8ae6cac0e9414691bdeda25aa7e63cb4d..d74efb4a7edee631a6737f2b953d2b76f9d6bb56 100644
--- a/benchmarks/execution/Rust_Primitives/LiftExec.rs
+++ b/benchmarks/execution/Rust_Primitives/LiftExec.rs
@@ -1,19 +1,30 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
mod Lift;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct LiftExec {
counter: BInteger,
_Lift: Lift::Lift,
}
+impl fmt::Display for LiftExec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "LiftExec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl LiftExec {
pub fn new() -> LiftExec {
@@ -27,7 +38,7 @@ impl LiftExec {
self._Lift = Lift::Lift::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/Makefile b/benchmarks/execution/Rust_Primitives/Makefile
index cae4c35665d0404a62edd8c5fd42b20cbbbb2b3b..8b76abf51080d10e494182b526b63e93bd158a18 100644
--- a/benchmarks/execution/Rust_Primitives/Makefile
+++ b/benchmarks/execution/Rust_Primitives/Makefile
@@ -6,7 +6,7 @@ all: CAN_BUS_tlc_exec Cruise_finite1_deterministic_exec LiftExec scheduler_deter
OUTPUT ?= runtimes.txt
-CARGO_PROJ_PATH=../../btypes_primitives/src/main/rust/bmachine
+CARGO_PROJ_PATH=../../../btypes_primitives/src/main/rust/bmachine
CARGO_BUILD=cargo build --release --manifest-path $(CARGO_PROJ_PATH)/Cargo.toml
%.main : %.rs
@@ -21,6 +21,10 @@ CARGO_BUILD=cargo build --release --manifest-path $(CARGO_PROJ_PATH)/Cargo.toml
% : clean %.cp
$(CARGO_BUILD)
/usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
+ /usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
+ /usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
+ /usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
+ /usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
clean:
rm -f $(CARGO_PROJ_PATH)/src/*.rs
\ No newline at end of file
diff --git a/benchmarks/execution/Rust_Primitives/Sieve.rs b/benchmarks/execution/Rust_Primitives/Sieve.rs
index c5fb680740a2d6999ccbc3c8bbb896db7e400433..e6ca8dfd0a77bba9f7cfed70fc87a4cfff43ad32 100644
--- a/benchmarks/execution/Rust_Primitives/Sieve.rs
+++ b/benchmarks/execution/Rust_Primitives/Sieve.rs
@@ -1,20 +1,33 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bset::BSet;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Sieve {
numbers: BSet<BInteger>,
cur: BInteger,
limit: BInteger,
}
+impl fmt::Display for Sieve {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Sieve: (".to_owned();
+ result += &format!("_get_numbers: {}, ", self._get_numbers());
+ result += &format!("_get_cur: {}, ", self._get_cur());
+ result += &format!("_get_limit: {}, ", self._get_limit());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Sieve {
pub fn new() -> Sieve {
@@ -29,32 +42,32 @@ impl Sieve {
self.limit = BInteger::new(2000000);
}
- pub fn get_numbers(&self) -> BSet<BInteger> {
+ pub fn _get_numbers(&self) -> BSet<BInteger> {
return self.numbers.clone();
}
- pub fn get_cur(&self) -> BInteger {
+ pub fn _get_cur(&self) -> BInteger {
return self.cur.clone();
}
- pub fn get_limit(&self) -> BInteger {
+ pub fn _get_limit(&self) -> BInteger {
return self.limit.clone();
}
pub fn ComputeNumberOfPrimes(&mut self) -> BInteger {
let mut res: Option<BInteger> = Option::None;
- while (self.cur.greater(&BInteger::new(1)).and(&self.cur.multiply(&self.cur).lessEqual(&self.limit))).booleanValue() {
+ while ((self.cur.greater(&BInteger::new(1)) && self.cur.multiply(&self.cur).lessEqual(&self.limit))).booleanValue() {
if (self.numbers.elementOf(&self.cur)).booleanValue() {
let mut n: Option<BInteger> = Option::None;
let mut set: Option<BSet<BInteger>> = Option::None;
n = Option::Some(self.cur);
- set = Option::Some(BSet::new(vec![]).clone()).clone();
+ set = Option::Some(BSet::<BInteger>::new(vec![]).clone()).clone();
while (n.unwrap().lessEqual(&self.limit.divide(&self.cur))).booleanValue() {
- set = Option::Some(set.unwrap()._union(&BSet::new(vec![self.cur.multiply(&n.unwrap())])).clone()).clone();
+ set = Option::Some(set.unwrap()._union(&BSet::new(vec![self.cur.multiply(&n.unwrap()).clone()])).clone()).clone();
n = Option::Some(n.unwrap().plus(&BInteger::new(1)));
}
self.numbers = self.numbers.difference(&set.unwrap()).clone().clone();
- }
+ }
self.cur = self.cur.plus(&BInteger::new(1));
}
res = Option::Some(self.numbers.card());
diff --git a/benchmarks/execution/Rust_Primitives/TrafficLight.rs b/benchmarks/execution/Rust_Primitives/TrafficLight.rs
index 16221c23f968b270c70cf80ae83051cdd1b7f8a8..824ce24811cd9678eecbf28ac865f64317c57f8c 100644
--- a/benchmarks/execution/Rust_Primitives/TrafficLight.rs
+++ b/benchmarks/execution/Rust_Primitives/TrafficLight.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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::bset::BSet;
use btypes::bobject::BObject;
@@ -9,9 +11,9 @@ use btypes::bobject::BObject;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum colors {
- red,
- redyellow,
- yellow,
+ red,
+ redyellow,
+ yellow,
green
}
impl colors {
@@ -24,22 +26,32 @@ impl Default for colors {
}
impl fmt::Display for colors {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- colors::red => write!(f, "red"),
- colors::redyellow => write!(f, "redyellow"),
- colors::yellow => write!(f, "yellow"),
- colors::green => write!(f, "green"),
- }
+ match *self {
+ colors::red => write!(f, "red"),
+ colors::redyellow => write!(f, "redyellow"),
+ colors::yellow => write!(f, "yellow"),
+ colors::green => write!(f, "green"),
+ }
}
}
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct TrafficLight {
tl_cars: colors,
tl_peds: colors,
_colors: BSet<colors>,
}
+impl fmt::Display for TrafficLight {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "TrafficLight: (".to_owned();
+ result += &format!("_get_tl_cars: {}, ", self._get_tl_cars());
+ result += &format!("_get_tl_peds: {}, ", self._get_tl_peds());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl TrafficLight {
pub fn new() -> TrafficLight {
@@ -49,25 +61,25 @@ impl TrafficLight {
return m;
}
fn init(&mut self) {
+ self._colors = BSet::new(vec![colors::red, colors::redyellow, colors::yellow, colors::green]);
self.tl_cars = colors::red;
self.tl_peds = colors::red;
- self._colors = BSet::new(vec![colors::red, colors::redyellow, colors::yellow, colors::green]);
}
- pub fn get_tl_cars(&self) -> colors {
+ pub fn _get_tl_cars(&self) -> colors {
return self.tl_cars.clone();
}
- pub fn get_tl_peds(&self) -> colors {
+ pub fn _get_tl_peds(&self) -> colors {
return self.tl_peds.clone();
}
- pub fn get__colors(&self) -> BSet<colors> {
+ pub fn _get__colors(&self) -> BSet<colors> {
return self._colors.clone();
}
pub fn cars_ry(&mut self) -> () {
- if (self.tl_cars.equal(&colors::red).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
+ if ((self.tl_cars.equal(&colors::red) && self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::redyellow;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -75,7 +87,7 @@ impl TrafficLight {
}
pub fn cars_y(&mut self) -> () {
- if (self.tl_cars.equal(&colors::green).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
+ if ((self.tl_cars.equal(&colors::green) && self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::yellow;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -83,7 +95,7 @@ impl TrafficLight {
}
pub fn cars_g(&mut self) -> () {
- if (self.tl_cars.equal(&colors::redyellow).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
+ if ((self.tl_cars.equal(&colors::redyellow) && self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::green;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -91,7 +103,7 @@ impl TrafficLight {
}
pub fn cars_r(&mut self) -> () {
- if (self.tl_cars.equal(&colors::yellow).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
+ if ((self.tl_cars.equal(&colors::yellow) && self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::red;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -99,7 +111,7 @@ impl TrafficLight {
}
pub fn peds_r(&mut self) -> () {
- if (self.tl_peds.equal(&colors::green).and(&self.tl_cars.equal(&colors::red))).booleanValue() {
+ if ((self.tl_peds.equal(&colors::green) && self.tl_cars.equal(&colors::red))).booleanValue() {
self.tl_peds = colors::red;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -107,7 +119,7 @@ impl TrafficLight {
}
pub fn peds_g(&mut self) -> () {
- if (self.tl_peds.equal(&colors::red).and(&self.tl_cars.equal(&colors::red))).booleanValue() {
+ if ((self.tl_peds.equal(&colors::red) && self.tl_cars.equal(&colors::red))).booleanValue() {
self.tl_peds = colors::green;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -115,3 +127,4 @@ impl TrafficLight {
}
}
+
diff --git a/benchmarks/execution/Rust_Primitives/TrafficLightExec.rs b/benchmarks/execution/Rust_Primitives/TrafficLightExec.rs
index 12771e03e72a7c4334a171249f7ebbc261cceedf..cce369309e770f1e9c0e4d0da217741c07579b6d 100644
--- a/benchmarks/execution/Rust_Primitives/TrafficLightExec.rs
+++ b/benchmarks/execution/Rust_Primitives/TrafficLightExec.rs
@@ -1,19 +1,30 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
mod TrafficLight;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct TrafficLightExec {
counter: BInteger,
_TrafficLight: TrafficLight::TrafficLight,
}
+impl fmt::Display for TrafficLightExec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "TrafficLightExec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl TrafficLightExec {
pub fn new() -> TrafficLightExec {
@@ -27,7 +38,7 @@ impl TrafficLightExec {
self._TrafficLight = TrafficLight::TrafficLight::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic.rs b/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic.rs
index 56f4f48ee4c80c3ec062f1952e3d971d5d20e4af..a7916cbfec373d35e8e863683efa3b250a1a51bd 100644
--- a/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic.rs
+++ b/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bset::BSet;
@@ -11,19 +13,19 @@ use btypes::btuple::BTuple;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum BLOCKS {
- A,
- B,
- C,
- D,
- E,
- F,
- G,
- H,
- I,
- J,
- K,
- L,
- M,
+ A,
+ B,
+ C,
+ D,
+ E,
+ F,
+ G,
+ H,
+ I,
+ J,
+ K,
+ L,
+ M,
N
}
impl BLOCKS {
@@ -36,36 +38,36 @@ impl Default for BLOCKS {
}
impl fmt::Display for BLOCKS {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- BLOCKS::A => write!(f, "A"),
- BLOCKS::B => write!(f, "B"),
- BLOCKS::C => write!(f, "C"),
- BLOCKS::D => write!(f, "D"),
- BLOCKS::E => write!(f, "E"),
- BLOCKS::F => write!(f, "F"),
- BLOCKS::G => write!(f, "G"),
- BLOCKS::H => write!(f, "H"),
- BLOCKS::I => write!(f, "I"),
- BLOCKS::J => write!(f, "J"),
- BLOCKS::K => write!(f, "K"),
- BLOCKS::L => write!(f, "L"),
- BLOCKS::M => write!(f, "M"),
- BLOCKS::N => write!(f, "N"),
- }
+ match *self {
+ BLOCKS::A => write!(f, "A"),
+ BLOCKS::B => write!(f, "B"),
+ BLOCKS::C => write!(f, "C"),
+ BLOCKS::D => write!(f, "D"),
+ BLOCKS::E => write!(f, "E"),
+ BLOCKS::F => write!(f, "F"),
+ BLOCKS::G => write!(f, "G"),
+ BLOCKS::H => write!(f, "H"),
+ BLOCKS::I => write!(f, "I"),
+ BLOCKS::J => write!(f, "J"),
+ BLOCKS::K => write!(f, "K"),
+ BLOCKS::L => write!(f, "L"),
+ BLOCKS::M => write!(f, "M"),
+ BLOCKS::N => write!(f, "N"),
+ }
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ROUTES {
- R1,
- R2,
- R3,
- R4,
- R5,
- R6,
- R7,
- R8,
- R9,
+ R1,
+ R2,
+ R3,
+ R4,
+ R5,
+ R6,
+ R7,
+ R8,
+ R9,
R10
}
impl ROUTES {
@@ -78,22 +80,22 @@ impl Default for ROUTES {
}
impl fmt::Display for ROUTES {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- ROUTES::R1 => write!(f, "R1"),
- ROUTES::R2 => write!(f, "R2"),
- ROUTES::R3 => write!(f, "R3"),
- ROUTES::R4 => write!(f, "R4"),
- ROUTES::R5 => write!(f, "R5"),
- ROUTES::R6 => write!(f, "R6"),
- ROUTES::R7 => write!(f, "R7"),
- ROUTES::R8 => write!(f, "R8"),
- ROUTES::R9 => write!(f, "R9"),
- ROUTES::R10 => write!(f, "R10"),
- }
+ match *self {
+ ROUTES::R1 => write!(f, "R1"),
+ ROUTES::R2 => write!(f, "R2"),
+ ROUTES::R3 => write!(f, "R3"),
+ ROUTES::R4 => write!(f, "R4"),
+ ROUTES::R5 => write!(f, "R5"),
+ ROUTES::R6 => write!(f, "R6"),
+ ROUTES::R7 => write!(f, "R7"),
+ ROUTES::R8 => write!(f, "R8"),
+ ROUTES::R9 => write!(f, "R9"),
+ ROUTES::R10 => write!(f, "R10"),
+ }
}
}
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Train_1_beebook_deterministic {
LBT: BSet<BLOCKS>,
TRK: BRelation<BLOCKS, BLOCKS>,
@@ -110,6 +112,21 @@ pub struct Train_1_beebook_deterministic {
_ROUTES: BSet<ROUTES>,
}
+impl fmt::Display for Train_1_beebook_deterministic {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Train_1_beebook_deterministic: (".to_owned();
+ result += &format!("_get_LBT: {}, ", self._get_LBT());
+ result += &format!("_get_TRK: {}, ", self._get_TRK());
+ result += &format!("_get_frm: {}, ", self._get_frm());
+ result += &format!("_get_OCC: {}, ", self._get_OCC());
+ result += &format!("_get_resbl: {}, ", self._get_resbl());
+ result += &format!("_get_resrt: {}, ", self._get_resrt());
+ result += &format!("_get_rsrtbl: {}, ", self._get_rsrtbl());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Train_1_beebook_deterministic {
pub fn new() -> Train_1_beebook_deterministic {
@@ -119,137 +136,155 @@ impl Train_1_beebook_deterministic {
return m;
}
fn init(&mut self) {
- 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._BLOCKS = BSet::new(vec![BLOCKS::A, BLOCKS::B, BLOCKS::C, BLOCKS::D, BLOCKS::E, BLOCKS::F, BLOCKS::G, BLOCKS::H, BLOCKS::I, BLOCKS::J, BLOCKS::K, BLOCKS::L, BLOCKS::M, BLOCKS::N]);
self._ROUTES = BSet::new(vec![ROUTES::R1, ROUTES::R2, ROUTES::R3, ROUTES::R4, ROUTES::R5, ROUTES::R6, ROUTES::R7, ROUTES::R8, ROUTES::R9, ROUTES::R10]);
+ self.nxt = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::C)])), BTuple::from_refs(&ROUTES::R2, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R3, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R4, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R5, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R6, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::C, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R7, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R8, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R9, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)])), BTuple::from_refs(&ROUTES::R10, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)]))]);
self.fst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::L), BTuple::from_refs(&ROUTES::R2, &BLOCKS::L), BTuple::from_refs(&ROUTES::R3, &BLOCKS::L), BTuple::from_refs(&ROUTES::R4, &BLOCKS::M), BTuple::from_refs(&ROUTES::R5, &BLOCKS::M), BTuple::from_refs(&ROUTES::R6, &BLOCKS::C), BTuple::from_refs(&ROUTES::R7, &BLOCKS::G), BTuple::from_refs(&ROUTES::R8, &BLOCKS::N), BTuple::from_refs(&ROUTES::R9, &BLOCKS::G), BTuple::from_refs(&ROUTES::R10, &BLOCKS::N)]);
self.lst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::C), BTuple::from_refs(&ROUTES::R2, &BLOCKS::G), BTuple::from_refs(&ROUTES::R3, &BLOCKS::N), BTuple::from_refs(&ROUTES::R4, &BLOCKS::G), BTuple::from_refs(&ROUTES::R5, &BLOCKS::N), BTuple::from_refs(&ROUTES::R6, &BLOCKS::L), BTuple::from_refs(&ROUTES::R7, &BLOCKS::L), BTuple::from_refs(&ROUTES::R8, &BLOCKS::L), BTuple::from_refs(&ROUTES::R9, &BLOCKS::M), BTuple::from_refs(&ROUTES::R10, &BLOCKS::M)]);
- self.nxt = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::C)])), BTuple::from_refs(&ROUTES::R2, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R3, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R4, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R5, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R6, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::C, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R7, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R8, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R9, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)])), BTuple::from_refs(&ROUTES::R10, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)]))]);
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() {
- if (self.nxt.domain().elementOf(&_ic_r_1).and(&self.nxt.functionCall(&_ic_r_1).domain().elementOf(&_ic_b_1).or(&self.nxt.functionCall(&_ic_r_1).range().elementOf(&_ic_b_1)))).booleanValue() {
+ //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)]));
}
}
}
self.rtbl = _ic_set_0;
+ 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> {
+ pub fn _get_fst(&self) -> BRelation<ROUTES, BLOCKS> {
return self.fst.clone();
}
- pub fn get_lst(&self) -> BRelation<ROUTES, BLOCKS> {
+ pub fn _get_lst(&self) -> BRelation<ROUTES, BLOCKS> {
return self.lst.clone();
}
- pub fn get_nxt(&self) -> BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> {
+ pub fn _get_nxt(&self) -> BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> {
return self.nxt.clone();
}
- pub fn get_rtbl(&self) -> BRelation<BLOCKS, ROUTES> {
+ pub fn _get_rtbl(&self) -> BRelation<BLOCKS, ROUTES> {
return self.rtbl.clone();
}
- pub fn get_LBT(&self) -> BSet<BLOCKS> {
+ pub fn _get_LBT(&self) -> BSet<BLOCKS> {
return self.LBT.clone();
}
- pub fn get_TRK(&self) -> BRelation<BLOCKS, BLOCKS> {
+ pub fn _get_TRK(&self) -> BRelation<BLOCKS, BLOCKS> {
return self.TRK.clone();
}
- pub fn get_frm(&self) -> BSet<ROUTES> {
+ pub fn _get_frm(&self) -> BSet<ROUTES> {
return self.frm.clone();
}
- pub fn get_OCC(&self) -> BSet<BLOCKS> {
+ pub fn _get_OCC(&self) -> BSet<BLOCKS> {
return self.OCC.clone();
}
- pub fn get_resbl(&self) -> BSet<BLOCKS> {
+ pub fn _get_resbl(&self) -> BSet<BLOCKS> {
return self.resbl.clone();
}
- pub fn get_resrt(&self) -> BSet<ROUTES> {
+ pub fn _get_resrt(&self) -> BSet<ROUTES> {
return self.resrt.clone();
}
- pub fn get_rsrtbl(&self) -> BRelation<BLOCKS, ROUTES> {
+ pub fn _get_rsrtbl(&self) -> BRelation<BLOCKS, ROUTES> {
return self.rsrtbl.clone();
}
- pub fn get__BLOCKS(&self) -> BSet<BLOCKS> {
+ pub fn _get__BLOCKS(&self) -> BSet<BLOCKS> {
return self._BLOCKS.clone();
}
- pub fn get__ROUTES(&self) -> BSet<ROUTES> {
+ pub fn _get__ROUTES(&self) -> BSet<ROUTES> {
return self._ROUTES.clone();
}
pub fn route_reservation(&mut self, mut r: ROUTES) -> () {
+ //pre_assert
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();
+
}
pub fn route_freeing(&mut self, mut r: ROUTES) -> () {
+ //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();
+
}
pub fn FRONT_MOVE_1(&mut self, mut r: ROUTES) -> () {
+ //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) -> () {
- self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
+ //pre_assert
+ self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b).clone()])).clone().clone();
+
}
pub fn BACK_MOVE_1(&mut self, mut b: BLOCKS) -> () {
+ //pre_assert
let mut _ld_rsrtbl = self.rsrtbl.clone();
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();
+
}
pub fn BACK_MOVE_2(&mut self, mut b: BLOCKS) -> () {
+ //pre_assert
let mut _ld_rsrtbl = self.rsrtbl.clone();
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();
+
}
pub fn point_positionning(&mut self, mut r: ROUTES) -> () {
+ //pre_assert
self.TRK = self.TRK.domainSubstraction(&self.nxt.functionCall(&r).domain()).rangeSubstraction(&self.nxt.functionCall(&r).range())._union(&self.nxt.functionCall(&r)).clone().clone();
+
}
pub fn route_formation(&mut self, mut r: ROUTES) -> () {
- self.frm = self.frm._union(&BSet::new(vec![r])).clone().clone();
+ //pre_assert
+ self.frm = self.frm._union(&BSet::new(vec![r.clone()])).clone().clone();
+
}
}
+
diff --git a/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic_exec.rs b/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic_exec.rs
index 64fb16febc0568de40f4dd8529cf4ecddd59e3b7..7deb42e649369aabfb017beac09d8993602fb772 100644
--- a/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic_exec.rs
+++ b/benchmarks/execution/Rust_Primitives/Train_1_beebook_deterministic_exec.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bobject::BObject;
@@ -9,12 +11,21 @@ mod Train_1_beebook_deterministic;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct Train_1_beebook_deterministic_exec {
counter: BInteger,
_Train_1_beebook_deterministic: Train_1_beebook_deterministic::Train_1_beebook_deterministic,
}
+impl fmt::Display for Train_1_beebook_deterministic_exec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "Train_1_beebook_deterministic_exec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl Train_1_beebook_deterministic_exec {
pub fn new() -> Train_1_beebook_deterministic_exec {
@@ -28,7 +39,7 @@ impl Train_1_beebook_deterministic_exec {
self._Train_1_beebook_deterministic = Train_1_beebook_deterministic::Train_1_beebook_deterministic::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/scheduler_deterministic.rs b/benchmarks/execution/Rust_Primitives/scheduler_deterministic.rs
index 34b71f0f10e76b263a91a805af319cad308d0e34..18149493b7d6b20dc5e4ea9aa8f2c4432350b9b0 100644
--- a/benchmarks/execution/Rust_Primitives/scheduler_deterministic.rs
+++ b/benchmarks/execution/Rust_Primitives/scheduler_deterministic.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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::bset::BSet;
use btypes::bobject::BObject;
@@ -9,8 +11,8 @@ use btypes::bobject::BObject;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum PID {
- process1,
- process2,
+ process1,
+ process2,
process3
}
impl PID {
@@ -23,15 +25,15 @@ impl Default for PID {
}
impl fmt::Display for PID {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- match *self {
- PID::process1 => write!(f, "process1"),
- PID::process2 => write!(f, "process2"),
- PID::process3 => write!(f, "process3"),
- }
+ match *self {
+ PID::process1 => write!(f, "process1"),
+ PID::process2 => write!(f, "process2"),
+ PID::process3 => write!(f, "process3"),
+ }
}
}
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct scheduler_deterministic {
active: BSet<PID>,
_ready: BSet<PID>,
@@ -39,6 +41,17 @@ pub struct scheduler_deterministic {
_PID: BSet<PID>,
}
+impl fmt::Display for scheduler_deterministic {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "scheduler_deterministic: (".to_owned();
+ result += &format!("_get_active: {}, ", self._get_active());
+ result += &format!("_get__ready: {}, ", self._get__ready());
+ result += &format!("_get_waiting: {}, ", self._get_waiting());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl scheduler_deterministic {
pub fn new() -> scheduler_deterministic {
@@ -48,31 +61,31 @@ impl scheduler_deterministic {
return m;
}
fn init(&mut self) {
- self.active = BSet::new(vec![]).clone().clone();
- self._ready = BSet::new(vec![]).clone().clone();
- self.waiting = BSet::new(vec![]).clone().clone();
self._PID = BSet::new(vec![PID::process1, PID::process2, PID::process3]);
+ self.active = BSet::<PID>::new(vec![]).clone().clone();
+ self._ready = BSet::<PID>::new(vec![]).clone().clone();
+ self.waiting = BSet::<PID>::new(vec![]).clone().clone();
}
- pub fn get_active(&self) -> BSet<PID> {
+ pub fn _get_active(&self) -> BSet<PID> {
return self.active.clone();
}
- pub fn get__ready(&self) -> BSet<PID> {
+ pub fn _get__ready(&self) -> BSet<PID> {
return self._ready.clone();
}
- pub fn get_waiting(&self) -> BSet<PID> {
+ pub fn _get_waiting(&self) -> BSet<PID> {
return self.waiting.clone();
}
- pub fn get__PID(&self) -> BSet<PID> {
+ pub fn _get__PID(&self) -> BSet<PID> {
return self._PID.clone();
}
pub fn _new(&mut self, mut pp: PID) -> () {
- if (self._PID.elementOf(&pp).and(&self.active.notElementOf(&pp)).and(&self._ready._union(&self.waiting).notElementOf(&pp))).booleanValue() {
- self.waiting = self.waiting._union(&BSet::new(vec![pp])).clone().clone();
+ if (((self._PID.elementOf(&pp) && self.active.notElementOf(&pp)) && self._ready._union(&self.waiting).notElementOf(&pp))).booleanValue() {
+ self.waiting = self.waiting._union(&BSet::new(vec![pp.clone()])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -80,7 +93,7 @@ impl scheduler_deterministic {
pub fn del(&mut self, mut pp: PID) -> () {
if (self.waiting.elementOf(&pp)).booleanValue() {
- self.waiting = self.waiting.difference(&BSet::new(vec![pp])).clone().clone();
+ self.waiting = self.waiting.difference(&BSet::new(vec![pp.clone()])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
@@ -88,11 +101,11 @@ impl scheduler_deterministic {
pub fn ready(&mut self, mut rr: PID) -> () {
if (self.waiting.elementOf(&rr)).booleanValue() {
- self.waiting = self.waiting.difference(&BSet::new(vec![rr])).clone().clone();
- if (self.active.equal(&BSet::new(vec![]))).booleanValue() {
- self.active = BSet::new(vec![rr]).clone().clone();
+ self.waiting = self.waiting.difference(&BSet::new(vec![rr.clone()])).clone().clone();
+ if (self.active.equal(&BSet::<PID>::new(vec![]))).booleanValue() {
+ self.active = BSet::new(vec![rr.clone()]).clone().clone();
} else {
- self._ready = self._ready._union(&BSet::new(vec![rr])).clone().clone();
+ self._ready = self._ready._union(&BSet::new(vec![rr.clone()])).clone().clone();
}
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
@@ -100,13 +113,14 @@ impl scheduler_deterministic {
}
pub fn swap(&mut self, mut pp: PID) -> () {
- if (self.active.unequal(&BSet::new(vec![]))).booleanValue() {
+ //pre_assert
+ if (self.active.unequal(&BSet::<PID>::new(vec![]))).booleanValue() {
self.waiting = self.waiting._union(&self.active).clone().clone();
- if (self._ready.equal(&BSet::new(vec![]))).booleanValue() {
- self.active = BSet::new(vec![]).clone().clone();
+ if (self._ready.equal(&BSet::<PID>::new(vec![]))).booleanValue() {
+ self.active = BSet::<PID>::new(vec![]).clone().clone();
} else {
- self.active = BSet::new(vec![pp]).clone().clone();
- self._ready = self._ready.difference(&BSet::new(vec![pp])).clone().clone();
+ self.active = BSet::new(vec![pp.clone()]).clone().clone();
+ self._ready = self._ready.difference(&BSet::new(vec![pp.clone()])).clone().clone();
}
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
diff --git a/benchmarks/execution/Rust_Primitives/scheduler_deterministic_exec.rs b/benchmarks/execution/Rust_Primitives/scheduler_deterministic_exec.rs
index 06e9c4cc8794a8a3d2e90f044ba717203119b4d1..8cd310ebb9b3612d18dbcb4648615a8de3b99960 100644
--- a/benchmarks/execution/Rust_Primitives/scheduler_deterministic_exec.rs
+++ b/benchmarks/execution/Rust_Primitives/scheduler_deterministic_exec.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::bobject::BObject;
@@ -9,12 +11,21 @@ mod scheduler_deterministic;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct scheduler_deterministic_exec {
counter: BInteger,
_scheduler_deterministic: scheduler_deterministic::scheduler_deterministic,
}
+impl fmt::Display for scheduler_deterministic_exec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "scheduler_deterministic_exec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl scheduler_deterministic_exec {
pub fn new() -> scheduler_deterministic_exec {
@@ -28,7 +39,7 @@ impl scheduler_deterministic_exec {
self._scheduler_deterministic = scheduler_deterministic::scheduler_deterministic::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
diff --git a/benchmarks/execution/Rust_Primitives/sort_m2_data1000.rs b/benchmarks/execution/Rust_Primitives/sort_m2_data1000.rs
index c9ad06338ba1b19164552418a69b80d59dff58f0..3bc4f4489924957d8604da055713b4c8a68372f8 100644
--- a/benchmarks/execution/Rust_Primitives/sort_m2_data1000.rs
+++ b/benchmarks/execution/Rust_Primitives/sort_m2_data1000.rs
@@ -1,7 +1,9 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
use btypes::brelation::BRelation;
@@ -10,7 +12,7 @@ use btypes::btuple::BTuple;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct sort_m2_data1000 {
j: BInteger,
k: BInteger,
@@ -20,6 +22,18 @@ pub struct sort_m2_data1000 {
n: BInteger,
}
+impl fmt::Display for sort_m2_data1000 {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "sort_m2_data1000: (".to_owned();
+ result += &format!("_get_j: {}, ", self._get_j());
+ result += &format!("_get_k: {}, ", self._get_k());
+ result += &format!("_get_l: {}, ", self._get_l());
+ result += &format!("_get_g: {}, ", self._get_g());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl sort_m2_data1000 {
pub fn new() -> sort_m2_data1000 {
@@ -32,7 +46,8 @@ impl sort_m2_data1000 {
self.n = BInteger::new(1000);
let mut _ic_set_0 = BRelation::<BInteger, BInteger>::new(vec![]);
for _ic_i_1 in BSet::<BInteger>::interval(&BInteger::new(1), &self.n).clone().iter().cloned() {
- _ic_set_0 = _ic_set_0._union(&BRelation::<BInteger, BInteger>::new(vec![BTuple::new(_ic_i_1, BInteger::new(15000).minus(&_ic_i_1))]));
+ //lambda_expression
+ _ic_set_0 = _ic_set_0._union(&BRelation::<BInteger, BInteger>::new(vec![BTuple::new(_ic_i_1.clone(), BInteger::new(15000).minus(&_ic_i_1))]));
}
self.f = _ic_set_0;
@@ -42,32 +57,32 @@ impl sort_m2_data1000 {
self.j = BInteger::new(1);
}
- pub fn get_f(&self) -> BRelation<BInteger, BInteger> {
+ pub fn _get_f(&self) -> BRelation<BInteger, BInteger> {
return self.f.clone();
}
- pub fn get_n(&self) -> BInteger {
+ pub fn _get_n(&self) -> BInteger {
return self.n.clone();
}
- pub fn get_j(&self) -> BInteger {
+ pub fn _get_j(&self) -> BInteger {
return self.j.clone();
}
- pub fn get_k(&self) -> BInteger {
+ pub fn _get_k(&self) -> BInteger {
return self.k.clone();
}
- pub fn get_l(&self) -> BInteger {
+ pub fn _get_l(&self) -> BInteger {
return self.l.clone();
}
- pub fn get_g(&self) -> BRelation<BInteger, BInteger> {
+ pub fn _get_g(&self) -> BRelation<BInteger, BInteger> {
return self.g.clone();
}
pub fn progress(&mut self) -> () {
- if (self.k.unequal(&self.n).and(&self.j.equal(&self.n))).booleanValue() {
+ if ((self.k.unequal(&self.n) && self.j.equal(&self.n))).booleanValue() {
let mut _ld_g = self.g.clone();
let mut _ld_k = self.k.clone();
let mut _ld_l = self.l.clone();
@@ -81,7 +96,7 @@ impl sort_m2_data1000 {
}
pub fn prog1(&mut self) -> () {
- if (self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
+ if (((self.k.unequal(&self.n) && self.j.unequal(&self.n)) && self.g.functionCall(&self.l).lessEqual(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
let mut _ld_j = self.j.clone();
let mut _ld_l = self.l.clone();
self.l = _ld_l;
@@ -92,7 +107,7 @@ impl sort_m2_data1000 {
}
pub fn prog2(&mut self) -> () {
- if (self.k.unequal(&self.n).and(&self.j.unequal(&self.n)).and(&self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
+ if (((self.k.unequal(&self.n) && self.j.unequal(&self.n)) && self.g.functionCall(&self.l).greater(&self.g.functionCall(&self.j.plus(&BInteger::new(1)))))).booleanValue() {
let mut _ld_j = self.j.clone();
self.j = _ld_j.plus(&BInteger::new(1));
self.l = _ld_j.plus(&BInteger::new(1));
@@ -109,3 +124,4 @@ impl sort_m2_data1000 {
}
}
+
diff --git a/benchmarks/execution/Rust_Primitives/sort_m2_data1000_exec.rs b/benchmarks/execution/Rust_Primitives/sort_m2_data1000_exec.rs
index dd63f06a210d4e75151922c9e4fe0f2f820da7b8..12b8dbf488514d92e157f08ea317bb49021290cd 100644
--- a/benchmarks/execution/Rust_Primitives/sort_m2_data1000_exec.rs
+++ b/benchmarks/execution/Rust_Primitives/sort_m2_data1000_exec.rs
@@ -1,20 +1,32 @@
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
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;
mod sort_m2_data1000;
-#[derive(Default, Debug)]
+#[derive(Clone, Default, Debug, Hash, PartialEq, Eq)]
pub struct sort_m2_data1000_exec {
counter: BInteger,
sorted: BInteger,
_sort_m2_data1000: sort_m2_data1000::sort_m2_data1000,
}
+impl fmt::Display for sort_m2_data1000_exec {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut result = "sort_m2_data1000_exec: (".to_owned();
+ result += &format!("_get_counter: {}, ", self._get_counter());
+ result += &format!("_get_sorted: {}, ", self._get_sorted());
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
+}
+
impl sort_m2_data1000_exec {
pub fn new() -> sort_m2_data1000_exec {
@@ -29,11 +41,11 @@ impl sort_m2_data1000_exec {
self._sort_m2_data1000 = sort_m2_data1000::sort_m2_data1000::new();
}
- pub fn get_counter(&self) -> BInteger {
+ pub fn _get_counter(&self) -> BInteger {
return self.counter.clone();
}
- pub fn get_sorted(&self) -> BInteger {
+ pub fn _get_sorted(&self) -> BInteger {
return self.sorted.clone();
}