Commit 577ffd0f authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

basic test cases running successfully

refs 3049
parent 6728bbd3
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="generated-src"/>
<classpathentry kind="src" path="test-src"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
......
......@@ -9,5 +9,6 @@ bin.includes = .,\
plugin.xml,\
plugin.properties
source.. = src/,\
generated-src/
generated-src/,\
test-src/
output.. = build/
# (c) 2011 ForTISS GmbH
# <copyright>
# </copyright>
#
# $Id$
pluginName = Micro Model
providerName = www.example.org
pluginName = AF3 Specification
providerName = fortiss GmbH
/*--------------------------------------------------------------------------+
$Id$
| |
| Copyright 2017 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package test.org.fortiss.af3.specification.nusmv.transformation;
import static org.eclipse.emf.common.util.URI.createPlatformPluginURI;
import static org.fortiss.af3.project.utils.ProjectUtils.loadProjectFromURI;
import static org.fortiss.af3.tools.nusmv.model.utils.TermEqualityOfNuSMVElements.isModuleDeclarationEqual;
import static org.fortiss.tooling.kernel.utils.EMFResourceUtils.loadModelFromFile;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import static org.junit.Assert.assertTrue;
import java.util.List;
import org.eclipse.emf.common.util.URI;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.af3.specification.modelchecking.af3tonusmv.NuSMVTransformations;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.junit.Before;
import org.junit.Test;
/**
*
* @author kanav
* @author $Author$
* @version $Rev$
* @ConQAT.Rating RED Hash:
*/
public class STLTransformationTest {
private NuSMVFile nusmvFileSTL;
private FileProject projectSTL;
private NuSMVFile output;
/** Setup. */
@Before
public void setUp() {
URI uri =
createPlatformPluginURI(
"org.fortiss.af3.specification/test-data/SimpleTrafficLightsExample.af3_23",
true);
projectSTL = loadProjectFromURI(uri, false);
URI uriNuSMVFile =
createPlatformPluginURI(
"org.fortiss.af3.specification/test-data/SimpleTrafficLightsExample_nuXmvModel.xml",
true);
// This is the test data which will be used to match the transformation output.
nusmvFileSTL = (NuSMVFile)loadModelFromFile(uriNuSMVFile);
NuSMVTransformations t = new NuSMVTransformations();
output = (NuSMVFile)t.getTransformationForModelChecking().buildTransformation(projectSTL);
}
/** Test if the transformation returns an output. */
@Test
public void testExecuteTransformationOnSTL() {
assertTrue(output == nusmvFileSTL);
}
/** Test code spec parsing. */
@Test
public void testAllModulesAreCorrectlyGenerated() {
List<Module> lstOutput = getChildrenWithType(output, Module.class);
List<Module> lstTestData = getChildrenWithType(nusmvFileSTL, Module.class);
// Again assuming that lists will be in same order
System.out.println("Output: " + lstOutput.size() + " modules and test data has " +
lstTestData.size());
assertTrue(lstOutput.size() == lstTestData.size());
for(int i = 0; i < lstOutput.size(); i++)
assertTrue(isModuleDeclarationEqual(lstOutput.get(i), lstTestData.get(i)));
}
}
......@@ -69,6 +69,7 @@ Export-Package: org.fortiss.af3.tools,
org.fortiss.af3.tools.nusmv.model.types.impl,
org.fortiss.af3.tools.nusmv.model.types.util,
org.fortiss.af3.tools.nusmv.model.util,
org.fortiss.af3.tools.nusmv.model.utils,
org.fortiss.af3.tools.nusmv.run,
org.fortiss.af3.tools.nusmv.textgen,
org.fortiss.af3.tools.nusmv.xml.counterexample,
......
/*--------------------------------------------------------------------------+
$Id$
| |
| Copyright 2017 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.tools.nusmv.model.utils;
import org.fortiss.af3.tools.nusmv.model.module.LocalVariable;
import org.fortiss.af3.tools.nusmv.model.module.Module;
import org.fortiss.af3.tools.nusmv.model.types.BooleanType;
import org.fortiss.af3.tools.nusmv.model.types.EnumerationType;
import org.fortiss.af3.tools.nusmv.model.types.RangeType;
import org.fortiss.af3.tools.nusmv.model.types.TypeBase;
/**
* Thoughts:
* 1) Just implementing it as a static class, but this function can be added to every nusmv element.
* 2) Type base should definitely have its own term equality
*
* @author kanav
* @author $Author$
* @version $Rev$
* @ConQAT.Rating RED Hash:
*/
public class TermEqualityOfNuSMVElements {
public static boolean isModuleDeclarationEqual(Module m1, Module m2) {
if(!m1.getName().equals(m2.getName()))
return false;
// Check parameters are equal
// Assuming list order is preserved
if(m1.getParameters().size() != m2.getParameters().size())
return false;
for(int i = 0; i < m1.getParameters().size(); i++) {
if(!checkLocalVariableEquality(m1.getParameters().get(i), m2.getParameters().get(i)))
return false;
}
return true;
}
public static boolean checkLocalVariableEquality(LocalVariable lv1, LocalVariable lv2) {
if(!lv1.getName().equals(lv2.getName()))
return false;
if(!checkTypeBaseEquality(lv1.getType(), lv2.getType()))
return false;
return true;
}
public static boolean checkTypeBaseEquality(TypeBase t1, TypeBase t2) {
if(t1 instanceof BooleanType && t2 instanceof BooleanType)
return true;
if((t1 instanceof RangeType && t2 instanceof RangeType) &&
(checkRangeTypeEquality((RangeType)t1, (RangeType)t2)))
return true;
if((t1 instanceof EnumerationType && t2 instanceof EnumerationType) &&
(checkEnumerationTypeEquality((EnumerationType)t1, (EnumerationType)t2)))
return true;
System.out.println("Error in function checkTypeBaseEquality. This case is not handled.");
return false;
}
private static boolean checkEnumerationTypeEquality(EnumerationType e1, EnumerationType e2) {
if(e1.getValues().containsAll(e2.getValues()) &&
(e2.getValues().containsAll(e1.getValues())))
return true;
return false;
}
private static boolean checkRangeTypeEquality(RangeType r1, RangeType r2) {
if((r1.getLowerBound() != r2.getLowerBound()) || (r1.getUpperBound() != r2.getUpperBound()))
return false;
return true;
}
}
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