diff --git a/benchmarks/model_checking/ProB/Other/Doors.mch b/benchmarks/model_checking/ProB/Other/Doors.mch
index f4b6925341ca1a69112cc70c9b536d128102fd94..76f43190d69aa60ecb8090a6887a248d1a3fab7b 100644
--- a/benchmarks/model_checking/ProB/Other/Doors.mch
+++ b/benchmarks/model_checking/ProB/Other/Doors.mch
@@ -2,8 +2,8 @@ MACHINE           Doors
 
 SETS              DOOR; POSITION = {open, closed}
 
-DEFINITIONS
-                  scope_DOOR == 1..3
+/*DEFINITIONS   // Definitions currently unused in b2program
+                  scope_DOOR == 1..3*/
                   
 VARIABLES         position
 
diff --git a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
index 2680018b8716deff8f20ad27b0f484f7ef949a51..c12262146c5e9c7ee6f87042df547b478404b030 100644
--- a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
@@ -55,7 +55,6 @@ impl<I: BObject> Ord for OrderedHashSet<I> {
     }
 }
 
-//TODO: check if replacing cache with mutex works and does not impact permormance too much
 unsafe impl<T: BObject> Sync for OrderedHashSet<T> {}
 
 impl<I: BObject> PartialEq for OrderedHashSet<I> {
@@ -126,6 +125,11 @@ impl<I: BObject> OrderedHashSet<I> {
         return self.set.remove_min()
     }
 
+    pub fn remove(&mut self, value: &I) -> Option<I> {
+        self.hash_cache.replace(Option::None);
+        return self.set.remove(value);
+    }
+
     pub fn get_min(&self) -> Option<&I> { self.set.get_min() }
     pub fn get_max(&self) -> Option<&I> { self.set.get_max() }
 
diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
index 690f506fc88e39b870a024cf9bb61ddc0cdc41cf..0ae3eebbcea9656044991556cb99f8f8615c02c4 100644
--- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
@@ -365,7 +365,7 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> {
     }
 
     pub fn _override(&self, arg: &BRelation<L, R>) -> BRelation<L, R> {
-        return BRelation { map: arg.map.clone().union(self.map.clone()), hash_cache: RefCell::new(Option::None)}
+        return BRelation { map: self.map.clone().union_with(arg.map.clone(), |_old_val, new_val| new_val), hash_cache: RefCell::new(Option::None)}
     }
 
     pub fn directProduct<ArgR: 'static + BObject>(&self, arg: &BRelation<L, ArgR>) -> BRelation<L, BTuple<R, ArgR>> {
diff --git a/btypes_primitives/src/main/rust/btypes/src/bset.rs b/btypes_primitives/src/main/rust/btypes/src/bset.rs
index ffe05dd2f2df125f5657b9a80c7f940be0ce06b7..a5aa61e0001c374cf1c481e2070d5ac311750446 100644
--- a/btypes_primitives/src/main/rust/btypes/src/bset.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/bset.rs
@@ -315,6 +315,14 @@ impl<T: 'static + BObject> BSet<T> {
         return self.equal(&of.domain());
     }
 
