plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestSafetyAnalysisOperations.java - chess/chess - Git at Google

 /*******************************************************************************
  * Copyright (C) 2020 Fondazione Bruno Kessler.
  * All rights reserved. This program and the accompanying materials
  * are made available under the terms of the Eclipse Public License v2.0
  * which accompanies this distribution, and is available at
  * http://www.eclipse.org/legal/epl-v20.html
  ******************************************************************************/
 package org.polarsys.chess.contracts.verificationService.test.runtime.tests;

 import java.io.File;
 import java.util.ArrayList;
 import java.util.List;
 import org.apache.log4j.Logger;
 import org.eclipse.core.resources.IFile;
 import org.eclipse.core.resources.IWorkspaceRoot;
 import org.eclipse.core.resources.ResourcesPlugin;
 import org.eclipse.core.runtime.NullProgressMonitor;
 import org.eclipse.emf.common.util.URI;
 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.uml2.uml.Class;
 import org.eclipse.uml2.uml.Model;
 import org.eclipse.uml2.uml.Package;
 import org.junit.Before;
 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.main.GenerateFaultExtensions;
 import org.polarsys.chess.contracts.verificationService.test.runtime.util.TestResultsUtil;
 import org.polarsys.chess.service.core.model.ChessSystemModel;
 import eu.fbk.eclipse.standardTools.XSapExecService.services.XSapExecService;
 import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
 import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSTranslatorServiceAPI;
 import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;

 //@Headless
 public class TestSafetyAnalysisOperations extends AbstractPapyrusTest {

 	@Rule
 	public ErrorCollector collector = new ErrorCollector();

 	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();
 		Class umlSelectedComponent = getSystemComponent();

 		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,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);

 		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory,collector);
 	}

 	@Test
 	@PluginResource(projectPath)
 	public void testFMEA() throws Exception {

 		String oracleFolder = projectFolderPath + "/VandVResults/FMEA";

 		File outputFolder = new File(testOutput);
 		String selectedDirectory = outputFolder.getAbsolutePath();
 		String resultFilePath = selectedDirectory + File.separator + "result_fmea.xml";
 		System.out.println("resultFilePath: " + resultFilePath);

 		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();
 		Class umlSelectedComponent = getSystemComponent();

 		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,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.computeFmea(extendedSmvFileName, fmsFileName, ftaFmeaCond, ftFileName, true);

 		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
 	}

 	@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);

 		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
 	}

 	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();
 		logger.debug("generateOssFileFromOssModel");
 		String fileName = ossTranslatorServiceAPI.getFileName(umlSelectedComponent);
 		File ossFile = ossTranslatorServiceAPI.exportOSSModelToOSSFile(ocraModel, fileName, selectedTempDirectory);
 		return ossFile;
 	}

 	@Before
 	public void setTestParameters() throws Exception {
 		testOutput = TestResultsUtil.cleanDirectory("testOutputSafetyOperations");
 		testTempOutput = TestResultsUtil.cleanDirectory("testTempOutput");
 		String OCRAFilePath = TestResultsUtil.getProperty("OCRAFilePath");
 		String nuXmvFilePath = TestResultsUtil.getProperty("nuXmvFilePath");
 		String xSapFilePath = TestResultsUtil.getProperty("xSapFilePath");
 		String feiFilePath = TestResultsUtil.getProperty("feiFilePathPath");
 		// 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);
 		File feiExpFile = new File(feiFilePath);

 		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());

 		eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
 				PreferenceConstants.FEI_EXPANDER_EXECUTABLE,
 					feiExpFile.getAbsolutePath());

 		eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
 				PreferenceConstants.OSLC_ENABLED, false);
 	}

 	Model getModel() {
 		return (Model) resourceSetFixture.getModel();
 	}


 }
	/*******************************************************************************
	* Copyright (C) 2020 Fondazione Bruno Kessler.
	* All rights reserved. This program and the accompanying materials
	* are made available under the terms of the Eclipse Public License v2.0
	* which accompanies this distribution, and is available at
	* http://www.eclipse.org/legal/epl-v20.html
	******************************************************************************/
	package org.polarsys.chess.contracts.verificationService.test.runtime.tests;

	import java.io.File;
	import java.util.ArrayList;
	import java.util.List;
	import org.apache.log4j.Logger;
	import org.eclipse.core.resources.IFile;
	import org.eclipse.core.resources.IWorkspaceRoot;
	import org.eclipse.core.resources.ResourcesPlugin;
	import org.eclipse.core.runtime.NullProgressMonitor;
	import org.eclipse.emf.common.util.URI;
	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.uml2.uml.Class;
	import org.eclipse.uml2.uml.Model;
	import org.eclipse.uml2.uml.Package;
	import org.junit.Before;
	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.main.GenerateFaultExtensions;
	import org.polarsys.chess.contracts.verificationService.test.runtime.util.TestResultsUtil;
	import org.polarsys.chess.service.core.model.ChessSystemModel;
	import eu.fbk.eclipse.standardTools.XSapExecService.services.XSapExecService;
	import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
	import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSTranslatorServiceAPI;
	import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;

	//@Headless
	public class TestSafetyAnalysisOperations extends AbstractPapyrusTest {

	@Rule
	public ErrorCollector collector = new ErrorCollector();

	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();
	Class umlSelectedComponent = getSystemComponent();

	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,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);

	TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory,collector);
	}

	@Test
	@PluginResource(projectPath)
	public void testFMEA() throws Exception {

	String oracleFolder = projectFolderPath + "/VandVResults/FMEA";

	File outputFolder = new File(testOutput);
	String selectedDirectory = outputFolder.getAbsolutePath();
	String resultFilePath = selectedDirectory + File.separator + "result_fmea.xml";
	System.out.println("resultFilePath: " + resultFilePath);

	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();
	Class umlSelectedComponent = getSystemComponent();

	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,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.computeFmea(extendedSmvFileName, fmsFileName, ftaFmeaCond, ftFileName, true);

	TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
	}

	@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);

	TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
	}

	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();
	logger.debug("generateOssFileFromOssModel");
	String fileName = ossTranslatorServiceAPI.getFileName(umlSelectedComponent);
	File ossFile = ossTranslatorServiceAPI.exportOSSModelToOSSFile(ocraModel, fileName, selectedTempDirectory);
	return ossFile;
	}

	@Before
	public void setTestParameters() throws Exception {
	testOutput = TestResultsUtil.cleanDirectory("testOutputSafetyOperations");
	testTempOutput = TestResultsUtil.cleanDirectory("testTempOutput");
	String OCRAFilePath = TestResultsUtil.getProperty("OCRAFilePath");
	String nuXmvFilePath = TestResultsUtil.getProperty("nuXmvFilePath");
	String xSapFilePath = TestResultsUtil.getProperty("xSapFilePath");
	String feiFilePath = TestResultsUtil.getProperty("feiFilePathPath");
	// 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);
	File feiExpFile = new File(feiFilePath);

	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());

	eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
	PreferenceConstants.FEI_EXPANDER_EXECUTABLE,
	feiExpFile.getAbsolutePath());

	eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore().setValue(
	PreferenceConstants.OSLC_ENABLED, false);
	}

	Model getModel() {
	return (Model) resourceSetFixture.getModel();
	}



	}