fixed bug in brelation

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;

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");

src/test/resources/de/hhu/stups/codegenerator/RelationSubset.mch

+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

src/test/resources/de/hhu/stups/codegenerator/RelationSubset.out

+true
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/RelationSubsetAddition.strs

+fn main() {
+  let mut machine = RelationSubset::new();
+  machine.calculate();
+  println!("{}", machine.getRes());
+}
\ No newline at end of file