+    pub fn permutate(&self) -> BSet<BRelation<BInteger, T>> {
+        let interval = BSet::<BInteger>::interval(&BInteger::new(1), &self._size());
+        let result = BRelation::cartesianProduct(&interval, self).pow().iter()
+            .filter(|permutation| permutation.isBijection(self))
+            .fold(OrdSet::new(), |acc, e| acc.update(e.clone()));
+        return BSet::fromOrdSet(result);
+    }
+
     //rust specific
     pub fn cartesian<T1: 'static + BObject, T2: 'static + BObject>(set_a: &OrdSet<T1>, set_b: &OrdSet<T2>) -> OrdSet<BTuple<T1, T2>> {
         if set_a.is_empty() || set_b.is_empty() {return OrdSet::<BTuple<T1, T2>>::new();}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 91ba5312e41a58b3429a9bb9ac6684a54699fe7d..64535298305b489a7ecaedde6ecf9faa28448f67 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -418,11 +418,11 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
 >>
 
 set_enumeration(leftType, type, rightType, enums, isRelation) ::= <<
-<if(isRelation)>BRelation<if(!type)>::\<bobject::Dummy, bobject::Dummy><endif><else>BSet<if(!type)>::\<bobject::Dummy><endif><endif>::new(vec![<enums; separator=", ">])
+/*set_enum <leftType>*/<if(isRelation)>BRelation<if(!enums)>::\<<if(!leftType)>Dummy, Dummy<else><leftType>, <rightType><endif>\><endif><else>BSet<if(!enums)>::\<<if(!type)>Dummy<else><type><endif>\><endif><endif>::new(vec![<enums; separator=", ">])
 >>
 
 seq_enumeration(type, elements) ::= <<
-BRelation::new(vec![<elements; separator=", ">])
+/*seq_enum <type>*/BRelation<if(!type)>::\<BInteger, Dummy><endif>::new(vec![<elements; separator=", ">])
 >>
 
 enum_call(machine, class, identifier, isCurrentMachine) ::= <<
@@ -489,7 +489,7 @@ let mut _ld_<name> = <identifier>.clone();
 >>
 
 function_call_range_element(expr, leftType, rightType, arg, val) ::= <<
-<expr>._override(&BRelation::new(vec![BTuple::new(<arg>,<val>)]))
+<expr>._override(&BRelation<if(!leftType)>::\<bobject::Dummy, bobject::Dummy><endif>::new(vec![BTuple::new(<arg>,<val>)]))
 >>
 
 function_call_nested(expr, arg, isNested) ::= <<
@@ -502,7 +502,7 @@ assignments(assignments) ::= <<
 
 nondeterminism(iterationConstruct, leftType, rightType, identifier, modified_identifier, set, isIdentifierLhs, isRecordAccessLhs, arg) ::= <<
 <iterationConstruct; separator="\n">
-<if(isIdentifierLhs)><identifier> = <set>.nondeterminism();<elseif(isRecordAccessLhs)><identifier> = <modified_identifier>.override_<arg>(<set>.nondeterminism());<else><identifier> = <modified_identifier>._override(BRelation::new(BTuple::new(<arg>,<set>.nondeterminism()));<endif>
+<if(isIdentifierLhs)><identifier> = <set>.nondeterminism();<elseif(isRecordAccessLhs)><identifier> = <modified_identifier>.override_<arg>(<set>.nondeterminism());<else><identifier> = <modified_identifier>._override(BRelation<if(!leftType)>::\<bobject::Dummy, bobject::Dummy><endif>::new(BTuple::new(<arg>,<set>.nondeterminism()));<endif>
 >>
 
 type(type, fromOtherMachine, otherMachine) ::= <<
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
index 64d1ee9ccc9c7dd02a03f6c62d4cda084783914b..a4cd83782ca072cd48dc372d4b87c04010ce034e 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
@@ -48,4 +48,24 @@ public class TestOthers extends TestRS{
     public void test_Doors() throws Exception {
         testRSMC("Doors", PROB_OTHER_PATH, true);
     }
+
+    @Test
+    public void test_EqualityLaws() throws Exception {
+        testRSMC("EqualityLaws", PROB_OTHER_PATH, true);
+    }
+
+    @Test
+    public void test_ExplicitChecks() throws Exception {
+        testRSMC("ExplicitChecks", PROB_OTHER_PATH, false);
+    }
+
+    @Test
+    public void test_Fin1Test() throws Exception {
+        testRSMC("Fin1Test", PROB_OTHER_PATH, true, true);
+    }
+
+    @Test
+    public void test_NatRangeLaws() throws Exception {
+        testRSMC("NatRangeLaws", PROB_OTHER_PATH, false);
+    }
 }
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Doors_MC.out b/src/test/resources/de/hhu/stups/codegenerator/Doors_MC.out
index e735a9dd0de7c1dcafc984c0971812ab1e6c2e1b..c1746d138de7e125d249f8b072cd76627c94bc2c 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Doors_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/Doors_MC.out
@@ -1,3 +1,3 @@
 MODEL CHECKING SUCCESSFUL
-Number of States: 7
-Number of Transitions: 49
\ No newline at end of file
+Number of States: 1024
+Number of Transitions: 20480
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws_MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..df50ea0f9b583322b3e53da773527ca64d2ef995
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 1
+Number of Transitions: 1
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_MC.out b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..0c65a207b01b263dbaa322030a52782f3aae0bae
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 1000
+Number of Transitions: 2001
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Fin1Test_MC.out b/src/test/resources/de/hhu/stups/codegenerator/Fin1Test_MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..26fada1f37f0de762ce58b5a83d385e1513ec014
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/Fin1Test_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 1
+Number of Transitions: 0
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws_MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..f3096009b69935a3af6fe787576a325cc3f12af8
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 30
+Number of Transitions: 360
\ No newline at end of file