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 105a537acf6bdeed817cada102479dcceade9ace..07b5681ae97508bdc6134d069553b99cf01f74a8 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
@@ -323,7 +323,6 @@ impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L,
//TODO: directProduct/ParallelProduct maybe?
- //TODO: support const-params in template? maybe compiler can figure them out itself?
pub fn composition<NewR, const NEW_RS: usize, const PARAM_TOTAL: usize, const NEW_TOTAL: usize>(&self, arg: &BRelation<R, RS, NewR, NEW_RS, PARAM_TOTAL>) -> BRelation<L, LS, NewR, NEW_RS, NEW_TOTAL>
where NewR: SetItem<NEW_RS>{
let mut result = BRelation::<L, LS, NewR, NEW_RS, NEW_TOTAL>::empty();
@@ -342,6 +341,8 @@ impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L,
//NewR::ItemType = R; not yet supported in rust, NewR: Set<RS, I = R> might be, but I'd need to rewrite the trait for that and the related code. For now, we assume the code-generator creates correct code (if it wouldn't the code probably wouldn't run anyway...)
let mut result = BRelation::<L, LS, NewR, NEW_RS, NEW_REL_TOTAL>::empty();
for left_idx in 0..LS {
+ let result_set = self.rel[left_idx];
+ if !result_set.contains(&true) { continue; } // dont create mappings to empty set
result.rel[left_idx][NewR::from_arr(self.rel[left_idx]).as_idx()] = true;
}
return result;
@@ -402,7 +403,17 @@ where L: SetItem<LS> {
return result;
}
}
-
+/* // Does not work in stable rust
+impl<L, const LS: usize, R, const RS: usize, const TOTAL: usize, const INNER_RS: usize> BRelation<L, LS, R, RS, TOTAL>
+ where L: SetItem<LS>,
+ R: SetItem<RS> + Set<RS>,
+ R::ItemType: SetItem<INNER_RS>{
+ pub fn rel<const NEWSIZE: usize>(&self) -> BRelation<L, LS, R::ItemType, INNER_RS, NEWSIZE> {
+ let result = BRelation::<L, LS, R::ItemType, R::ItemType::VARIS, NEWSIZE>::empty();
+ return result;
+ }
+}
+*/
#[macro_export]
macro_rules! brel {
($rel_type:ty $( ,$e:expr )* ) => {
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/btuple.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/btuple.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6b352e5ed56da6ff956924e632218100cefdf66c
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/btuple.rs
@@ -0,0 +1,13 @@
+
+
+pub trait BTuple<L, R> {
+ fn projection1(self) -> L;
+ fn projection2(self) -> R;
+}
+
+impl<L, R> BTuple<L, R> for (L, R)
+where L: Clone,
+ R: Clone {
+ fn projection1(self) -> L { self.0.clone() }
+ fn projection2(self) -> R { self.1.clone() }
+}
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/lib.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/lib.rs
index 3e0bee3a8a4e7d44f999678c9795603c7fe859d0..e434ff1c6364bffe2fb998953f6c2fa8e5f9d4f5 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/lib.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/lib.rs
@@ -8,7 +8,7 @@ pub mod binteger;
//pub mod bstruct;
pub mod bset;
//pub mod bstring;
-//pub mod btuple;
+pub mod btuple;
pub mod brelation;
//pub mod butils;
//pub mod orderedhashset;
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 2ca09eae49c557df87a1db99b76de8cf91c56a47..e21654393bf6e6463d77779fb949d1049d50b9e2 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
@@ -589,11 +589,11 @@ projection_tuple(arg, isProjection1) ::= <<
>>
identity(type, arg) ::= <<
-BRelation::\<<type>,<type>\>::identity(&<arg>)
+<relation_type(type, type)>::identity(&<arg>)
>>
cartesian_product(leftName, rightName, arg1, arg2) ::= <<
-rel_<relation_name(leftName, rightName)>::cartesian_product(&<arg1>, &<arg2>)
+<relation_type(leftName, rightName)>::cartesian_product(&<arg1>, &<arg2>)
>>
tuple_create(leftType, rightType, arg1, arg1IsPrivate, arg2, arg2IsPrivate) ::= <<
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java
new file mode 100644
index 0000000000000000000000000000000000000000..7c8cb5b20f46f2f30ee600a9d389c4e185625888
--- /dev/null
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java
@@ -0,0 +1,244 @@
+package de.hhu.stups.codegenerator.rust_embedded;
+
+import org.junit.Test;
+
+import java.io.IOException;
+import java.net.URISyntaxException;
+
+public class TestRelation extends TestRSE {
+ public TestRelation() throws URISyntaxException, IOException {}
+
+ @Test
+ public void testDomain() throws Exception {
+ testRSE("Domain", "DomainAddition.strs");
+ }
+
+ @Test
+ public void testRange() throws Exception {
+ testRSE("Range", "RangeAddition.strs");
+ }
+
+ @Test
+ public void testId() throws Exception {
+ testRSE("Id", "IdAddition.strs");
+ }
+
+ @Test
+ public void testDomainRestriction() throws Exception {
+ testRSE("DomainRestriction", "DomainRestrictionAddition.strs");
+ }
+
+ @Test
+ public void testDomainSubstraction() throws Exception {
+ testRSE("DomainSubstraction", "DomainSubstractionAddition.strs");
+ }
+
+ @Test
+ public void testRangeRestriction() throws Exception {
+ testRSE("RangeRestriction", "RangeRestrictionAddition.strs");
+ }
+
+ @Test
+ public void testRangeSubstraction() throws Exception {
+ testRSE("RangeSubstraction", "RangeSubstractionAddition.strs");
+ }
+
+ @Test
+ public void testInverse() throws Exception {
+ testRSE("Inverse", "InverseAddition.strs");
+ }
+
+ @Test
+ public void testRelationalImage() throws Exception {
+ testRSE("RelationalImage", "RelationalImageAddition.strs");
+ }
+
+ @Test // relational override/ r1<+r2
+ public void testOverride() throws Exception {
+ testRSE("Override", "OverrideAddition.strs");
+ }
+
+ @Test(expected = RuntimeException.class) // SetItem is not implemented for Tuples (yet)
+ public void testDirectProduct() throws Exception {
+ testRSE("DirectProduct", "DirectProductAddition.strs");
+ }
+
+ @Test
+ public void testComposition() throws Exception {
+ testRSE("Composition", "CompositionAddition.strs");
+ }
+
+ @Test(expected = RuntimeException.class) // SetItem is not implemented for Tuples (yet)
+ public void testParallelProduct() throws Exception {
+ testRSE("ParallelProduct", "ParallelProductAddition.strs");
+ }
+
+ @Test(expected = RuntimeException.class) // SetItem is not implemented for Tuples (yet)
+ public void testProjection1() throws Exception {
+ testRSE("Projection1", "Projection1Addition.strs");
+ }
+
+ @Test(expected = RuntimeException.class) // SetItem is not implemented for Tuples (yet)
+ public void testProjection2() throws Exception {
+ testRSE("Projection2", "Projection2Addition.strs");
+ }
+
+ @Test
+ public void testClosure1() throws Exception {
+ testRSE("Closure1", "Closure1Addition.strs");
+ }
+
+ @Test
+ public void testClosure() throws Exception {
+ testRSE("Closure", "ClosureAddition.strs");
+ }
+
+ @Test
+ public void testIterate() throws Exception {
+ testRSE("Iterate", "IterateAddition.strs");
+ }
+
+ @Test
+ public void testFnc() throws Exception {
+ testRSE("Fnc", "FncAddition.strs");
+ }
+
+ @Test(expected = RuntimeException.class) // currently difficult to implement in Rust...
+ public void testRel() throws Exception {
+ testRSE("Rel", "RelAddition.strs");
+ }
+
+
+
+ @Test
+ public void testRelationGeneralizedUnion() throws Exception {
+ testRSE("RelationGeneralizedUnion", "RelationGeneralizedUnionAddition.strs");
+ }
+
+ @Test
+ public void testRelationGeneralizedUnionEmpty() throws Exception {
+ testRSE("RelationGeneralizedUnionEmpty", "RelationGeneralizedUnionEmptyAddition.strs");
+ }
+
+ @Test
+ public void testRelationGeneralizedIntersection() throws Exception {
+ testRSE("RelationGeneralizedIntersection", "RelationGeneralizedIntersectionAddition.strs");
+ }
+
+ @Test
+ public void testRelationGeneralizedIntersectionEmpty() throws Exception {
+ testRSE("RelationGeneralizedIntersectionEmpty", "RelationGeneralizedIntersectionEmptyAddition.strs");
+ }
+
+ @Test
+ public void testFunctionalOverride() throws Exception {
+ testRSE("FunctionalOverride", "FunctionalOverrideAddition.strs");
+ }
+
+ @Test
+ public void testFunctionalOverride2() throws Exception {
+ testRSE("FunctionalOverride2", "FunctionalOverride2Addition.strs");
+ }
+
+ @Test
+ public void testFunctionalOverride3() throws Exception {
+ testRSE("FunctionalOverride3", "FunctionalOverride3Addition.strs");
+ }
+
+ @Test
+ public void testRelationPow() throws Exception {
+ testRSE("RelationPow", "RelationPowAddition.strs");
+ }
+
+ @Test
+ public void testRelationPow1() throws Exception {
+ testRSE("RelationPow1", "RelationPow1Addition.strs");
+ }
+
+ @Test
+ public void testTupleProjection1() throws Exception {
+ testRSE("TupleProjection1", "TupleProjection1Addition.strs");
+ }
+
+ @Test
+ public void testTupleProjection2() throws Exception {
+ testRSE("TupleProjection2", "TupleProjection2Addition.strs");
+ }
+
+
+
+ @Test
+ public void testTake() throws Exception {
+ testRSE("Take", "TakeAddition.strs");
+ }
+
+ @Test
+ public void testAppend() throws Exception {
+ testRSE("Append", "AppendAddition.strs");
+ }
+
+ @Test
+ public void testConc() throws Exception {
+ testRSE("Conc", "ConcAddition.strs");
+ }
+
+ @Test
+ public void testConcat() throws Exception {
+ testRSE("Concat", "ConcatAddition.strs");
+ }
+
+ @Test
+ public void testDrop() throws Exception {
+ testRSE("Drop", "DropAddition.strs");
+ }
+
+ @Test
+ public void testEmptySequence() throws Exception {
+ testRSE("EmptySequence", "EmptySequenceAddition.strs");
+ }
+
+ @Test
+ public void testEnumeratedSequence() throws Exception {
+ testRSE("EnumeratedSequence", null);
+ }
+
+ @Test
+ public void testFirstElementSequence() throws Exception {
+ testRSE("FirstElementSequence", "FirstElementSequenceAddition.strs");
+ }
+
+ @Test
+ public void testFrontSequence() throws Exception {
+ testRSE("FrontSequence", "FrontSequenceAddition.strs");
+ }
+
+ @Test
+ public void testLastElementSequence() throws Exception {
+ testRSE("LastElementSequence", "LastElementSequenceAddition.strs");
+ }
+
+ @Test
+ public void testPrepend() throws Exception {
+ testRSE("Prepend", "PrependAddition.strs");
+ }
+
+ @Test
+ public void testReverse() throws Exception {
+ testRSE("ReverseSequence", "ReverseSequenceAddition.strs");
+ }
+
+ @Test
+ public void testSizeOfSequence() throws Exception {
+ testRSE("SizeOfSequence", null);
+ }
+
+ @Test
+ public void testTailSequence() throws Exception {
+ testRSE("TailSequence", "TailSequenceAddition.strs");
+ }
+
+ @Test
+ public void testSequenceOperateRelation() throws Exception {
+ testRSE("SequenceOperateRelation", "SequenceOperateRelationAddition.strs");
+ }
+}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Closure.mch b/src/test/resources/de/hhu/stups/codegenerator/Closure.mch
index 243cacba6dff1d465a77375e5124728ba117b004..165cf0b3a544ec6680bf6692d45158406daa6e3f 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Closure.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Closure.mch
@@ -1,10 +1,12 @@
MACHINE Closure
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s
-INVARIANT f : INT --> INT & s : INT --> INT
+INVARIANT f : EINT --> EINT & s : EINT --> EINT
-INITIALISATION f := {0|->1, 1|->2, 2|->3}; s := {}
+INITIALISATION f := {ZERO|->ONE, ONE|->TWO, TWO|->THREE}; s := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Closure1.mch b/src/test/resources/de/hhu/stups/codegenerator/Closure1.mch
index e4c9ddd5c7cec9740ce64f7a94c21697c756bb34..b08299c7472bd147920d75f51f1d374c155d7854 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Closure1.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Closure1.mch
@@ -1,10 +1,12 @@
MACHINE Closure1
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s
-INVARIANT f : INT --> INT & s : INT --> INT
+INVARIANT f : EINT --> EINT & s : EINT --> EINT
-INITIALISATION f := {0|->1, 1|->2, 2|->3}; s := {}
+INITIALISATION f := {ZERO|->ONE, ONE|->TWO, TWO|->THREE}; s := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Composition.mch b/src/test/resources/de/hhu/stups/codegenerator/Composition.mch
index 77761e79e21809f015c5c42e079369d2d3af335b..6fcea1b93569ac441ed124f9fe801b9274dba8c8 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Composition.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Composition.mch
@@ -1,10 +1,12 @@
MACHINE Composition
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s, r
-INVARIANT f : INT --> INT & s : INT --> INT & r : INT --> INT
+INVARIANT f : EINT --> EINT & s : EINT --> EINT & r : EINT --> EINT
-INITIALISATION f := {0|->0, 1|->1, 2|->2}; s := {1|->3}; r:= {}
+INITIALISATION f := {ZERO|->ZERO, ONE|->ONE, TWO|->TWO}; s := {ONE|->THREE}; r:= {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/DirectProduct.mch b/src/test/resources/de/hhu/stups/codegenerator/DirectProduct.mch
index e54dd79b10a6199c9f739f7da0d3d54e70bb536d..ad7cb9b8afbe6afbf1481bc317243b1bd900d2a1 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/DirectProduct.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/DirectProduct.mch
@@ -1,10 +1,12 @@
MACHINE DirectProduct
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s, r
-INVARIANT f : INT --> INT & s : INT --> INT & r : INT --> (INT * INT)
+INVARIANT f : EINT --> EINT & s : EINT --> EINT & r : EINT --> (EINT * EINT)
-INITIALISATION f := {0|->0, 1|->1, 2|->2}; s := {1|->3}; r:= {}
+INITIALISATION f := {ZERO|->ZERO, ONE|->ONE, TWO|->TWO}; s := {ONE|->THREE}; r:= {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Domain.mch b/src/test/resources/de/hhu/stups/codegenerator/Domain.mch
index 1bba697ac05518102a96ca14e5007689c033f73a..034ee527165b5c4c7fd9891d1d30a6b6d3d5dae9 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Domain.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Domain.mch
@@ -1,10 +1,12 @@
MACHINE Domain
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : POW(INT * INT) & r : POW(INT)
+INVARIANT f : POW(EINT * EINT) & r : POW(EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/DomainRestriction.mch b/src/test/resources/de/hhu/stups/codegenerator/DomainRestriction.mch
index affe8a4edd0218c8575e4232f1962c348ed1f54a..ec92ae995f08c3cad538bbb384fd50207d2e14c6 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/DomainRestriction.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/DomainRestriction.mch
@@ -1,10 +1,12 @@
MACHINE DomainRestriction
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, g, r
-INVARIANT f : POW(INT * INT) & g : POW(INT) & r : POW(INT*INT)
+INVARIANT f : POW(EINT * EINT) & g : POW(EINT) & r : POW(EINT*EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; g := {1,2}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE), (FIFE |-> SIX)}; g := {ONE,TWO}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.mch b/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.mch
index ea284546a6b0338b583c14fe11100444dd873279..a1b7867e72c836aac1e03c474da60bd01e2d770e 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.mch
@@ -1,10 +1,12 @@
MACHINE DomainSubstraction
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, g, r
-INVARIANT f : POW(INT * INT) & g : POW(INT) & r : POW(INT*INT)
+INVARIANT f : POW(EINT * EINT) & g : POW(EINT) & r : POW(EINT*EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; g := {1,2}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE), (FIFE |-> SIX)}; g := {ONE,TWO}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.out b/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.out
index d8263ee9860594d2806b0dfd1bfd17528b0ba2a4..e440e5c842586965a7fb77deda2eca68612b1f53 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/DomainSubstraction.out
@@ -1 +1 @@
-2
\ No newline at end of file
+3
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Fnc.mch b/src/test/resources/de/hhu/stups/codegenerator/Fnc.mch
index 7b836e928b7b29f2c8aff95f54e3cb3558c81b0c..25ab0d86c33894fbc477a9fb0c7313da459ac2ba 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Fnc.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Fnc.mch
@@ -1,10 +1,12 @@
MACHINE Fnc
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : INT <-> INT & r : INT +-> POW(INT)
+INVARIANT f : EINT <-> EINT & r : EINT +-> POW(EINT)
-INITIALISATION f := {1|->2, 1|->3, 1|->4, 2|->1}; r := {}
+INITIALISATION f := {ONE|->TWO, ONE|->THREE, ONE|->FOUR, TWO|->ONE}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Id.mch b/src/test/resources/de/hhu/stups/codegenerator/Id.mch
index 10f57a59dce915b2846df785347c06709eb4bd62..f241bd29164c65bb0076c7f75374a48390e7b66a 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Id.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Id.mch
@@ -1,14 +1,16 @@
MACHINE Id
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : POW(INT) & r : INT --> INT
+INVARIANT f : POW(EINT) & r : EINT --> EINT
-INITIALISATION f := {1,2,3}; r := {}
+INITIALISATION f := {ONE,TWO,THREE}; r := {}
OPERATIONS
- calculate = BEGIN r := id(f) END;
+ calculate = BEGIN IF id(f)[{TWO}] = {TWO} THEN r := id(f) ELSE r := {} END END;
out <-- getRes = out := card(r)
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Inverse.mch b/src/test/resources/de/hhu/stups/codegenerator/Inverse.mch
index e57d6e65ed6749f9edd74378286b19e6876396e3..2ccd9289d6f3528c79fd9d376f8fc18b2af64730 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Inverse.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Inverse.mch
@@ -1,14 +1,16 @@
MACHINE Inverse
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : POW(INT * INT) & r : POW(INT * INT)
+INVARIANT f : POW(EINT * EINT) & r : POW(EINT * EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; r := {}
OPERATIONS
calculate = BEGIN r := f~ END;
- out <-- getRes = out := card(r)
+ out <-- getRes = out := card(r[{TWO, THREE, FOUR, FIFE}])
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Iterate.mch b/src/test/resources/de/hhu/stups/codegenerator/Iterate.mch
index a7b0eae23b66610edf374f02ac90ae11f82dc8bd..6d706d0b74ca7b65cd2b8f9e0554199622731ee2 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Iterate.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Iterate.mch
@@ -1,10 +1,12 @@
MACHINE Iterate
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s
-INVARIANT f : INT --> INT & s : INT --> INT
+INVARIANT f : EINT --> EINT & s : EINT --> EINT
-INITIALISATION f := {0|->1, 1|->2, 2|->3}; s := {}
+INITIALISATION f := {ZERO|->ONE, ONE|->TWO, TWO|->THREE}; s := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Override.mch b/src/test/resources/de/hhu/stups/codegenerator/Override.mch
index 7db1ccbfb615542d56d045d5821429a0522a664b..9deab40aad05319e46058d0ee55dd5376eee8e34 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Override.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Override.mch
@@ -1,14 +1,16 @@
MACHINE Override
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, s, r
-INVARIANT f : INT --> INT & s : INT --> INT & r : INT --> INT
+INVARIANT f : EINT --> EINT & s : EINT --> EINT & r : EINT --> EINT
-INITIALISATION f := {0|->0, 1|->1, 2|->2}; s := {1|->3}; r:= {}
+INITIALISATION f := {ZERO|->ZERO, ONE|->ONE, TWO|->TWO}; s := {ONE|->THREE}; r:= {}
OPERATIONS
calculate = BEGIN r := r <+ s END;
- out <-- getRes = out := r(1)
+ out <-- getRes = out := r(ONE)
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/OverrideAddition.strs b/src/test/resources/de/hhu/stups/codegenerator/OverrideAddition.strs
index eae48320826e3045c08230a24b318fdf40ba2756..60983cf4b3511ff9ce7ce106930122a0e780942b 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/OverrideAddition.strs
+++ b/src/test/resources/de/hhu/stups/codegenerator/OverrideAddition.strs
@@ -1,5 +1,9 @@
fn main() {
let mut _override = Override::new();
_override.calculate();
- println!("{}", _override.getRes());
+ if _override.getRes().eq(&EINT::THREE) {
+ println!("3");
+ } else {
+ println!("Wrong result!");
+ }
}
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Range.mch b/src/test/resources/de/hhu/stups/codegenerator/Range.mch
index fc01122f8bf6a18cb818debc33c95da5464c4031..4132c1e0fb9d6c6bd0b756edc2349267f4ac9733 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Range.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Range.mch
@@ -1,10 +1,12 @@
MACHINE Range
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : POW(INT * INT) & r : POW(INT)
+INVARIANT f : POW(EINT * EINT) & r : POW(EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/RangeRestriction.mch b/src/test/resources/de/hhu/stups/codegenerator/RangeRestriction.mch
index c84c522d4532f3833ab2a0bfaac546b9b95140d1..caf3d36282fd57e8d254db8d5c483f93c41ce3c3 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/RangeRestriction.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/RangeRestriction.mch
@@ -1,10 +1,12 @@
MACHINE RangeRestriction
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, g, r
-INVARIANT f : POW(INT * INT) & g : POW(INT) & r : POW(INT*INT)
+INVARIANT f : POW(EINT * EINT) & g : POW(EINT) & r : POW(EINT*EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; g := {1,2}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; g := {ONE,TWO}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/RangeRestrictionAddition.strs b/src/test/resources/de/hhu/stups/codegenerator/RangeRestrictionAddition.strs
index 26cf1b75d866a9a5f44c8348509cc4f87224d7e8..9d64955204a2549733ede24744a8dbafe06a3c85 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/RangeRestrictionAddition.strs
+++ b/src/test/resources/de/hhu/stups/codegenerator/RangeRestrictionAddition.strs
@@ -1,5 +1,10 @@
fn main() {
let mut range = RangeRestriction::new();
range.calculate();
- println!("{}", range.getRes());
+ let res = range.getRes();
+ if res.card() == 1 && res.functionCall(&EINT::ONE).eq(&EINT::TWO) {
+ println!("{{(1 |-> 2)}}");
+ } else {
+ println!("Wrong result!");
+ }
}
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/RangeSubstraction.mch b/src/test/resources/de/hhu/stups/codegenerator/RangeSubstraction.mch
index d238ac832c62758bd00c9c337d1fee0510bf88b1..c1091f18e47e7dcf0b5ba8ef67ebb8703520a9b3 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/RangeSubstraction.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/RangeSubstraction.mch
@@ -1,10 +1,12 @@
MACHINE RangeSubstraction
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, g, r
-INVARIANT f : POW(INT * INT) & g : POW(INT) & r : POW(INT*INT)
+INVARIANT f : POW(EINT * EINT) & g : POW(EINT) & r : POW(EINT*EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; g := {1,2}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; g := {ONE,TWO}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Rel.mch b/src/test/resources/de/hhu/stups/codegenerator/Rel.mch
index f74143ab528091a7c0c2d0e728a4739b28029887..5d27feb54001c8e643c51573694dde897af21d25 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Rel.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Rel.mch
@@ -1,10 +1,12 @@
MACHINE Rel
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, r
-INVARIANT f : INT +-> POW(INT) & r : INT <-> INT
+INVARIANT f : EINT +-> POW(EINT) & r : EINT <-> EINT
-INITIALISATION f := {1|->{2,3,4}, 2|->{1}}; r := {}
+INITIALISATION f := {ONE|->{TWO,THREE,FOUR}, TWO|->{ONE}}; r := {}
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/RelationalImage.mch b/src/test/resources/de/hhu/stups/codegenerator/RelationalImage.mch
index 8ab69e95d46409a745c8c6e08cac8acbbe93f81e..f0f72990b5cc017927ffa8d9bf41687158b8e82c 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/RelationalImage.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/RelationalImage.mch
@@ -1,10 +1,12 @@
MACHINE RelationalImage
+SETS EINT = {ZERO, ONE, TWO, THREE, FOUR, FIFE, SIX}
+
VARIABLES f, g, r
-INVARIANT f : POW(INT * INT) & g : POW(INT) & r : POW(INT)
+INVARIANT f : POW(EINT * EINT) & g : POW(EINT) & r : POW(EINT)
-INITIALISATION f := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (4 |-> 5)}; g := {1,2}; r := {}
+INITIALISATION f := {(ONE |-> TWO), (TWO |-> THREE), (THREE |-> FOUR), (FOUR |-> FIFE)}; g := {ONE,TWO}; r := {}
OPERATIONS