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 838374c8e1d4622b6f27e2bd7260e4bd0d861c97..4c05e3a8e1d78dd928de4a1375bff46d6ca836ce 100644 --- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs +++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs @@ -350,6 +350,8 @@ impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, for left_idx in 0..LS { for right_idx in 0..RS { if other.rel[left_idx][right_idx] && !self.rel[left_idx][right_idx] { return false; } + // if self/left side contains an element that other/right side does not -> self not subset of other + if self.rel[left_idx][right_idx] && !other.rel[left_idx][right_idx] { return false; } } } return true; 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 index 19823efdb01cce7543e36a1a32bc22d38ae6187a..55d515c0ed996db90838bdde308f14c7bd970950 100644 --- a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java +++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java @@ -18,6 +18,11 @@ public class TestRelation extends TestRSE { testRSE("Range", "RangeAddition.strs"); } + @Test + public void testSubset() throws Exception { + testRSE("RelationSubset", "RelationSubsetAddition.strs"); + } + @Test public void testId() throws Exception { testRSE("Id", "IdAddition.strs"); diff --git a/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.mch b/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.mch new file mode 100644 index 0000000000000000000000000000000000000000..3e513c7a10ca54d3e42737474c2fd2f5afa1f8a9 --- /dev/null +++ b/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.mch @@ -0,0 +1,21 @@ +MACHINE RelationSubset + +SETS FOO = {F1, F2, F3, F4} + +VARIABLES r1, r2, res + +INVARIANT + r1 : FOO <-> FOO + & r2 : FOO <-> FOO + & res : BOOL + +INITIALISATION + r1 := {F1 |-> F2, F3 |-> F2} + ; r2 := {F1 |-> F2, F2 |-> F4, F3 |-> F2, F3 |-> F4} + ; res := FALSE + +OPERATIONS + calculate = BEGIN IF r1 <: r2 THEN res := TRUE ELSE res := FALSE END END; + out <-- getRes = out := res + +END \ No newline at end of file diff --git a/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.out b/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.out new file mode 100644 index 0000000000000000000000000000000000000000..f32a5804e292d30bedf68f62d32fb75d87e99fd9 --- /dev/null +++ b/src/test/resources/de/hhu/stups/codegenerator/RelationSubset.out @@ -0,0 +1 @@ +true \ No newline at end of file diff --git a/src/test/resources/de/hhu/stups/codegenerator/RelationSubsetAddition.strs b/src/test/resources/de/hhu/stups/codegenerator/RelationSubsetAddition.strs new file mode 100644 index 0000000000000000000000000000000000000000..4622805f545627c42eab48b8d47883aaeaa33c16 --- /dev/null +++ b/src/test/resources/de/hhu/stups/codegenerator/RelationSubsetAddition.strs @@ -0,0 +1,5 @@ +fn main() { + let mut machine = RelationSubset::new(); + machine.calculate(); + println!("{}", machine.getRes()); +} \ No newline at end of file