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 446f1f6b0a6a8a9b5b90b9dfc6419def299e2deb..838374c8e1d4622b6f27e2bd7260e4bd0d861c97 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
@@ -533,7 +533,7 @@ macro_rules! brel {
{
let mut __temp_gen_rel__ = <$rel_type>::empty();
$(
- __temp_gen_rel__.add_tuple($e.0, $e.1);
+ __temp_gen_rel__.add_tuple(&$e.0, &$e.1);
)*
__temp_gen_rel__
}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
index 61fab5cc48cf004c5e441d578e79d0832441425f..557f430f536c6f542aa22835c9141fb6f5243612 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
@@ -272,20 +272,20 @@ let mut <identifier> = <if(isRelation)><relation_type(leftType, rightType)><else
>>
set_comprehension_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, isRelation, leftType, rightType, subType, hasCondition, conditionalPredicate) ::= <<
-//set_comprehension_predicate TODO: FASTER!
+//set_comprehension_predicate
<otherIterationConstructs>
<if(emptyPredicate)>
-<set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<set_type(subType)><endif>, <element>]);
+<set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<subType><endif>, <element>]);
<else>
<if(hasCondition)>
if <conditionalPredicate> {
if <predicate> {
- <set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<set_type(subType)><endif>, <element>]);
+ <set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<subType><endif>, <element>]);
}
}
<else>
if <predicate> {
- <set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<set_type(subType)><endif>, <element>]);
+ <set> = <set>.union(&<if(isRelation)>brel![<relation_type(leftType, rightType)><else>bset![<subType><endif>, <element>]);
}
<endif>
<endif>
@@ -372,8 +372,7 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
>>
set_enumeration(leftType, type, rightType, relationName, enums, isRelation) ::= <<
-<if(isRelation)>brel![rel_<relationName><if(enums)>, <endif><enums; separator=", ">]
-<else>bset![<type><if(enums)>, <endif><enums; separator=", ">]<endif>
+<if(isRelation)>brel![rel_<relationName><else>bset![<type><endif><if(enums)>, <endif><enums; separator=", ">]
>>
seq_enumeration(type, elements, relationName) ::= <<
@@ -680,7 +679,7 @@ _ => {<then>}
>>
any(body) ::= <<
-/any
+//any
<body>
>>
@@ -689,11 +688,9 @@ any_body(otherIterationConstructs, emptyPredicate, predicate, body) ::= <<
<otherIterationConstructs>
<if(emptyPredicate)>
<body>
-break;
<else>
if <predicate> {
<body>
- break;
}
<endif>
>>
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.mch
new file mode 100644
index 0000000000000000000000000000000000000000..fb3dd257911e2f38da3fc26963457f83cf8473b3
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.mch
@@ -0,0 +1,89 @@
+MACHINE MultiLift
+
+SETS LIFTS = {Lift1, Lift2, Lift3, Lift4}
+
+CONCRETE_CONSTANTS LiftOrder
+
+VARIABLES ActiveLifts, InactiveLifts, NextActiveLift
+
+PROPERTIES
+ LiftOrder : LIFTS --> 1..4
+ & LiftOrder = {Lift1 |-> 1, Lift2 |-> 2, Lift3 |-> 3, Lift4 |-> 4}
+
+INVARIANT
+ ActiveLifts : LIFTS +-> -2..10
+ & card(dom(ActiveLifts)) > 0
+ & InactiveLifts <: LIFTS
+ & LIFTS \ InactiveLifts = dom(ActiveLifts)
+ & NextActiveLift : dom(ActiveLifts) +-> dom(ActiveLifts)
+ // Enforce ordered cycle in NextActiveLift, ie. keep NextActiveLift consistent no matter the insert order.
+ & !(l).((l : dom(ActiveLifts)) => (LiftOrder(l) /= max(LiftOrder[dom(ActiveLifts)]) => LiftOrder(NextActiveLift(l)) = min(LiftOrder[{lift | lift : dom(NextActiveLift) & LiftOrder(lift) > LiftOrder(l)}]) ))
+ & !(l).((l : dom(ActiveLifts)) => (LiftOrder(l) = max(LiftOrder[dom(ActiveLifts)]) => LiftOrder(NextActiveLift(l)) = min(LiftOrder[dom(NextActiveLift)])))
+
+INITIALISATION
+ ActiveLifts := {Lift1 |-> 0}
+ || InactiveLifts := {Lift2, Lift3, Lift4}
+ || NextActiveLift := {Lift1 |-> Lift1}
+
+OPERATIONS
+
+ inc_lift(l) =
+ PRE
+ l : dom(ActiveLifts)
+ & ActiveLifts(l) < 10
+ THEN
+ ActiveLifts(l) := ActiveLifts(l) + 1
+ END;
+
+ dec_lift(l) =
+ PRE
+ l : dom(ActiveLifts)
+ & ActiveLifts(l) > -2
+ THEN
+ ActiveLifts(l) := ActiveLifts(l) - 1
+ END;
+
+ init_lift(l) =
+ PRE
+ l : InactiveLifts
+ THEN
+ LET smallerLifts, biggerLifts BE smallerLifts = {al| al: dom(NextActiveLift) & LiftOrder(al) < LiftOrder(l)} & biggerLifts = {al| al: dom(NextActiveLift) & LiftOrder(al) > LiftOrder(l)}
+ IN
+ ActiveLifts(l) := 0
+ || InactiveLifts := InactiveLifts \ { l }
+ || IF card(smallerLifts) = 0
+ THEN NextActiveLift(LiftOrder~(max(LiftOrder[biggerLifts]))) := l; NextActiveLift(l) := LiftOrder~(min(LiftOrder[biggerLifts])) // if smallerLifts is empty, biggerLifts cannot be empty (since ActiveLifts cannot be empty)
+ ELSE NextActiveLift(LiftOrder~(max(LiftOrder[smallerLifts]))) := l; IF card(biggerLifts) = 0
+ THEN NextActiveLift(l) := LiftOrder~(min(LiftOrder[smallerLifts]))
+ ELSE NextActiveLift(l) := LiftOrder~(min(LiftOrder[biggerLifts]))
+ END
+ END
+ // For some reason, B2Program doesn't like the if here...
+ /*; IF card(biggerLifts) = 0
+ THEN NextActiveLift(l) := LiftOrder~(min(LiftOrder[smallerLifts]))
+ ELSE NextActiveLift(l) := LiftOrder~(min(LiftOrder[biggerLifts]))
+ END*/
+ END
+ END;
+
+ close_lift(l) =
+ PRE
+ l : dom(ActiveLifts)
+ & card(dom(ActiveLifts)) > 1
+ THEN
+ ActiveLifts := {l} <<| ActiveLifts
+ || InactiveLifts := InactiveLifts \/ { l }
+ || LET l_pred, l_succ BE l_pred = NextActiveLift~(l) & l_succ = NextActiveLift(l) IN
+ NextActiveLift := NextActiveLift \ {l |-> l_succ}
+ ; NextActiveLift(l_pred) := l_succ
+ END
+ END;
+
+ out <-- getFloor(l) =
+ PRE
+ l : dom(ActiveLifts)
+ THEN
+ out := ActiveLifts(l)
+ END
+
+END
\ No newline at end of file