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