From 6afda26f4bfad3cf387120baa8effd3c7a120375 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Mon, 15 Aug 2022 15:34:08 +0200
Subject: [PATCH] fixed empty Set/Relation typing and added missing permutate
function
---
.../model_checking/ProB/Other/Doors.mch | 4 ++--
.../main/rust/btypes/src/OrderedHashSet.rs | 6 +++++-
.../src/main/rust/btypes/src/brelation.rs | 2 +-
.../src/main/rust/btypes/src/bset.rs | 8 ++++++++
.../hhu/stups/codegenerator/RustTemplate.stg | 8 ++++----
.../stups/codegenerator/rust/TestOthers.java | 20 +++++++++++++++++++
.../de/hhu/stups/codegenerator/Doors_MC.out | 4 ++--
.../stups/codegenerator/EqualityLaws_MC.out | 3 +++
.../stups/codegenerator/ExplicitChecks_MC.out | 3 +++
.../hhu/stups/codegenerator/Fin1Test_MC.out | 3 +++
.../stups/codegenerator/NatRangeLaws_MC.out | 3 +++
11 files changed, 54 insertions(+), 10 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/EqualityLaws_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/Fin1Test_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws_MC.out
diff --git a/benchmarks/model_checking/ProB/Other/Doors.mch b/benchmarks/model_checking/ProB/Other/Doors.mch
index f4b692534..76f43190d 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 2680018b8..c12262146 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 690f506fc..0ae3eebbc 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 ffe05dd2f..a5aa61e00 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 91ba5312e..645352983 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 64d1ee9cc..a4cd83782 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 e735a9dd0..c1746d138 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 000000000..df50ea0f9
--- /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 000000000..0c65a207b
--- /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 000000000..26fada1f3
--- /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 000000000..f3096009b
--- /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
--
GitLab