Skip to content
Snippets Groups Projects
Commit 947fb1f9 authored by Cookiebowser's avatar Cookiebowser
Browse files

started embedded test machine and fixed a thing

parent 5407bab0
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+ 1
− 1
View file @ 947fb1f9
......@@ -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__
}
......
src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
+ 6
− 9
View file @ 947fb1f9
......@@ -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>
>>
......
src/test/resources/de/hhu/stups/codegenerator/embedded/MultiLift.mch 0 → 100644
+ 89
− 0
View file @ 947fb1f9
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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment