Implement FTA, contract-based FTA tests.
Change-Id: I4078435626a2250d72fdc9f8c4869058c2fac086
diff --git a/plugins/contracts/org.polarsys.chess.contracts.profile/src/org/polarsys/chess/contracts/profile/chesscontract/util/EntityUtil.java b/plugins/contracts/org.polarsys.chess.contracts.profile/src/org/polarsys/chess/contracts/profile/chesscontract/util/EntityUtil.java
index 8f77848..e165db0 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.profile/src/org/polarsys/chess/contracts/profile/chesscontract/util/EntityUtil.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.profile/src/org/polarsys/chess/contracts/profile/chesscontract/util/EntityUtil.java
@@ -213,7 +213,7 @@
return null;
}
- public void openCurrentModelIntoEditor(IFile file) throws Exception {
+ public IEditorPart openCurrentModelIntoEditor(IFile file) throws Exception {
IProject project = file.getProject();
@@ -246,10 +246,11 @@
// Open the model file
IWorkbenchPage page = PlatformUI.getWorkbench().getActiveWorkbenchWindow().getActivePage();
try {
- IDE.openEditor(page, modelFile, true);
+ return IDE.openEditor(page, modelFile, true);
} catch (PartInitException e) {
}
+ return null;
}
public Model loadModel(String projectName, String fileName) {
diff --git a/plugins/contracts/org.polarsys.chess.contracts.transformations/META-INF/MANIFEST.MF b/plugins/contracts/org.polarsys.chess.contracts.transformations/META-INF/MANIFEST.MF
index d8d72e3..fdc562f 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.transformations/META-INF/MANIFEST.MF
+++ b/plugins/contracts/org.polarsys.chess.contracts.transformations/META-INF/MANIFEST.MF
@@ -51,6 +51,7 @@
Bundle-ActivationPolicy: lazy
Eclipse-LazyStart: true
Export-Package: org.polarsys.chess.contracts.transformations,
+ org.polarsys.chess.contracts.transformations.commands,
org.polarsys.chess.contracts.transformations.main,
org.polarsys.chess.contracts.transformations.service
Bundle-ClassPath: .
diff --git a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/commands/CommandsCommon.java b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/commands/CommandsCommon.java
index f3ee82c..6bb6802 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/commands/CommandsCommon.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/commands/CommandsCommon.java
@@ -49,6 +49,7 @@
import org.eclipse.ui.IEditorPart;
import org.eclipse.ui.IFileEditorInput;
import org.eclipse.ui.PlatformUI;
+import org.eclipse.ui.testing.TestableObject;
import org.eclipse.uml2.uml.Class;
import org.eclipse.uml2.uml.Element;
import org.eclipse.uml2.uml.Model;
@@ -74,6 +75,7 @@
public static enum CommandEnum {REFINEMENT, IMPLEMENTATION, FTA, FEI, VALIDPROP}
+
public static void TransformationJob(final Shell activeShell, final IEditorPart editor, final List<String> args, final CommandEnum commandType, final String blockName, final String ftaCondition){
Job job = new Job("Analysis Running"){
@@ -84,6 +86,7 @@
monitor.beginTask("operation in progress ...", NUM_SUB_TASKS);
monitor.subTask("setting up project folders (if needed)...");
+ System.out.println("setting up project folders (if needed)...");
IFileEditorInput input = (IFileEditorInput) editor.getEditorInput();
IFile inputfile = input.getFile();
@@ -184,10 +187,12 @@
case FTA:
systemName = args.get(0).substring(args.get(0).lastIndexOf("::")+2);
monitor.subTask("transforming uml model... (SMV)");
+ System.out.println("transforming uml model... (SMV)");
GenerateErrorModel genFTA = new GenerateErrorModel(modelURI, target, args);
genFTA.doGenerate(null);
monitor.worked(1);
monitor.subTask("transforming uml model... (Fault Extensions)");
+ System.out.println("transforming uml model... (Fault Extensions)");
GenerateFaultExtensions genFex = new GenerateFaultExtensions(modelURI, target, args);
genFex.doGenerate(null);
smvLocation = target + File.separator + args.get(2);
@@ -195,6 +200,7 @@
smvLocation = smvLocation + FileNamesUtil.SMV_EXT;
feiLocation = feiLocation + FileNamesUtil.FEI_EXT;
monitor.subTask("calling xSAP");
+ System.out.println("calling xSAP");
checker.FTA(smvLocation, feiLocation, ftaCondition);
monitor.worked(1);
break;
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF
index 88262f6..8d174ec 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF
@@ -35,7 +35,11 @@
eu.fbk.eclipse.standardtools.diagram,
org.polarsys.chess.diagram.ui,
eu.fbk.tools.adapter.ui,
- org.polarsys.chess.OSSImporter
+ org.polarsys.chess.OSSImporter,
+ eu.fbk.eclipse.standardTools.XSapExecService,
+ org.polarsys.chess.smvExporter,
+ org.polarsys.chess.contracts.transformations,
+ org.eclipse.acceleo.engine;bundle-version="3.6.6"
Bundle-ActivationPolicy: lazy
Import-Package: eu.fbk.eclipse.standardtools.logger,
eu.fbk.tools.adapter.ui.preferences,
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties
index 66bb512..d4d2e6a 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties
@@ -1,6 +1,6 @@
OCRAPath=C:\\Users\\Alberto\\Downloads\\20180124_OpenCertCHESSClient_Win_x64\\amass_P1\\FBK_Tools\\OCRA\\ocra_win64.exe
testOutput=testOutput
-testTempOutput=C:\\tmp\\adapter
+testTempOutput=C:\\tmp\\adapter4
OCRAFilePath=resources\\tools\\ocra_win64.exe
nuXmvFilePath=resources\\tools\\nuXmv_win64.exe
-xSAPFilePath=resources\\tools\\xSAP_win64.exe
\ No newline at end of file
+xSapFilePath=resources\\tools\\xSAP_win64.exe
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/VandVResults/ContractBasedFTA/result_contract_baset_fta.xml b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/VandVResults/ContractBasedFTA/result_contract_baset_fta.xml
new file mode 100644
index 0000000..f8debcd
--- /dev/null
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/VandVResults/ContractBasedFTA/result_contract_baset_fta.xml
@@ -0,0 +1,8 @@
+<fault-tree>
+ <gate type="OR" name="G1" description="System.Sense-FAILURE_O" page="Off">
+ <event name="E2" description="System.Sense-FAILURE_I"/>
+ <event name="E3" description="System.selector.Select-FAILURE_O"/>
+ <event name="E4" description="System.sensor2.Sense-FAILURE_O"/>
+ <event name="E5" description="System.sensor1.Sense-FAILURE_O"/>
+ </gate>
+</fault-tree>
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe
index 4e45b3d..8ae22d9 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe
Binary files differ
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java
index b10b078..01e880d 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java
@@ -29,6 +29,7 @@
import org.eclipse.papyrus.junit.framework.classification.tests.AbstractPapyrusTest;
import org.eclipse.papyrus.junit.utils.rules.PluginResource;
import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture;
+import org.eclipse.ui.IEditorPart;
import org.eclipse.ui.IWorkbenchPage;
import org.eclipse.ui.PlatformUI;
import org.eclipse.uml2.uml.Class;
@@ -66,12 +67,13 @@
private final String configFileName = "configTest.properties";
private String testOutput;
- //private String testTempOutput;
-
- /*private String OCRAFilePath;
- private String nuXmvFilePath;
- private String xSAPFilePath;*/
-
+ // private String testTempOutput;
+
+ /*
+ * private String OCRAFilePath; private String nuXmvFilePath; private String
+ * xSAPFilePath;
+ */
+
private EntityUtil entityUtil = EntityUtil.getInstance();
private static final Logger logger = Logger.getLogger(TestBasicOperations.class);
@@ -80,7 +82,6 @@
@Rule
public final ResourceSetFixture resourceSetFixture = new ResourceSetFixture();
-
private Class getSystemComponent() throws Exception {
Model model = getModel();
Package umlSelectedPackage = entityUtil.getSystemViewPackage(model);
@@ -91,26 +92,24 @@
return umlSelectedComponent;
}
-
@Test
@PluginResource(projectPath)
public void testExportStateMachinesAsMonolithicSmv() throws Exception {
File outputFolder = new File(testOutput);
String selectedDirectory = outputFolder.getAbsolutePath();
-
- //IWorkspaceRoot wRoot = ResourcesPlugin.getWorkspace().getRoot();
- //logger.debug("wRoot: " + wRoot);
+
+ // IWorkspaceRoot wRoot = ResourcesPlugin.getWorkspace().getRoot();
+ // logger.debug("wRoot: " + wRoot);
Class umlSelectedComponent = getSystemComponent();
-
+
exportModelAsMonolithicSmvFile(selectedDirectory, umlSelectedComponent);
- String oracleFolder = projectFolderPath + "/MonolithicSmvFile";
+ String oracleFolder = projectFolderPath + "/MonolithicSmvFile";
verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
}
-
public static File exportModelAsMonolithicSmvFile(String selectedDirectory, Class umlSelectedComponent)
throws Exception, IOException {
OSSTranslatorServiceAPI ossTranslatorServiceAPI = new OSSTranslatorServiceAPI(ChessSystemModel.getInstance());
@@ -126,13 +125,12 @@
String outputFilePath = selectedDirectory + File.separator + umlSelectedComponent.getName().replace(".", "_")
+ "_monolithic.smv";
-
+
OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
ocraExecService.executePrintSystemImplementation(ossFile, smvMapFile, outputFilePath, true, true);
-
- return new File(outputFilePath);
- }
+ return new File(outputFilePath);
+ }
public static File createSmvMapFile(String selectedDirectory, Class umlSelectedComponent)
throws Exception, IOException {
@@ -152,7 +150,7 @@
ChessSystemModel chessSystemModel = ChessSystemModel.getInstance();
Model model = getModel();
-
+
openEditor(model);
OSSTranslatorServiceAPI ocraTranslatorService = OSSTranslatorServiceAPI.getInstance(chessSystemModel);
@@ -164,7 +162,7 @@
final OSS ossModel = ocraTranslatorService.exportRootComponentToOssModel(umlSelectedComponent, isDiscreteTime,
new NullProgressMonitor());
- String imageExtension = ".svg";
+ String imageExtension = ".svg";
String currentProjectName = "SSR";
String docFormat = "html";
@@ -176,8 +174,8 @@
DocumentGeneratorServiceFromOssModel documentGeneratorService = new DocumentGeneratorServiceFromOssModel(
ossModel, chessSystemModel, activePackage);
- documentGeneratorService.setParametersBeforeDocumentGeneration(testOutput, imageExtension, true, true,
- true, true, true, true, true, true, true, true, true, true, true, true, true);
+ documentGeneratorService.setParametersBeforeDocumentGeneration(testOutput, imageExtension, true, true, true,
+ true, true, true, true, true, true, true, true, true, true, true, true);
final DocumentGenerator documentGenerator = documentGeneratorService.createDocumentFile(currentProjectName,
docFormat, ossModel.getSystem(), new NullProgressMonitor());
@@ -185,37 +183,40 @@
documentGeneratorService.addLocalAttributeDescriptors(umlSelectedComponent, documentGenerator);
System.out.println("resultsGeneratorService");
-
+
final ResultsGeneratorService resultsGeneratorService = new ResultsGeneratorService();
resultsGeneratorService.setParametersBeforeDocumentGeneration(testOutput, true, imageExtension);
resultsGeneratorService.addResultsDescriptors(umlSelectedComponent, activePackage, documentGenerator);
- chessDiagramsGeneratorService.setParametersBeforeDiagramsGenerator(testOutput, imageExtension
- );
+ chessDiagramsGeneratorService.setParametersBeforeDiagramsGenerator(testOutput, imageExtension);
System.out.println("diagramDescriptors");
Set<DiagramDescriptor> diagramDescriptors = new HashSet<DiagramDescriptor>();
for (Diagram diagram : chessDiagrams) {
- DiagramDescriptor dd = chessDiagramsGeneratorService.createDiagramWithDescriptor(diagram, null,
- new NullProgressMonitor());
- if (dd != null) {
- diagramDescriptors.add(dd);
- }
+ DiagramDescriptor dd = chessDiagramsGeneratorService.createDiagramWithDescriptor(diagram, null,
+ new NullProgressMonitor());
+ if (dd != null) {
+ diagramDescriptors.add(dd);
+ }
}
documentGeneratorService.addDiagramDescriptors(diagramDescriptors, documentGenerator);
documentGenerator.generate(testOutput);
-
+
String oracleFolder = projectFolderPath + "/Documentation";
File outputFolder = new File(testOutput);
String selectedDirectory = outputFolder.getAbsolutePath();
-
+
verifyDirsHaveSameSize(Paths.get(oracleFolder), Paths.get(selectedDirectory));
verifyDirsHaveSameSize(Paths.get(selectedDirectory), Paths.get(oracleFolder));
}
+ public static IEditorPart openEditor(final Model model) throws Exception {
+ IFile iFile = getUmlFile(model);
+ return EntityUtil.getInstance().openCurrentModelIntoEditor(iFile);
+ }
- private void openEditor(final Model model) throws Exception {
+ public static IFile getUmlFile(final Model model) {
final org.eclipse.emf.ecore.resource.Resource resource = model.eResource();
URI resourceURI = resource.getURI();
@@ -226,45 +227,44 @@
// System.out.println("location: "+location);
IFile iFile = files[0];
- EntityUtil.getInstance().openCurrentModelIntoEditor(iFile);
+ return iFile;
}
-
@Before
public void setTestParameters() throws Exception {
testOutput = cleanDirectory("testOutput");
String testTempOutput = cleanDirectory("testTempOutput");
String OCRAFilePath = getConfigTestProperties().getProperty("OCRAFilePath");
String nuXmvFilePath = getConfigTestProperties().getProperty("nuXmvFilePath");
- //String xSAPFilePath = getConfigTestProperties().getProperty("xSAPFilePath");
+ // String xSAPFilePath =
+ // getConfigTestProperties().getProperty("xSAPFilePath");
File testTempOutputFile = new File(testTempOutput);
File ocraFile = new File(OCRAFilePath);
File nuXmvFile = new File(nuXmvFilePath);
-
- eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
- PreferenceConstants.TOOL_WORKSPACE,
- //"C:/Users/Alberto/Google Drive/AMASS Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/testTempOutput"
+
+ eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(PreferenceConstants.TOOL_WORKSPACE,
+ // "C:/Users/Alberto/Google Drive/AMASS
+ // Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/testTempOutput"
testTempOutputFile.getAbsolutePath());
-
+
eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
PreferenceConstants.OCRA_EXECUTABLE,
- //"C:/Users/Alberto/Google Drive/AMASS Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe"
- ocraFile.getAbsolutePath()
- );
+ // "C:/Users/Alberto/Google Drive/AMASS
+ // Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe"
+ ocraFile.getAbsolutePath());
eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
PreferenceConstants.NUXMV_EXECUTABLE,
- //"C:/Users/Alberto/Google Drive/AMASS Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP_win64.exe"
- nuXmvFile.getAbsolutePath()
- );
-
+ // "C:/Users/Alberto/Google Drive/AMASS
+ // Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP_win64.exe"
+ nuXmvFile.getAbsolutePath());
+
}
Model getModel() {
return (Model) resourceSetFixture.getModel();
}
-
private void verifyDirsAreEqual(Path correctResultsDir, Path toCheckResultsDir) throws IOException {
Files.walkFileTree(correctResultsDir, new SimpleFileVisitor<Path>() {
@Override
@@ -287,7 +287,7 @@
}
});
}
-
+
private void verifyDirsHaveSameSize(Path correctResultsDir, Path toCheckResultsDir) throws IOException {
Files.walkFileTree(correctResultsDir, new SimpleFileVisitor<Path>() {
@Override
@@ -310,16 +310,16 @@
}
});
}
-
+
private static String getFileSizeKiloBytes(File file) {
return (double) file.length() / 1024 + " kb";
}
-
- private boolean sameSize(Path p1, Path p2){
-
- String sizeFile1 = getFileSizeKiloBytes(p1.toFile());
- String sizeFile2 = getFileSizeKiloBytes(p2.toFile());
-
+
+ private boolean sameSize(Path p1, Path p2) {
+
+ String sizeFile1 = getFileSizeKiloBytes(p1.toFile());
+ String sizeFile2 = getFileSizeKiloBytes(p2.toFile());
+
return sizeFile1.equals(sizeFile2);
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestSafetyAnalysisOperations.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestSafetyAnalysisOperations.java
new file mode 100644
index 0000000..f226c4d
--- /dev/null
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestSafetyAnalysisOperations.java
@@ -0,0 +1,339 @@
+package org.polarsys.chess.contracts.verificationService.test.runtime.tests;
+
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.FileReader;
+import java.io.IOException;
+import java.nio.file.FileVisitResult;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.nio.file.SimpleFileVisitor;
+import java.nio.file.attribute.BasicFileAttributes;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Properties;
+import java.util.Set;
+import org.apache.commons.io.FileUtils;
+import org.apache.log4j.Logger;
+import org.eclipse.core.resources.IFile;
+import org.eclipse.core.resources.IWorkspace;
+import org.eclipse.core.resources.IWorkspaceRoot;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.core.runtime.IPath;
+import org.eclipse.core.runtime.NullProgressMonitor;
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.gmf.runtime.notation.Diagram;
+import org.eclipse.papyrus.junit.framework.classification.tests.AbstractPapyrusTest;
+import org.eclipse.papyrus.junit.utils.rules.PluginResource;
+import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture;
+import org.eclipse.ui.IEditorPart;
+import org.eclipse.uml2.uml.Class;
+import org.eclipse.uml2.uml.Model;
+import org.eclipse.uml2.uml.Package;
+import org.eclipse.uml2.uml.StateMachine;
+import org.junit.Assert;
+import org.junit.Before;
+import org.junit.Ignore;
+import org.junit.Rule;
+import org.junit.Test;
+import org.junit.rules.ErrorCollector;
+import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil;
+import org.polarsys.chess.contracts.transformations.commands.CommandsCommon;
+import org.polarsys.chess.contracts.transformations.commands.CommandsCommon.CommandEnum;
+import org.polarsys.chess.contracts.transformations.main.GenerateFaultExtensions;
+import org.polarsys.chess.diagram.ui.services.CHESSDiagramsGeneratorService;
+import org.polarsys.chess.diagram.ui.services.ResultsGeneratorService;
+import org.polarsys.chess.service.core.model.ChessSystemModel;
+import org.polarsys.chess.service.core.model.UMLStateMachineModel;
+import org.polarsys.chess.smvExporter.ui.services.CHESSSmvExporterService;
+
+import eu.fbk.eclipse.standardTools.XSapExecService.services.XSapExecService;
+import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
+import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService.ValidationType;
+import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSTranslatorServiceAPI;
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.core.services.SMVTranslatorServiceAPI;
+import eu.fbk.eclipse.standardtools.diagram.DiagramDescriptor;
+import eu.fbk.eclipse.standardtools.diagram.DocumentGenerator;
+import eu.fbk.eclipse.standardtools.diagram.ui.docGenerators.DocumentGeneratorServiceFromOssModel;
+import eu.fbk.eclipse.standardtools.nuXmvService.ui.services.NuXmvExecService;
+import eu.fbk.eclipse.standardtools.utils.core.utils.StringArrayUtil;
+import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;
+import eu.fbk.tools.editor.oss.oss.OSS;
+
+//@Headless
+public class TestSafetyAnalysisOperations extends AbstractPapyrusTest {
+
+ @Rule
+ public ErrorCollector collector = new ErrorCollector();
+
+ private final String configFileName = "configTest.properties";
+
+ private String testOutput;
+ private String testTempOutput;
+
+ private EntityUtil entityUtil = EntityUtil.getInstance();
+ private static final Logger logger = Logger.getLogger(TestSafetyAnalysisOperations.class);
+
+ private final String projectFolderPath = "resources/SSR_fi/";
+ private final String projectPath = projectFolderPath + "SSR.di";
+ @Rule
+ public final ResourceSetFixture resourceSetFixture = new ResourceSetFixture();
+
+ private Class getSystemComponent() throws Exception {
+ Model model = getModel();
+ Package umlSelectedPackage = entityUtil.getSystemViewPackage(model);
+
+ System.out.println("umlSelectedPackage: " + umlSelectedPackage);
+
+ Class umlSelectedComponent = entityUtil.getSystemElement(model);
+ return umlSelectedComponent;
+ }
+
+ @Test
+ @PluginResource(projectPath)
+ public void testFTA() throws Exception {
+
+ // File ossFile = exportModelAsOssFile(testTempOutput);
+
+ String oracleFolder = projectFolderPath + "/VandVResults/FTA";
+
+ File outputFolder = new File(testOutput);
+ String selectedDirectory = outputFolder.getAbsolutePath();
+ String resultFilePath = selectedDirectory + File.separator + "result_contract_baset_fta.xml";
+ System.out.println("resultFilePath: " + resultFilePath);
+ // OCRAExecService ocraExecService =
+ // OCRAExecService.getInstance(ChessSystemModel.getInstance());
+ // ocraExecService.executeComputeFaultTree(ossFile, true,
+ // resultFilePath, new NullProgressMonitor(), true);
+
+ XSapExecService xSapExecService = XSapExecService.getInstance();
+
+ File tempFolder = new File(testTempOutput);
+ String selectedTempDirectory = tempFolder.getAbsolutePath();
+ String extendedSmvFileName = selectedTempDirectory + File.separator + "extendedSmv.smv";
+ String expandedFeiFileName = selectedTempDirectory + File.separator + "extendedFei.smv";
+ String feiFileName = selectedTempDirectory + File.separator + "RootElement_System.fei";
+
+ String fmsFileName = selectedTempDirectory + File.separator + "fms.xml";
+ String ftaFmeaCond = "sensor1.sensed_speed_is_present=TRUE";
+
+ Model model = getModel();
+ //IEditorPart editor = TestBasicOperations.openEditor(model);
+ Class umlSelectedComponent = getSystemComponent();
+
+ String fileName = model.getName();
+ String systemQN = umlSelectedComponent.getQualifiedName();
+ List<String> args = new ArrayList<String>();
+ args.add(systemQN);
+ final String systemName = systemQN.substring(systemQN.lastIndexOf("::") + 2);
+ args.add(systemName);
+ String modelName = systemQN; // Used by the
+ args.add(modelName);
+
+ IFile umlFile = TestBasicOperations.getUmlFile(model);
+ URI modelURI = URI.createPlatformResourceURI(umlFile.getFullPath().toString() , true);
+
+ // Generate the monolithic SMV file
+ File smvFile = TestBasicOperations.exportModelAsMonolithicSmvFile(selectedTempDirectory, umlSelectedComponent);
+ String smvFileName = smvFile.getAbsolutePath();
+
+
+ // Generate the FEI file
+ GenerateFaultExtensions genFei = new GenerateFaultExtensions(modelURI, tempFolder, args);
+ genFei.doGenerate(null);
+
+ // Expand the FEI file
+ xSapExecService.expandFaultExtensions(feiFileName, expandedFeiFileName, true);
+ // Extend the SMV model
+ xSapExecService.extendModel(smvFileName, expandedFeiFileName, fmsFileName, extendedSmvFileName, true);
+
+ String ftFileName = selectedDirectory + File.separator + "ft.xml";
+
+ xSapExecService.computeFt(extendedSmvFileName, fmsFileName, ftaFmeaCond, ftFileName, true);
+
+ verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
+ verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
+ }
+
+ @Test
+ @PluginResource(projectPath)
+ // @Ignore
+ public void testContractBasedFTA() throws Exception {
+
+ File ossFile = exportModelAsOssFile(testTempOutput);
+
+ String oracleFolder = projectFolderPath + "/VandVResults/ContractBasedFTA";
+
+ File outputFolder = new File(testOutput);
+ String selectedDirectory = outputFolder.getAbsolutePath();
+ String resultFilePath = selectedDirectory + File.separator + "result_contract_baset_fta.xml";
+ System.out.println("resultFilePath: " + resultFilePath);
+ OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
+ ocraExecService.executeComputeFaultTree(ossFile, true, resultFilePath, new NullProgressMonitor(), true);
+
+ verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
+ verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
+ }
+
+ private File exportModelAsOssFile(String outputFolder) throws Exception {
+ IWorkspaceRoot wRoot = ResourcesPlugin.getWorkspace().getRoot();
+ logger.debug("wRoot: " + wRoot);
+ Class umlSelectedComponent = getSystemComponent();
+
+ OSSTranslatorServiceAPI ossTranslatorServiceAPI = new OSSTranslatorServiceAPI(ChessSystemModel.getInstance());
+ Object ocraModel = ossTranslatorServiceAPI.exportRootComponentToOssModel(umlSelectedComponent, true,
+ new NullProgressMonitor());
+ File tempFolder = new File(outputFolder);
+ String selectedTempDirectory = tempFolder.getAbsolutePath();
+ // String fileName =
+ // toolToOCRAModelTranslator.getFileName(umlSelectedComponent);
+ logger.debug("generateOssFileFromOssModel");
+ String fileName = ossTranslatorServiceAPI.getFileName(umlSelectedComponent);
+ File ossFile = ossTranslatorServiceAPI.exportOSSModelToOSSFile(ocraModel, fileName, selectedTempDirectory);
+ return ossFile;
+ }
+
+ @Before
+ public void setTestParameters() throws Exception {
+ testOutput = cleanDirectory("testOutput");
+ testTempOutput = cleanDirectory("testTempOutput");
+ String OCRAFilePath = getConfigTestProperties().getProperty("OCRAFilePath");
+ String nuXmvFilePath = getConfigTestProperties().getProperty("nuXmvFilePath");
+ String xSapFilePath = getConfigTestProperties().getProperty("xSapFilePath");
+ // String xSAPFilePath =
+ // getConfigTestProperties().getProperty("xSAPFilePath");
+
+ File testTempOutputFile = new File(testTempOutput);
+ File ocraFile = new File(OCRAFilePath);
+ File nuXmvFile = new File(nuXmvFilePath);
+ File xSapFile = new File(xSapFilePath);
+
+ eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(PreferenceConstants.TOOL_WORKSPACE,
+ // "C:/Users/Alberto/Google Drive/AMASS
+ // Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/testTempOutput"
+ testTempOutputFile.getAbsolutePath());
+
+ eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
+ PreferenceConstants.OCRA_EXECUTABLE,
+ // "C:/Users/Alberto/Google Drive/AMASS
+ // Project/ARTA_p1/eclipse/git_home/CHESS_FBK/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/ocra_win64.exe"
+ ocraFile.getAbsolutePath());
+ eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
+ PreferenceConstants.NUXMV_EXECUTABLE,
+ nuXmvFile.getAbsolutePath());
+
+ eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
+ PreferenceConstants.XSAP_EXECUTABLE,
+ xSapFile.getAbsolutePath());
+
+ }
+
+ Model getModel() {
+ return (Model) resourceSetFixture.getModel();
+ }
+
+ private void verifyDirsAreEqual(Path correctResultsDir, Path toCheckResultsDir) throws IOException {
+
+ Files.walkFileTree(correctResultsDir, new SimpleFileVisitor<Path>() {
+ @Override
+ public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException {
+ FileVisitResult result = super.visitFile(file, attrs);
+
+ // get the relative file name from path "one"
+ Path correctFilePath = correctResultsDir.relativize(file);
+ // construct the path for the counterpart file in "other"
+ Path toCheckFilePath = toCheckResultsDir.resolve(correctFilePath);
+
+ try {
+ Assert.assertTrue(file + " is not equal to " + toCheckFilePath,
+ compareTwoFilesIgnoreEOL(file, toCheckFilePath));
+ } catch (Throwable t) {
+ collector.addError(t);
+ }
+
+ return result;
+ }
+ });
+ }
+
+ private void verifyDirsHaveSameSize(Path correctResultsDir, Path toCheckResultsDir) throws IOException {
+ Files.walkFileTree(correctResultsDir, new SimpleFileVisitor<Path>() {
+ @Override
+ public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException {
+ FileVisitResult result = super.visitFile(file, attrs);
+
+ // get the relative file name from path "one"
+ Path correctFilePath = correctResultsDir.relativize(file);
+ // construct the path for the counterpart file in "other"
+ Path toCheckFilePath = toCheckResultsDir.resolve(correctFilePath);
+
+ try {
+ Assert.assertTrue(file + " has not the same size of " + toCheckFilePath,
+ sameSize(file, toCheckFilePath));
+ } catch (Throwable t) {
+ collector.addError(t);
+ }
+
+ return result;
+ }
+ });
+ }
+
+ private static String getFileSizeKiloBytes(File file) {
+ return (double) file.length() / 1024 + " kb";
+ }
+
+ private boolean sameSize(Path p1, Path p2) {
+
+ String sizeFile1 = getFileSizeKiloBytes(p1.toFile());
+ String sizeFile2 = getFileSizeKiloBytes(p2.toFile());
+
+ return sizeFile1.equals(sizeFile2);
+ }
+
+ private static boolean compareTwoFilesIgnoreEOL(Path p1, Path p2) throws IOException {
+ BufferedReader reader1 = new BufferedReader(new FileReader(p1.toFile()));
+ BufferedReader reader2 = new BufferedReader(new FileReader(p2.toFile()));
+ String line1 = reader1.readLine();
+ String line2 = reader2.readLine();
+ boolean areEqual = true;
+
+ while (line1 != null || line2 != null) {
+ if (line1 == null || line2 == null) {
+ areEqual = false;
+ break;
+ } else if (!StringArrayUtil.equalsIgnoreNewlineStyle(line1, line2)) {
+ areEqual = false;
+ break;
+ }
+ line1 = reader1.readLine();
+ line2 = reader2.readLine();
+ }
+ reader1.close();
+ reader2.close();
+
+ return areEqual;
+ }
+
+ private String cleanDirectory(String propertyDirectoryPathName) throws IOException {
+ String workspaceDir = getConfigTestProperties().getProperty(propertyDirectoryPathName);
+ File workspaceDirFile = new File(workspaceDir);
+ FileUtils.deleteDirectory(workspaceDirFile);
+ workspaceDirFile.mkdirs();
+ return workspaceDir;
+ }
+
+ private Properties getConfigTestProperties() throws IOException {
+ File configFile = new File(configFileName);
+
+ FileReader reader = new FileReader(configFile);
+ Properties props = new Properties();
+ props.load(reader);
+ reader.close();
+ return props;
+
+ }
+}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestVAndVOperations.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestVAndVOperations.java
index 7facc2c..924e597 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestVAndVOperations.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestVAndVOperations.java
@@ -11,19 +11,13 @@
import java.nio.file.SimpleFileVisitor;
import java.nio.file.attribute.BasicFileAttributes;
import java.util.Collection;
-import java.util.HashSet;
import java.util.Properties;
import java.util.Set;
import org.apache.commons.io.FileUtils;
import org.apache.log4j.Logger;
-import org.eclipse.core.resources.IFile;
-import org.eclipse.core.resources.IWorkspace;
import org.eclipse.core.resources.IWorkspaceRoot;
import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.core.runtime.IPath;
import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eclipse.emf.common.util.URI;
-import org.eclipse.gmf.runtime.notation.Diagram;
import org.eclipse.papyrus.junit.framework.classification.tests.AbstractPapyrusTest;
import org.eclipse.papyrus.junit.utils.rules.PluginResource;
import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture;
@@ -33,13 +27,10 @@
import org.eclipse.uml2.uml.StateMachine;
import org.junit.Assert;
import org.junit.Before;
-import org.junit.Ignore;
import org.junit.Rule;
import org.junit.Test;
import org.junit.rules.ErrorCollector;
import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil;
-import org.polarsys.chess.diagram.ui.services.CHESSDiagramsGeneratorService;
-import org.polarsys.chess.diagram.ui.services.ResultsGeneratorService;
import org.polarsys.chess.service.core.model.ChessSystemModel;
import org.polarsys.chess.service.core.model.UMLStateMachineModel;
@@ -47,13 +38,9 @@
import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService.ValidationType;
import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSTranslatorServiceAPI;
import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.core.services.SMVTranslatorServiceAPI;
-import eu.fbk.eclipse.standardtools.diagram.DiagramDescriptor;
-import eu.fbk.eclipse.standardtools.diagram.DocumentGenerator;
-import eu.fbk.eclipse.standardtools.diagram.ui.docGenerators.DocumentGeneratorServiceFromOssModel;
import eu.fbk.eclipse.standardtools.nuXmvService.ui.services.NuXmvExecService;
import eu.fbk.eclipse.standardtools.utils.core.utils.StringArrayUtil;
import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;
-import eu.fbk.tools.editor.oss.oss.OSS;
//@Headless
public class TestVAndVOperations extends AbstractPapyrusTest {
@@ -291,89 +278,7 @@
verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
}
- @Test
- @Ignore
- @PluginResource(projectPath)
- public void testGenerationDocumentation() throws Exception {
-
- ChessSystemModel chessSystemModel = ChessSystemModel.getInstance();
-
- Model model = getModel();
-
- openEditor(model);
-
- OSSTranslatorServiceAPI ocraTranslatorService = OSSTranslatorServiceAPI.getInstance(chessSystemModel);
-
- Class umlSelectedComponent = getSystemComponent();
- Package activePackage = umlSelectedComponent.getNearestPackage();
-
- boolean isDiscreteTime = false;
- final OSS ossModel = ocraTranslatorService.exportRootComponentToOssModel(umlSelectedComponent, isDiscreteTime,
- new NullProgressMonitor());
-
- String imageExtension = ".svg";
- String currentProjectName = "SSR";
- String docFormat = "html";
-
- CHESSDiagramsGeneratorService chessDiagramsGeneratorService = CHESSDiagramsGeneratorService.getInstance();
-
- Collection<Diagram> chessDiagrams = chessDiagramsGeneratorService.getDiagrams();
-
- System.out.println("num diagrams: " + chessDiagrams.size());
-
- DocumentGeneratorServiceFromOssModel documentGeneratorService = new DocumentGeneratorServiceFromOssModel(
- ossModel, chessSystemModel, activePackage);
- documentGeneratorService.setParametersBeforeDocumentGeneration(testOutput, imageExtension, true, true, true,
- true, true, true, true, true, true, true, true, true, true, true, true);
-
- final DocumentGenerator documentGenerator = documentGeneratorService.createDocumentFile(currentProjectName,
- docFormat, ossModel.getSystem(), new NullProgressMonitor());
-
- documentGeneratorService.addLocalAttributeDescriptors(umlSelectedComponent, documentGenerator);
-
- System.out.println("resultsGeneratorService");
-
- final ResultsGeneratorService resultsGeneratorService = new ResultsGeneratorService();
- resultsGeneratorService.setParametersBeforeDocumentGeneration(testOutput, true, imageExtension);
- resultsGeneratorService.addResultsDescriptors(umlSelectedComponent, activePackage, documentGenerator);
-
- chessDiagramsGeneratorService.setParametersBeforeDiagramsGenerator(testOutput, imageExtension);
- System.out.println("diagramDescriptors");
- Set<DiagramDescriptor> diagramDescriptors = new HashSet<DiagramDescriptor>();
- for (Diagram diagram : chessDiagrams) {
- DiagramDescriptor dd = chessDiagramsGeneratorService.createDiagramWithDescriptor(diagram, null,
- new NullProgressMonitor());
- if (dd != null) {
- diagramDescriptors.add(dd);
- }
- }
- documentGeneratorService.addDiagramDescriptors(diagramDescriptors, documentGenerator);
- documentGenerator.generate(testOutput);
-
- String oracleFolder = projectFolderPath + "/Documentation";
-
- File outputFolder = new File(testOutput);
- String selectedDirectory = outputFolder.getAbsolutePath();
-
- verifyDirsHaveSameSize(Paths.get(oracleFolder), Paths.get(selectedDirectory));
- verifyDirsHaveSameSize(Paths.get(selectedDirectory), Paths.get(oracleFolder));
-
- }
-
- private void openEditor(final Model model) throws Exception {
- final org.eclipse.emf.ecore.resource.Resource resource = model.eResource();
-
- URI resourceURI = resource.getURI();
- IWorkspace workspace = ResourcesPlugin.getWorkspace();
- IPath workspacePath = workspace.getRoot().getLocation();
- IPath finalPath = workspacePath.append(resourceURI.toPlatformString(false));
- final IFile[] files = ResourcesPlugin.getWorkspace().getRoot().findFilesForLocation(finalPath);
-
- // System.out.println("location: "+location);
- IFile iFile = files[0];
- EntityUtil.getInstance().openCurrentModelIntoEditor(iFile);
- }
-
+
@Before
public void setTestParameters() throws Exception {
testOutput = cleanDirectory("testOutput");
diff --git a/plugins/fla/org.polarsys.chess.xtext.fladsl.ide/target/classes/org/polarsys/chess/xtext/ide/.FlaDslIdeModule.java._trace b/plugins/fla/org.polarsys.chess.xtext.fladsl.ide/target/classes/org/polarsys/chess/xtext/ide/.FlaDslIdeModule.java._trace
new file mode 100644
index 0000000..d50479e
--- /dev/null
+++ b/plugins/fla/org.polarsys.chess.xtext.fladsl.ide/target/classes/org/polarsys/chess/xtext/ide/.FlaDslIdeModule.java._trace
Binary files differ
