diff --git a/btypes_primitives/src/main/rust/bmachine/Cargo.toml b/btypes_primitives/src/main/rust/bmachine/Cargo.toml
index 148b6bc0a6810d1e851133b9f689a4a399f66f84..f6f90f9dac027d2ae58dae7fe9e9253f69f3562d 100644
--- a/btypes_primitives/src/main/rust/bmachine/Cargo.toml
+++ b/btypes_primitives/src/main/rust/bmachine/Cargo.toml
@@ -15,6 +15,7 @@ btypes = { path = "../btypes" }
[profile.release]
opt-level = 3
+lto = 'thin'
[profile.dev]
opt-level = 0
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml
index 2e001c335dfdca8f0b015957df7c78ed196103d6..7d89e643742a8b570174c885eea349a101d24132 100644
--- a/btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml
+++ b/btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml
@@ -5,11 +5,17 @@ edition = "2018"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+[[bin]]
+name = "bmachine"
+test = false
+bench = false
+
[dependencies]
btypes = { path = "../btypes" }
[profile.release]
opt-level = 3
+lto = 'thin'
panic = "abort"
[profile.dev]
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml
index 030c40e153da903bc2b2ac6a7a5d2c47d118c251..b1af3b74b5a60da4ce92eada1caea0ed8db58af0 100644
--- a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec/Cargo.toml
@@ -19,13 +19,8 @@ default-features = false
features = []
[profile.release]
-#opt-level = 3
panic = "abort"
-#lto = 'fat'
-codegen-units = 1
-debug = true
-lto = true
-opt-level = "s"
+lto = 'thin'
[profile.dev]
opt-level = 0
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml
index df7a8fa938149962c1259983f3f0bec3fb6e61a4..8fa792358f9be97751ba9265ecb898d3777de841 100644
--- a/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_bitvec_mc/Cargo.toml
@@ -12,13 +12,9 @@ dashmap = "~5.1.0"
derivative = "2.2.0"
[profile.release]
-#opt-level = 3
+opt-level = 3
panic = "abort"
-#lto = 'fat'
-codegen-units = 1
-debug = true
-lto = true
-opt-level = "s"
+lto = 'thin'
[profile.dev]
opt-level = 0
diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml
index f3e1f38f53a251b9c6a10844be56f9272469c070..762c19f4211be0b8de460da8e74c7feb60bbe0b2 100644
--- a/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml
@@ -12,13 +12,8 @@ dashmap = "~5.1.0"
derivative = "2.2.0"
[profile.release]
-#opt-level = 3
panic = "abort"
-#lto = 'fat'
-codegen-units = 1
-debug = true
-lto = true
-opt-level = "s"
+lto = 'thin'
[profile.dev]
opt-level = 0
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
index e216cb905ad83b09cdb9befaf83320b1fa0beb6c..0395ee9bc0cf5f1b42f3aec830a4f774b7c48743 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
@@ -56,29 +56,6 @@ where L: SetItem<LS> + RelLeftItem<LS, R, RS, SIZE, REL_SIZE>,
return BRelation { rel: L::idx_to_rel(idx), _p: PhantomData, _p2: PhantomData };
}
}
-/*
-impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> Set<REL_SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
- where L: SetItem<LS> + RelLeftItem<LS, R, RS, REL_SIZE>,
- R: SetItem<RS>{
- type ItemType = L::RelEnum;
-
- fn as_arr(&self) -> [bool; REL_SIZE] {
- todo!()
- }
-
- fn from_arr(arr: [bool; REL_SIZE]) -> Self {
- todo!()
- }
-
- fn contains_idx(&self, idx: usize) -> bool {
- todo!()
- }
-
- fn subset_of(&self, other: &Self) -> bool {
- todo!()
- }
-}
-*/
pub trait RelPowAble<const REL_VARIANTS: usize, const REL_SIZE: usize>: SetItem<REL_VARIANTS> {
fn pow(&self) -> BSet<Self, REL_VARIANTS>;
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
index 8721d88b84582080170013fb81c5feb3ae75d968..794e57bfb9caec20d02bf8be0b7be6715350c8fd 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
@@ -25,6 +25,7 @@ import de.prob.parser.ast.nodes.substitution.VarSubstitutionNode;
import de.prob.parser.ast.nodes.substitution.WhileSubstitutionNode;
import de.prob.parser.ast.types.BType;
import de.prob.parser.ast.types.CoupleType;
+import de.prob.parser.ast.types.DeferredSetElementType;
import de.prob.parser.ast.types.SetType;
import org.antlr.v4.runtime.misc.OrderedHashSet;
import org.stringtemplate.v4.ST;
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.rs b/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.rs
new file mode 100644
index 0000000000000000000000000000000000000000..5da5c7429f5cd2fc44d1832d26ea9bac3eb6e953
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.rs
@@ -0,0 +1,248 @@
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
+//#![no_std] //std is enabled for the generated machine by default, since without it there is no println which makes unit-testing very difficult
+use btypes::{bset, brel};
+use btypes::bset::BSet;
+use btypes::bset::SetItem;
+use btypes::bset::PowSetItem;
+use btypes::bset::PowAble;
+use btypes::bset::NestedSet;
+use btypes::brelation::BRelation;
+use btypes::brelation::RelLeftItem;
+use btypes::brelation::RelPowAble;
+use btypes::bboolean::BBoolean;
+use btypes::bboolean::BBool;
+use btypes::bboolean::BOOL;
+use btypes::binteger::BInteger;
+use btypes::binteger::BInt;
+use btypes::binteger::set_BInteger;
+use btypes::btuple::BTuple;
+
+
+
+
+//set_enum_declaration
+#[derive(Default, Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub enum LIFTS {
+ #[default]
+ Lift1 = 0,
+ Lift2 = 1,
+ Lift3 = 2,
+ Lift4 = 3
+}
+
+impl LIFTS {
+ pub fn equal(&self, other: &LIFTS) -> bool { *self == *other }
+ pub fn unequal(&self, other: &LIFTS) -> bool { *self != *other }
+ pub const fn to_idx(self) -> usize { self as usize }
+ pub fn from_idx(idx: usize) -> Self {
+ match idx {
+ 0 => Self::Lift1,
+ 1 => Self::Lift2,
+ 2 => Self::Lift3,
+ 3 => Self::Lift4,
+ _ => panic!("LIFTS index out of range! {:?}", idx)
+ }
+ }
+}
+
+impl SetItem<4> for LIFTS {
+ fn as_idx(&self) -> usize { self.to_idx() }
+ fn from_idx(idx: usize) -> Self { Self::from_idx(idx) }
+}
+
+type set_LIFTS = BSet<LIFTS, 4>;
+//set_enum_declaration done
+
+//relation_declaration
+#[derive(Default, Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub enum LIFTS_X_LIFTS {
+ #[default]
+ Lift1_Lift1 = 0,
+ Lift1_Lift2 = 1,
+ Lift1_Lift3 = 2,
+ Lift1_Lift4 = 3,
+ Lift2_Lift1 = 4,
+ Lift2_Lift2 = 5,
+ Lift2_Lift3 = 6,
+ Lift2_Lift4 = 7,
+ Lift3_Lift1 = 8,
+ Lift3_Lift2 = 9,
+ Lift3_Lift3 = 10,
+ Lift3_Lift4 = 11,
+ Lift4_Lift1 = 12,
+ Lift4_Lift2 = 13,
+ Lift4_Lift3 = 14,
+ Lift4_Lift4 = 15
+}
+type rel_LIFTS_X_LIFTS = BRelation<LIFTS, { LIFTS::VARIANTS }, LIFTS, { LIFTS::VARIANTS }, 16>;
+//relation_declaration done
+
+
+
+//relation_declaration
+type rel_LIFTS_X_BInteger = BRelation<LIFTS, { LIFTS::VARIANTS }, BInteger, { BInteger::VARIANTS }, 0>;
+//relation_declaration done
+
+
+
+#[derive(Default, Debug)]
+pub struct MultiLift {
+ /*declarations*/ActiveLifts: rel_LIFTS_X_BInteger,
+ InactiveLifts: set_LIFTS,
+ NextActiveLift: rel_LIFTS_X_LIFTS,
+ /*constant_declarations*/LiftOrder: rel_LIFTS_X_BInteger,
+ /*sets*//*set_declaration*/_LIFTS: set_LIFTS,
+}
+
+
+impl MultiLift {
+
+ pub fn new() -> MultiLift {
+ //values: ''
+ let mut m: MultiLift = Default::default();
+ m.init();
+ return m;
+ }
+ fn init(&mut self) {
+ /*set_initializations*///set_initialization
+ self._LIFTS = bset![LIFTS, /*enum_call*/LIFTS::Lift1, /*enum_call*/LIFTS::Lift2, /*enum_call*/LIFTS::Lift3, /*enum_call*/LIFTS::Lift4];
+ /*properties*///constant_initialization
+ self.LiftOrder = brel![rel_LIFTS_X_BInteger, (/*enum_call*/LIFTS::Lift1.clone(), 1.clone()), (/*enum_call*/LIFTS::Lift2.clone(), 2.clone()), (/*enum_call*/LIFTS::Lift3.clone(), 3.clone()), (/*enum_call*/LIFTS::Lift4.clone(), 4.clone())];
+ /*body*/self.ActiveLifts = brel![rel_LIFTS_X_BInteger, (/*enum_call*/LIFTS::Lift1.clone(), 0.clone())].clone().clone();
+ self.InactiveLifts = bset![LIFTS, /*enum_call*/LIFTS::Lift2, /*enum_call*/LIFTS::Lift3, /*enum_call*/LIFTS::Lift4].clone().clone();
+ self.NextActiveLift = brel![rel_LIFTS_X_LIFTS, (/*enum_call*/LIFTS::Lift1.clone(), /*enum_call*/LIFTS::Lift1.clone())].clone().clone();
+ /*includesInitialization*/
+ }
+
+ pub fn get_LiftOrder(&self) -> rel_LIFTS_X_BInteger {
+ return self.LiftOrder.clone();
+ }
+
+ pub fn get_ActiveLifts(&self) -> rel_LIFTS_X_BInteger {
+ return self.ActiveLifts.clone();
+ }
+
+ pub fn get_InactiveLifts(&self) -> set_LIFTS {
+ return self.InactiveLifts.clone();
+ }
+
+ pub fn get_NextActiveLift(&self) -> rel_LIFTS_X_LIFTS {
+ return self.NextActiveLift.clone();
+ }
+
+ pub fn get__LIFTS(&self) -> set_LIFTS {
+ return self._LIFTS.clone();
+ }
+
+ pub fn inc_lift(&mut self, mut l: LIFTS) -> () {
+ //pre_assert
+ self.ActiveLifts = self.ActiveLifts._override_single(l, self.ActiveLifts.functionCall(&l).plus(&1));
+
+ }
+
+ pub fn dec_lift(&mut self, mut l: LIFTS) -> () {
+ //pre_assert
+ self.ActiveLifts = self.ActiveLifts._override_single(l, self.ActiveLifts.functionCall(&l).minus(&1));
+
+ }
+
+ pub fn init_lift(&mut self, mut l: LIFTS) -> () {
+ //pre_assert
+ //any
+ //iteration_construct_assignment
+ let mut _ic_set_0 = set_LIFTS::empty();
+ //iteration_construct_enumeration
+ for _ic_al_1 in self.NextActiveLift.domain().clone().iter() {
+ //set_comprehension_predicate
+ if self.LiftOrder.functionCall(&_ic_al_1).less(&self.LiftOrder.functionCall(&l)) {
+ _ic_set_0 = _ic_set_0.union(&bset![LIFTS, _ic_al_1]);
+ }
+
+ }
+ {
+ let mut _ic_smallerLifts_1 = _ic_set_0;
+ //iteration_construct_assignment
+ let mut _ic_set_1 = set_LIFTS::empty();
+ //iteration_construct_enumeration
+ for _ic_al_1 in self.NextActiveLift.domain().clone().iter() {
+ //set_comprehension_predicate
+ if self.LiftOrder.functionCall(&_ic_al_1).greater(&self.LiftOrder.functionCall(&l)) {
+ _ic_set_1 = _ic_set_1.union(&bset![LIFTS, _ic_al_1]);
+ }
+
+ }
+ {
+ let mut _ic_biggerLifts_1 = _ic_set_1;
+ //any_body
+ let mut _ic_set_2 = set_LIFTS::empty();
+ //iteration_construct_enumeration
+ for _ic_al_1 in self.NextActiveLift.domain().clone().iter() {
+ //set_comprehension_predicate
+ if self.LiftOrder.functionCall(&_ic_al_1).less(&self.LiftOrder.functionCall(&l)) {
+ _ic_set_2 = _ic_set_2.union(&bset![LIFTS, _ic_al_1]);
+ }
+
+ }let mut _ic_set_3 = set_LIFTS::empty();
+ //iteration_construct_enumeration
+ for _ic_al_1 in self.NextActiveLift.domain().clone().iter() {
+ //set_comprehension_predicate
+ if self.LiftOrder.functionCall(&_ic_al_1).greater(&self.LiftOrder.functionCall(&l)) {
+ _ic_set_3 = _ic_set_3.union(&bset![LIFTS, _ic_al_1]);
+ }
+
+ }
+ let mut _ld_InactiveLifts = self.InactiveLifts.clone();
+ self.ActiveLifts = self.ActiveLifts._override_single(l, 0);
+ self.InactiveLifts = _ld_InactiveLifts.difference(&bset![LIFTS, l]).clone().clone();
+ //if
+ if _ic_smallerLifts_1.card().equal(&0) {
+ self.NextActiveLift = self.NextActiveLift._override_single(self.LiftOrder.inverse().functionCall(&self.LiftOrder.relationImage(&_ic_biggerLifts_1)._max()), l);
+ self.NextActiveLift = self.NextActiveLift._override_single(l, self.LiftOrder.inverse().functionCall(&self.LiftOrder.relationImage(&_ic_biggerLifts_1)._min()));
+ } //else
+ else {
+ self.NextActiveLift = self.NextActiveLift._override_single(self.LiftOrder.inverse().functionCall(&self.LiftOrder.relationImage(&_ic_smallerLifts_1)._max()), l);
+ //if
+ if _ic_biggerLifts_1.card().equal(&0) {
+ self.NextActiveLift = self.NextActiveLift._override_single(l, self.LiftOrder.inverse().functionCall(&self.LiftOrder.relationImage(&_ic_smallerLifts_1)._min()));
+ } //else
+ else {
+ self.NextActiveLift = self.NextActiveLift._override_single(l, self.LiftOrder.inverse().functionCall(&self.LiftOrder.relationImage(&_ic_biggerLifts_1)._min()));
+ }
+ }
+
+ }
+ }
+
+ }
+
+ pub fn close_lift(&mut self, mut l: LIFTS) -> () {
+ //pre_assert
+ let mut _ld_InactiveLifts = self.InactiveLifts.clone();
+ let mut _ld_ActiveLifts = self.ActiveLifts.clone();
+ self.ActiveLifts = _ld_ActiveLifts.domainSubstraction(&bset![LIFTS, l]).clone().clone();
+ self.InactiveLifts = _ld_InactiveLifts.union(&bset![LIFTS, l]).clone().clone();
+ //any
+ //iteration_construct_assignment
+ {
+ let mut _ic_l_pred_1 = self.NextActiveLift.inverse().functionCall(&l);
+ //iteration_construct_assignment
+ {
+ let mut _ic_l_succ_1 = self.NextActiveLift.functionCall(&l);
+ //any_body
+ self.NextActiveLift = self.NextActiveLift.difference(&brel![rel_LIFTS_X_LIFTS, (l.clone(), _ic_l_succ_1.clone())]).clone().clone();
+ self.NextActiveLift = self.NextActiveLift._override_single(_ic_l_pred_1, _ic_l_succ_1);
+
+ }
+ }
+
+ }
+
+ pub fn getFloor(&mut self, mut l: LIFTS) -> BInteger {
+ let mut out: Option<BInteger> = Option::None;
+ //pre_assert
+ out = Option::Some(self.ActiveLifts.functionCall(&l));
+
+ return out.unwrap();
+ }
+}
+