Commit f1f34e58 authored by Daniel Ratiu's avatar Daniel Ratiu
Browse files

small fixes

refs 799
parent 351a5120
......@@ -165,13 +165,7 @@
<layoutData xsi:type="org-fortiss-tooling-base-model-layout:Point" key="pos"/>
<layoutData xsi:type="org-fortiss-tooling-base-model-layout:Dimension" key="dim" width="108" height="72"/>
</containedElements>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms atomID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." checkResultStatus="-1">
<placeHolders>P</placeHolders>
<predicates>paced</predicates>
</atoms>
</specifications>
</specifications>
<connectors xsi:type="org-fortiss-af3-component:OutputPort" id="496" name="paced" comment="" outgoing="//@rootElements.1/@containedElements.0/@containedElements.1/@specifications.1/@containedElements.0/@containedElements.0/@specifications.1/@containedElements.0/@connections.0">
<specifications xsi:type="org-fortiss-af3-component:PortSpecification">
<type xsi:type="org-fortiss-af3-expression-types:TBool"/>
......@@ -307,20 +301,6 @@
<layoutData xsi:type="org-fortiss-tooling-base-model-layout:Dimension" key="dim" width="108" height="72"/>
</containedElements>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms atomID="RESPONSE_GLOBALLY" userFriendlyExplanation="'S' Responds to 'P' Globally." lastCheckDate="2012-02-27T13:38:51.233+0100">
<placeHolders>P</placeHolders>
<placeHolders>S</placeHolders>
<predicates>brady == true</predicates>
<predicates>paced == true</predicates>
</atoms>
<atoms atomID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:38:51.311+0100">
<placeHolders>Q</placeHolders>
<placeHolders>P</placeHolders>
<predicates>brady == true</predicates>
<predicates>paced == true</predicates>
</atoms>
</specifications>
<connectors xsi:type="org-fortiss-af3-component:OutputPort" id="540" name="paced" comment="" outgoing="//@rootElements.1/@containedElements.0/@containedElements.1/@specifications.1/@containedElements.0/@containedElements.1/@specifications.1/@containedElements.0/@connections.0">
<specifications xsi:type="org-fortiss-af3-component:PortSpecification">
<type xsi:type="org-fortiss-af3-expression-types:TBool"/>
......@@ -570,20 +550,6 @@
<type xsi:type="org-fortiss-af3-expression-types:TInt"/>
</dataStateVariables>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms atomID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:41:44.316+0100">
<placeHolders>Q</placeHolders>
<placeHolders>P</placeHolders>
<predicates>timer >= 800</predicates>
<predicates>paced == true</predicates>
</atoms>
<atoms atomID="EXISTENCE_BEFORE" userFriendlyExplanation="'P' becomes true Before 'R'." lastCheckDate="2012-02-27T13:41:44.394+0100">
<placeHolders>P</placeHolders>
<placeHolders>R</placeHolders>
<predicates>paced != true</predicates>
<predicates>timer == 800</predicates>
</atoms>
</specifications>
<connectors xsi:type="org-fortiss-af3-component:InputPort" id="552" name="heartBeat" comment="" incoming="//@rootElements.1/@containedElements.0/@containedElements.1/@specifications.1/@containedElements.0/@containedElements.2/@specifications.1/@containedElements.0/@connections.0">
<specifications xsi:type="org-fortiss-af3-component:PortSpecification">
<type xsi:type="org-fortiss-af3-expression-types:TBool"/>
......@@ -962,19 +928,7 @@
<layoutData xsi:type="org-fortiss-tooling-base-model-layout:Dimension" key="dim" width="108" height="72"/>
</containedElements>
</specifications>
<specifications xsi:type="org-fortiss-af3-mira-usecase:ScopeSpecification" reference="3" id="804" name="Ref: 3"/>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms atomID="ABSENCE_BEFORE" userFriendlyExplanation="Property 'P' is false Before 'R'." lastCheckDate="2012-02-27T14:39:35.964+0100">
<placeHolders>P</placeHolders>
<placeHolders>R</placeHolders>
<predicates>paced == true</predicates>
<predicates>user_input != NoVal</predicates>
</atoms>
<atoms atomID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." lastCheckDate="2012-02-27T14:39:36.073+0100">
<placeHolders>P</placeHolders>
<predicates>paced == NoVal</predicates>
</atoms>
</specifications>
<specifications xsi:type="org-fortiss-af3-mira-usecase:ScopeSpecification" reference="3" id="804" name="Ref: 3"/>
<connectors xsi:type="org-fortiss-af3-component:InputPort" id="451" name="user_input" comment="" incoming="//@rootElements.1/@containedElements.0/@connections.0">
<specifications xsi:type="org-fortiss-af3-component:PortSpecification">
<type xsi:type="org-fortiss-af3-expression-types:TDefinedType" name="pacemaker_mode"/>
......
......@@ -30,7 +30,7 @@ import test.org.fortiss.af3.rcp.application.semantic.alignment.nusmv.ModelChecke
* @author ratiu
* @author $Author: mou $
* @version $Rev: 4272 $
* @ConQAT.Rating GREEN Hash: 9B7548593ECCF1437EC806E9891B0A3F
* @ConQAT.Rating YELLOW Hash: 0793C5B57740B0207AD2E936489050C7
*/
// @CodeFormatterOff
@RunWith(Suite.class)
......
......@@ -20,6 +20,7 @@ package test.org.fortiss.af3.rcp.application.semantic.alignment.nusmv;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createStateCoverage;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestSuiteSpecification;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import static org.fortiss.tooling.kernel.utils.KernelModelElementUtils.getParentElement;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.fail;
......@@ -60,7 +61,7 @@ import test.org.fortiss.af3.expression.evaluator.EvaluatorTestData;
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 4076 $
* @ConQAT.Rating YELLOW Hash: DB13082CFBC91487FE9539713C9EBBC7
* @ConQAT.Rating YELLOW Hash: 36FFAC9C1E81933C7C45EF68680F2EEA
*/
@RunWith(Parameterized.class)
public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
......@@ -83,7 +84,7 @@ public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
gen =
new ModelCheckingTestSuiteGenerator(new StatesCoverageAnalyzer(config, specPart),
15000);
120000);
}
/** Test data. */
......@@ -94,6 +95,7 @@ public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
"platform:/plugin/org.fortiss.af3.analyses/test-data/ModelCheckerBasicTests.af3_20",
"platform:/plugin/org.fortiss.af3.rcp.application/test-data/ACC.af3_20",
"platform:/plugin/org.fortiss.af3.rcp.application/test-data/Pacemaker.af3_20",
"platform:/plugin/org.fortiss.af3.rcp.application/test-data/Emergency-Stop-Module_WeaklyCausal.af3_20",
"platform:/plugin/org.fortiss.af3.testing.ui/test-data/SimpleTrafficLightsExample.af3_20"};
List<Component> topmostComponents = new ArrayList<Component>();
......@@ -111,7 +113,9 @@ public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
public void testSemanticsAlignment() {
ToolRunnerBase.DEBUG = true;
System.out.println("### Checking semantics alignment on component: " + current.getName());
FileProject project = getParentElement(current, FileProject.class);
System.out.println("### Checking semantics alignment on component: " + current.getName() +
" from project: " + project.getName());
TestSuiteSpecification tss = createTestSuiteSpecification();
current.getSpecificationsList().add(tss);
......@@ -128,7 +132,8 @@ public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
ITerm simulated = to.getSimulatedValue();
assertEquals(
"Error with step " + stepsCount + " in component " +
current.getName(), expected, simulated);
current.getName() + " of project: " + project.getName(),
expected, simulated);
}
}
}
......@@ -137,7 +142,8 @@ public class ModelCheckerEquivalenceTest extends ModelCheckerAnalysesTestBase {
" test-cases and " + stepsCount + " test steps.");
} catch(Exception ex) {
ex.printStackTrace();
fail("Error occurred while processing component: " + current.getName());
fail("Error occurred while processing component: " + current.getName() +
" from project: " + project.getName());
}
ToolRunnerBase.DEBUG = false;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment