diff --git a/btypes_primitives/src/main/rust/btypes/src/bset.rs b/btypes_primitives/src/main/rust/btypes/src/bset.rs
index a5aa61e0001c374cf1c481e2070d5ac311750446..6fb0bb483764473e071f72c2fba105c55024e6be 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 64535298305b489a7ecaedde6ecf9faa28448f67..a2416fcad3e0920eda4b474b7e4d5329ea04ebee 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 a4cd83782ca072cd48dc372d4b87c04010ce034e..c2ebe21028fdcd59777ca2dad55c2dc81077bf82 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 0000000000000000000000000000000000000000..68b9681a21d32d03d4fc5e24034cb2cf4af9bf1a
--- /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 0000000000000000000000000000000000000000..9ac059c5f90b2e137eaa724e1d4550bc79b25539
--- /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 0000000000000000000000000000000000000000..9ac059c5f90b2e137eaa724e1d4550bc79b25539
--- /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 0000000000000000000000000000000000000000..953622e10538fa9bec58c14b1461a9f7fa686c62
--- /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