From bc5a17ec366255966ea6b1d0470c25599c490af6 Mon Sep 17 00:00:00 2001 From: Cookiebowser <lucas.doering@live.de> Date: Mon, 6 Mar 2023 15:12:30 +0100 Subject: [PATCH] added some relation tests and fixed some stuff also tried to implement some for functions (unsuccesful) --- .../rust_embedded/btypes/src/brelation.rs | 15 +- .../main/rust_embedded/btypes/src/btuple.rs | 13 + .../src/main/rust_embedded/btypes/src/lib.rs | 2 +- .../stups/codegenerator/RustTemplate_e.stg | 4 +- .../rust_embedded/TestRelation.java | 244 ++++++++++++++++++ .../de/hhu/stups/codegenerator/Closure.mch | 6 +- .../de/hhu/stups/codegenerator/Closure1.mch | 6 +- .../hhu/stups/codegenerator/Composition.mch | 6 +- .../hhu/stups/codegenerator/DirectProduct.mch | 6 +- .../de/hhu/stups/codegenerator/Domain.mch | 6 +- .../stups/codegenerator/DomainRestriction.mch | 6 +- .../codegenerator/DomainSubstraction.mch | 6 +- .../codegenerator/DomainSubstraction.out | 2 +- .../de/hhu/stups/codegenerator/Fnc.mch | 6 +- .../de/hhu/stups/codegenerator/Id.mch | 8 +- .../de/hhu/stups/codegenerator/Inverse.mch | 8 +- .../de/hhu/stups/codegenerator/Iterate.mch | 6 +- .../de/hhu/stups/codegenerator/Override.mch | 8 +- .../stups/codegenerator/OverrideAddition.strs | 6 +- .../de/hhu/stups/codegenerator/Range.mch | 6 +- .../stups/codegenerator/RangeRestriction.mch | 6 +- .../RangeRestrictionAddition.strs | 7 +- .../stups/codegenerator/RangeSubstraction.mch | 6 +- .../de/hhu/stups/codegenerator/Rel.mch | 6 +- .../stups/codegenerator/RelationalImage.mch | 6 +- 25 files changed, 356 insertions(+), 45 deletions(-) create mode 100644 btypes_primitives/src/main/rust_embedded/btypes/src/btuple.rs create mode 100644 src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java 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 105a537ac..07b5681ae 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 000000000..6b352e5ed --- /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 3e0bee3a8..e434ff1c6 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 2ca09eae4..e21654393 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 000000000..7c8cb5b20 --- /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 243cacba6..165cf0b3a 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 e4c9ddd5c..b08299c74 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 77761e79e..6fcea1b93 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 e54dd79b1..ad7cb9b8a 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 1bba697ac..034ee5271 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 affe8a4ed..ec92ae995 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 ea284546a..a1b7867e7 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 d8263ee98..e440e5c84 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 7b836e928..25ab0d86c 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 10f57a59d..f241bd291 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 e57d6e65e..2ccd9289d 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 a7b0eae23..6d706d0b7 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 7db1ccbfb..9deab40aa 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 eae483208..60983cf4b 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 fc01122f8..4132c1e0f 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 c84c522d4..caf3d3628 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 26cf1b75d..9d6495520 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 d238ac832..c1091f18e 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 f74143ab5..5d27feb54 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 8ab69e95d..f0f72990b 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 -- GitLab