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

forwarded master-fixes, added benchmark tests

parent b175e682
No related branches found
No related tags found
1 merge request!28Rust support
Showing
with 92 additions and 37 deletions
...@@ -386,7 +386,7 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> { ...@@ -386,7 +386,7 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> {
pub fn isTotalNatural1(&self) -> BBoolean { return BBoolean::new(false); } pub fn isTotalNatural1(&self) -> BBoolean { return BBoolean::new(false); }
pub fn isTotalString(&self) -> BBoolean { return BBoolean::new(false); } pub fn isTotalString(&self) -> BBoolean { return BBoolean::new(false); }
pub fn isTotalStruct(&self) -> BBoolean { return BBoolean::new(false); } pub fn isTotalStruct(&self) -> BBoolean { return BBoolean::new(false); }
pub fn isPartial(&self, domain: &BSet<L>) -> BBoolean { return self.domain().strictSubset(domain); } pub fn isPartial(&self, domain: &BSet<L>) -> BBoolean { return self.domain().subset(domain); }
pub fn checkDomain(&self, domain: &BSet<L>) -> BBoolean { return self.domain().subset(domain); } pub fn checkDomain(&self, domain: &BSet<L>) -> BBoolean { return self.domain().subset(domain); }
pub fn checkRange(&self, range: &BSet<R>) -> BBoolean { return self.range().subset(range); } pub fn checkRange(&self, range: &BSet<R>) -> BBoolean { return self.range().subset(range); }
......
...@@ -343,9 +343,16 @@ lambda_function_call(arg1, arg2, fromOtherMachine, otherMachine) ::= << ...@@ -343,9 +343,16 @@ lambda_function_call(arg1, arg2, fromOtherMachine, otherMachine) ::= <<
<if(fromOtherMachine)><otherMachine>.<endif><arg1>(<arg2; separator=", ">) <if(fromOtherMachine)><otherMachine>.<endif><arg1>(<arg2; separator=", ">)
>> >>
quantified_predicate(identifier, forall, predicate) ::= << quantified_predicate(identifier, forall, hasCondition, conditionalPredicate, predicate) ::= <<
//quantified_predicate
let mut <identifier> = BBoolean::new(<if(forall)>true<else>false<endif>); let mut <identifier> = BBoolean::new(<if(forall)>true<else>false<endif>);
<if(hasCondition)>
if <conditionalPredicate>.booleanValue() {
<predicate>
}
<else>
<predicate> <predicate>
<endif>
>> >>
quantified_predicate_evaluation(otherIterationConstructs, identifier, emptyPredicate, predicate, forall) ::= << quantified_predicate_evaluation(otherIterationConstructs, identifier, emptyPredicate, predicate, forall) ::= <<
...@@ -361,9 +368,16 @@ if <if(forall)>!<endif>(<predicate>).booleanValue() { ...@@ -361,9 +368,16 @@ if <if(forall)>!<endif>(<predicate>).booleanValue() {
<endif> <endif>
>> >>
quantified_expression(identifier, identity, setType, evaluation, isInteger) ::= << quantified_expression(identifier, identity, useBigInteger, setType, hasCondition, conditionalPredicate, evaluation, isInteger) ::= <<
//quantified_expression
let mut <identifier> = <if(isInteger)>BInteger::new(<identity>);<else>BSet::\<<setType>\>::new(vec![]);<endif> let mut <identifier> = <if(isInteger)>BInteger::new(<identity>);<else>BSet::\<<setType>\>::new(vec![]);<endif>
<if(hasCondition)>
if <conditionalPredicate>.booleanValue() {
<evaluation> <evaluation>
}
<else>
<evaluation>
<endif>
>> >>
quantified_expression_evaluation(otherIterationConstructs, emptyPredicate, predicate, identifier, operation, expression) ::= << quantified_expression_evaluation(otherIterationConstructs, emptyPredicate, predicate, identifier, operation, expression) ::= <<
...@@ -591,10 +605,13 @@ any_body(otherIterationConstructs, emptyPredicate, predicate, body) ::= << ...@@ -591,10 +605,13 @@ any_body(otherIterationConstructs, emptyPredicate, predicate, body) ::= <<
<otherIterationConstructs> <otherIterationConstructs>
<if(emptyPredicate)> <if(emptyPredicate)>
<body> <body>
break;
<else> <else>
if (<predicate>).booleanValue() { if (<predicate>).booleanValue() {
<body> <body>
}<endif> break;
}
<endif>
>> >>
becomes_such_that(loads, body) ::= << becomes_such_that(loads, body) ::= <<
...@@ -1119,6 +1136,7 @@ pub fn _tr_<operationName>(&mut self, is_caching: bool) -> <if(noParameters)>boo ...@@ -1119,6 +1136,7 @@ pub fn _tr_<operationName>(&mut self, is_caching: bool) -> <if(noParameters)>boo
<combination> <combination>
} }
<else> <else>
//transition, parameters, no condidtion
<combination> <combination>
<endif> <endif>
self._tr_cache_<operationName> = Option::Some(<identifier>.clone()); self._tr_cache_<operationName> = Option::Some(<identifier>.clone());
......
package de.hhu.stups.codegenerator.rust;
import org.junit.Test;
public class TestMCBenchmarks extends TestRS {
@Test
public void testCanBusMC() throws Exception {
testRSMC("CAN_BUS_tlc");
}
@Test
public void testCruiseControllerDeterministic_MC() throws Exception {
testRSMC("Cruise_finite1_deterministic_MC");
}
@Test
public void testLandingGear_MC() throws Exception {
testRSMC("landing_gear/LandingGear_R6");
}
@Test
public void testLift_MC() throws Exception {
testRSMC("Lift_MC_Large");
}
@Test
public void testNotaV2_MC() throws Exception {
testRSMC("nota_v2");
}
@Test
public void testQueens4_MC() throws Exception {
testRSMC("QueensWithEvents_4");
}
@Test
public void testQueens8_MC() throws Exception {
testRSMC("QueensWithEvents_8");
}
@Test
public void testsort_m2_data1000_MC() throws Exception {
testRSMC("sort_m2_data1000_MC");
}
@Test
public void testTrain1_Lukas_POR() throws Exception {
testRSMC("Train1_Lukas_POR");
}
@Test
public void testTrain_1_beebook_deterministic_MC_POR() throws Exception {
testRSMC("Train_1_beebook_deterministic_MC_POR", false);
}
}
...@@ -110,11 +110,6 @@ public class TestMachines extends TestRS { ...@@ -110,11 +110,6 @@ public class TestMachines extends TestRS {
testRS("Cruise_finite1_deterministic"); testRS("Cruise_finite1_deterministic");
} }
@Test
public void testCruiseControllerDeterministic_MC() throws Exception {
testRSMC("Cruise_finite1_deterministic_MC");
}
@Test @Test
public void testCruiseControllerDeterministicExec() throws Exception { public void testCruiseControllerDeterministicExec() throws Exception {
testRS("Cruise_finite1_deterministic_exec"); testRS("Cruise_finite1_deterministic_exec");
...@@ -145,16 +140,6 @@ public class TestMachines extends TestRS { ...@@ -145,16 +140,6 @@ public class TestMachines extends TestRS {
testRS("CAN_BUS_tlc"); testRS("CAN_BUS_tlc");
} }
@Test
public void testCanBusMC() throws Exception {
testRSMC("CAN_BUS_tlc");
}
@Test
public void testCanBus_testMC() throws Exception {
testRSMC("CAN_BUS_tlc_test");
}
@Test @Test
public void testCanBusTLCExec() throws Exception { public void testCanBusTLCExec() throws Exception {
testRS("CAN_BUS_tlc_exec"); testRS("CAN_BUS_tlc_exec");
...@@ -285,14 +270,4 @@ public class TestMachines extends TestRS { ...@@ -285,14 +270,4 @@ public class TestMachines extends TestRS {
public void testPitmanController_TIME_MC_v4() throws Exception { public void testPitmanController_TIME_MC_v4() throws Exception {
testRS("visualisation/PitmanController_TIME_MC_v4"); testRS("visualisation/PitmanController_TIME_MC_v4");
} }
@Test
public void testLandingGear_MC() throws Exception {
testRSMC("landing_gear/LandingGear_R6");
}
@Test
public void testNotaV2_MC() throws Exception {
testRSMC("nota_v2");
}
} }
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 132598 Number of States: 132598
Number of Transitions: Number of Transitions: 340264
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 1360 Number of States: 1360
Number of Transitions: Number of Transitions: 26149
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL
Number of States: 1000001
Number of Transitions: 2000001
\ No newline at end of file
MODEL CHECKING SUCCESSFUL
Number of States: 3
Number of Transitions: 4
\ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 24636 Number of States: 24636
Number of Transitions: Number of Transitions: 62226
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 1044336 Number of States: 672173
Number of Transitions: Number of Transitions: 2244484
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 131328 Number of States: 131328
Number of Transitions: Number of Transitions: 884369
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 80718 Number of States: 80718
Number of Transitions: Number of Transitions: 1797353
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 500501 Number of States: 500501
Number of Transitions: Number of Transitions: 500502
\ No newline at end of file \ 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