Skip to content
Snippets Groups Projects
Commit fcf4ba93 authored by Cookiebowser's avatar Cookiebowser
Browse files

added more tests and fixed some bugs

parent 6afda26f
Branches
Tags
1 merge request!28Rust support
...@@ -404,6 +404,9 @@ impl<T: 'static + SetLike> BSet<T> { ...@@ -404,6 +404,9 @@ impl<T: 'static + SetLike> BSet<T> {
} }
pub fn unary_intersect(&self) -> 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
...@@ -307,7 +307,7 @@ for <identifier> in <set>.pow().iter().cloned() { ...@@ -307,7 +307,7 @@ for <identifier> in <set>.pow().iter().cloned() {
iteration_construct_subsetneq(otherIterationConstructs, type, identifier, set, body) ::= << iteration_construct_subsetneq(otherIterationConstructs, type, identifier, set, body) ::= <<
<otherIterationConstructs> <otherIterationConstructs>
for <identifier> in <set>.pow().difference(<set>).iter().cloned() { for <identifier> in <set>.pow().iter().filter(|e| e.unequal(&<set>)).cloned() {
<body> <body>
} }
>> >>
...@@ -327,14 +327,23 @@ let mut <identifier> = <if(isRelation)>BRelation::\<<leftType>, <rightType>\><el ...@@ -327,14 +327,23 @@ let mut <identifier> = <if(isRelation)>BRelation::\<<leftType>, <rightType>\><el
<comprehension> <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> <otherIterationConstructs>
<if(emptyPredicate)> <if(emptyPredicate)>
<set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>])); <set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>]));
<else> <else>
<if(hasCondition)>
if (<conditionalPredicate>).booleanValue() {
if (<predicate>).booleanValue() { if (<predicate>).booleanValue() {
<set> = <set>._union(&<if(isRelation)>BRelation::\<<leftType>, <rightType>\><else>BSet::\<<subType>\><endif>::new(vec![<element>])); <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> <endif>
>> >>
...@@ -403,6 +412,7 @@ if <conditionalPredicate>.booleanValue() { ...@@ -403,6 +412,7 @@ if <conditionalPredicate>.booleanValue() {
>> >>
quantified_expression_evaluation(otherIterationConstructs, emptyPredicate, predicate, identifier, operation, expression) ::= << quantified_expression_evaluation(otherIterationConstructs, emptyPredicate, predicate, identifier, operation, expression) ::= <<
//quantified_expression_evaluation
<otherIterationConstructs> <otherIterationConstructs>
<if(emptyPredicate)> <if(emptyPredicate)>
<identifier> = <identifier>.<operation>(&<expression>); <identifier> = <identifier>.<operation>(&<expression>);
...@@ -418,11 +428,11 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= << ...@@ -418,11 +428,11 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
>> >>
set_enumeration(leftType, type, rightType, enums, isRelation) ::= << 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_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) ::= << enum_call(machine, class, identifier, isCurrentMachine) ::= <<
...@@ -1103,6 +1113,7 @@ impl fmt::Display for <machine> { ...@@ -1103,6 +1113,7 @@ impl fmt::Display for <machine> {
>> >>
parameter_combination_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, subType) ::= << parameter_combination_predicate(otherIterationConstructs, set, element, emptyPredicate, predicate, subType) ::= <<
//parameter_combination_predicate
<otherIterationConstructs> <otherIterationConstructs>
<if(emptyPredicate)> <if(emptyPredicate)>
<set> = <set>._union(&BSet::new(vec![<element>])); <set> = <set>._union(&BSet::new(vec![<element>]));
......
...@@ -68,4 +68,34 @@ public class TestOthers extends TestRS{ ...@@ -68,4 +68,34 @@ public class TestOthers extends TestRS{
public void test_NatRangeLaws() throws Exception { public void test_NatRangeLaws() throws Exception {
testRSMC("NatRangeLaws", PROB_OTHER_PATH, false); 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);
}
} }
MODEL CHECKING SUCCESSFUL
Number of States: 4096
Number of Transitions: 98304
\ No newline at end of file
MODEL CHECKING SUCCESSFUL
Number of States: 4096
Number of Transitions: 36864
\ No newline at end of file
MODEL CHECKING SUCCESSFUL
Number of States: 4096
Number of Transitions: 36864
\ No newline at end of file
MODEL CHECKING SUCCESSFUL
Number of States: 512
Number of Transitions: 3840
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment