From fcf4ba934be137ebedc3c07e0ee68183dc692d33 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Thu, 18 Aug 2022 15:01:38 +0200
Subject: [PATCH] added more tests and fixed some bugs
---
.../src/main/rust/btypes/src/bset.rs | 5 +++-
.../hhu/stups/codegenerator/RustTemplate.stg | 19 +++++++++---
.../stups/codegenerator/rust/TestOthers.java | 30 +++++++++++++++++++
.../hhu/stups/codegenerator/SetLawsNat_MC.out | 3 ++
.../stups/codegenerator/SetLawsPow2_MC.out | 3 ++
.../hhu/stups/codegenerator/SetLawsPow_MC.out | 3 ++
.../de/hhu/stups/codegenerator/SetLaws_MC.out | 3 ++
7 files changed, 61 insertions(+), 5 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SetLawsNat_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SetLawsPow_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SetLaws_MC.out
diff --git a/btypes_primitives/src/main/rust/btypes/src/bset.rs b/btypes_primitives/src/main/rust/btypes/src/bset.rs
index a5aa61e00..6fb0bb483 100644
--- a/btypes_primitives/src/main/rust/btypes/src/bset.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/bset.rs
@@ -404,6 +404,9 @@ impl<T: 'static + SetLike> BSet<T> {
}
pub fn unary_intersect(&self) -> T {
- return self.iter().fold(T::get_empty(), |result, next| result.intersect(next));
+ match self.iter().cloned().reduce(|result, next| result.intersect(&next)) {
+ Some(v) => return v,
+ None => panic!("Error: inter applied to empty set!"),
+ }
}
}
\ No newline at end of file
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 645352983..a2416fcad 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -307,7 +307,7 @@ for <identifier> in <set>.pow().iter().cloned() {
iteration_construct_subsetneq(otherIterationConstructs, type, identifier, set, body) ::= <<
<otherIterationConstructs>
-for <identifier> in <set>.pow().difference(<set>).iter().cloned() {
+for <identifier> in <set>.pow().iter().filter(|e| e.unequal(&<set>)).cloned() {
<body>
}
>>
@@ -327,15 +327,24 @@ let mut <identifier> = <if(isRelation)>BRelation::\<<leftType>, <rightType>\><el
<comprehension>
>>
-set_comprehension_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, isRelation, leftType, rightType, subType) ::= <<
+set_comprehension_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, isRelation, leftType, rightType, subType, hasCondition, conditionalPredicate) ::= <<
+//set_comprehension_predicate
<otherIterationConstructs>
<if(emptyPredicate)>
<set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>]));
<else>
+<if(hasCondition)>
+if (<conditionalPredicate>).booleanValue() {
+ if (<predicate>).booleanValue() {
+ <set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>]));
+ }
+}
+<else>
if (<predicate>).booleanValue() {
<set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>]));
}
<endif>
+<endif>
>>
lambda(type, identifier, lambda, leftType, rightType) ::= <<
@@ -403,6 +412,7 @@ if <conditionalPredicate>.booleanValue() {
>>
quantified_expression_evaluation(otherIterationConstructs, emptyPredicate, predicate, identifier, operation, expression) ::= <<
+//quantified_expression_evaluation
<otherIterationConstructs>
<if(emptyPredicate)>
<identifier> = <identifier>.<operation>(&<expression>);
@@ -418,11 +428,11 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
>>
set_enumeration(leftType, type, rightType, enums, isRelation) ::= <<
-/*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=", ">])
+/*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![<if(isRelation)><enums; separator=", "><else><enums:{e | <e>.clone()}; separator=", "><endif>])
>>
seq_enumeration(type, elements) ::= <<
-/*seq_enum <type>*/BRelation<if(!type)>::\<BInteger, Dummy><endif>::new(vec![<elements; separator=", ">])
+BRelation<if(!type)>::\<BInteger, Dummy><endif>::new(vec![<elements; separator=", ">])
>>
enum_call(machine, class, identifier, isCurrentMachine) ::= <<
@@ -1103,6 +1113,7 @@ impl fmt::Display for <machine> {
>>
parameter_combination_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, subType) ::= <<
+//parameter_combination_predicate
<otherIterationConstructs>
<if(emptyPredicate)>
<set> = <set>._union(&BSet::new(vec![<element>]));
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 a4cd83782..c2ebe2102 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
@@ -68,4 +68,34 @@ public class TestOthers extends TestRS{
public void test_NatRangeLaws() throws Exception {
testRSMC("NatRangeLaws", PROB_OTHER_PATH, false);
}
+
+ @Test
+ public void test_SetLaws() throws Exception {
+ testRSMC("SetLaws", PROB_OTHER_PATH, true);
+ }
+
+ @Test
+ public void test_SetLawsNat() throws Exception {
+ testRSMC("SetLawsNat", PROB_OTHER_PATH, false);
+ }
+
+ @Test
+ public void test_SetLawsPow() throws Exception {
+ testRSMC("SetLawsPow", PROB_OTHER_PATH, true);
+ }
+
+ @Test
+ public void test_SetLawsPow2() throws Exception {
+ testRSMC("SetLawsPow2", PROB_OTHER_PATH, true);
+ }
+
+ @Test
+ public void test_SetLawsPowPow() throws Exception {
+ testRSMC("SetLawsPowPow", PROB_OTHER_PATH, false);
+ }
+
+ @Test
+ public void test_SetLawsPowPowCart() throws Exception {
+ testRSMC("SetLawsPowPowCart", PROB_OTHER_PATH, false);
+ }
}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat_MC.out
new file mode 100644
index 000000000..68b9681a2
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 4096
+Number of Transitions: 98304
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2_MC.out
new file mode 100644
index 000000000..9ac059c5f
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 4096
+Number of Transitions: 36864
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow_MC.out
new file mode 100644
index 000000000..9ac059c5f
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 4096
+Number of Transitions: 36864
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SetLaws_MC.out
new file mode 100644
index 000000000..953622e10
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SetLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 512
+Number of Transitions: 3840
\ No newline at end of file
--
GitLab