plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestVAndVOperations.java

package org.polarsys.chess.contracts.verificationService.test.runtime.tests;

import java.io.File;
import java.util.Collection;
import java.util.Set;

import org.apache.commons.io.FilenameUtils;
import org.apache.log4j.Logger;
import org.eclipse.core.resources.IWorkspaceRoot;
import org.eclipse.core.resources.ResourcesPlugin;
import org.eclipse.core.runtime.NullProgressMonitor;
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.eclipse.uml2.uml.StateMachine;
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.verificationService.test.runtime.util.TestResultsUtil;
import org.polarsys.chess.service.core.model.ChessSystemModel;
import org.polarsys.chess.service.core.model.UMLStateMachineModel;

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.nuXmvService.ui.services.NuXmvExecService;
import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;

public class TestVAndVOperations extends AbstractPapyrusTest {

	@Rule
	public ErrorCollector collector = new ErrorCollector();

	protected String testOutput;
	private String testTempOutput;

	private EntityUtil entityUtil = EntityUtil.getInstance();
	private static final Logger logger = Logger.getLogger(TestVAndVOperations.class);

	private final String projectFolderPath = "resources/SSR_fi/";
	private final String projectPath = projectFolderPath + "SSR.di";

	private final String projectParamArchFolderPath = "resources/ParamArch/";
	private final String projectParamArchPath = projectParamArchFolderPath + "ParamArch.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 testCheckValidationOnProperties() throws Exception {

		File ossFile = exportModelAsOssFile(testTempOutput);

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

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();
		String resultFilePath = selectedDirectory + File.separator + "result_validation_property.xml";
		System.out.println("resultFilePath: " + resultFilePath);
		OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
		ocraExecService.executeValidationProperty(ossFile, ValidationType.CONSISTENCY, "consistency", "ALL", "", "",
				true, resultFilePath, new NullProgressMonitor(), true);

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

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

		File tempFolder = new File(testTempOutput);
		String selectedTempDirectory = tempFolder.getAbsolutePath();

		String property = "TRUE";
		String algorithm_type = "ic3";
		String check_type = "ltlspec";

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();

		// IWorkspaceRoot wRoot = ResourcesPlugin.getWorkspace().getRoot();
		// logger.debug("wRoot: " + wRoot);
		Class umlSelectedComponent = getSystemComponent();

		File smvFile = TestBasicOperations.exportModelAsMonolithicSmvFile(selectedTempDirectory, selectedTempDirectory,
				umlSelectedComponent);

		String resultFilePath = selectedDirectory + File.separator + "result_validation_property.xml";

		NuXmvExecService nuXmvExecService = NuXmvExecService.getInstance(ChessSystemModel.getInstance());
		nuXmvExecService.modelCheckingCommand(smvFile.getAbsolutePath(), property, algorithm_type, check_type,
				resultFilePath, true);

		String oracleFolder = projectFolderPath + "/VandVResults/ModelCheckingOnSystemComponent";
		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
	}

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

		File tempFolder = new File(testTempOutput);
		String selectedTempDirectory = tempFolder.getAbsolutePath();

		OSSTranslatorServiceAPI ossTranslatorServiceAPI = new OSSTranslatorServiceAPI(ChessSystemModel.getInstance());
		Class umlSelectedComponent = getSystemComponent();
		Object ocraModel = ossTranslatorServiceAPI.exportRootComponentToOssModel(umlSelectedComponent, true,
				new NullProgressMonitor());

		// File ossFile = exportModelAsOssFile(testTempOutput);
		String fileName = ossTranslatorServiceAPI.getFileName(umlSelectedComponent);
		File ossFile = ossTranslatorServiceAPI.exportOSSModelToOSSFile(ocraModel, fileName, selectedTempDirectory);

		File smvMapFile = TestBasicOperations.createSmvMapFile(selectedTempDirectory, umlSelectedComponent);

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();

		String resultFilePath = selectedDirectory + File.separator + "result_composite_implementation_property.xml";
		System.out.println("resultFilePath: " + resultFilePath);

		OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
		ocraExecService.executeCheckCompositeImplementation(ossFile, smvMapFile, resultFilePath, true, true);

		logger.debug("verifyDirsAreEqual");
		String oracleFolder = projectFolderPath + "/VandVResults/CheckCompositeContractImplementation";
		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
	}

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

		File tempFolder = new File(testTempOutput);
		String selectedTempDirectory = tempFolder.getAbsolutePath();

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();

		Model model = getModel();
		// Set<?> stateMachines = entityUtil.getNominalStateMachines(model);
		Package umlSelectedPackage = entityUtil.getSystemViewPackage(model);
		Collection<Class> blocks = entityUtil.getAllClasses(umlSelectedPackage);
		SMVTranslatorServiceAPI smvTranslatorService = SMVTranslatorServiceAPI
				.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());

		// File ossFile = exportModelAsOssFile(testTempOutput);

		logger.debug("blocks.size: " + blocks.size());
		for (Class block : blocks) {
			StateMachine stateMachine = entityUtil.getFirstNominalStateMachine(block);
			if (stateMachine != null) {
				File ossFile = TestBasicOperationsHeadless.exportModelAsOss(block, testTempOutput);
				File smvFile = smvTranslatorService.exportStateMachineToSmvFile(stateMachine, selectedTempDirectory,
						null, new NullProgressMonitor());
				System.out.println("smvFile: " + smvFile.getAbsolutePath());
				String resultFilePath =
						// "C:\\tmp\\output.xml";
						// "C:\\tmp\\output_result_model_checking_"+smvFile.getName()+".xml";
						selectedDirectory + File.separator + "result_check_implementation_" + smvFile.getName()
								+ ".xml";
				System.out.println("resultFilePath: " + resultFilePath);

				OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
				ocraExecService.executeCheckContractImplementation(ossFile.getAbsolutePath(), smvFile.getAbsolutePath(),
						resultFilePath, true, true);
			}
		}
		Thread.sleep(5000);
		logger.debug("verifyDirsAreEqual");
		String oracleFolder = projectFolderPath + "/VandVResults/CheckContractImplementation";
		TestResultsUtil.dirsAreEqual(selectedDirectory, oracleFolder, collector);
	}

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

		File tempFolder = new File(testTempOutput);
		String selectedTempDirectory = tempFolder.getAbsolutePath();

		String property = "TRUE";
		String algorithm_type = "ic3";
		String check_type = "ltlspec";

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();

		Model model = getModel();
		Set<?> stateMachines = entityUtil.getNominalStateMachines(model);

		SMVTranslatorServiceAPI smvTranslatorService = SMVTranslatorServiceAPI
				.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());

		logger.debug("stateMachines.size: " + stateMachines.size());
		for (Object stateMachine : stateMachines) {
			File smvFile = smvTranslatorService.exportStateMachineToSmvFile(stateMachine, selectedTempDirectory, null,
					new NullProgressMonitor());
			System.out.println("smvFile: " + smvFile.getAbsolutePath());
			String resultFilePath =
					// "C:\\tmp\\output.xml";
					// "C:\\tmp\\output_result_model_checking_"+smvFile.getName()+".xml";
					selectedDirectory + File.separator + "result_model_checking_" + smvFile.getName() + ".xml";
			System.out.println("resultFilePath: " + resultFilePath);

			NuXmvExecService nuXmvExecService = NuXmvExecService.getInstance(ChessSystemModel.getInstance());
			nuXmvExecService.modelCheckingCommand(smvFile.getAbsolutePath(), property, algorithm_type, check_type,
					resultFilePath, true);
		}

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

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

		File ossFile = exportModelAsOssFile(testTempOutput);
		String oracleFolder = projectFolderPath + "/VandVResults/ContractRefinement";

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();
		String resultFilePath = selectedDirectory + File.separator + "result_contract_refinement.xml";
		System.out.println("resultFilePath: " + resultFilePath);
		OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
		ocraExecService.executeCheckContractRefinement(ossFile, true, resultFilePath, new NullProgressMonitor(), true);

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

	@Test
	@PluginResource(projectParamArchPath)
	public void testCheckContractRefinementOnInstantiateArch() throws Exception {

		File ossFile = exportModelAsOssFile(testTempOutput);
		File outputTempFolder = new File(testTempOutput);
		String selectedTempDirectory = outputTempFolder.getAbsolutePath();
		String originalOssFileName = FilenameUtils.removeExtension(ossFile.getName());
		String resultFileName = originalOssFileName + "_instantiate.oss";
		File instantiateOssFile = TestBasicOperations.instantiateParamArch(resultFileName, selectedTempDirectory,
				ossFile, "4");

		File outputFolder = new File(testOutput);
		String selectedDirectory = outputFolder.getAbsolutePath();
		String resultFilePath = selectedDirectory + File.separator + "result_contract_refinement.xml";
		System.out.println("resultFilePath: " + resultFilePath);
		OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
		ocraExecService.executeCheckContractRefinement(instantiateOssFile, true, resultFilePath,
				new NullProgressMonitor(), true);

		String oracleFolder = projectParamArchFolderPath + "/VandVResults/ContractRefinement";
		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
	}

	@Before
	public void setTestParameters() throws Exception {
		testOutput = TestResultsUtil.cleanDirectory("testOutputVandVOperations");
		testTempOutput = TestResultsUtil.cleanDirectory("testTempOutput");
		String OCRAFilePath = TestResultsUtil.getProperty("OCRAFilePath");
		String nuXmvFilePath = TestResultsUtil.getProperty("nuXmvFilePath");
		// 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,
				testTempOutputFile.getAbsolutePath());
		eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore()
				.setValue(PreferenceConstants.OCRA_EXECUTABLE, ocraFile.getAbsolutePath());
		eu.fbk.tools.adapter.ui.Activator.getDefault().getPreferenceStore()
				.setValue(PreferenceConstants.NUXMV_EXECUTABLE, nuXmvFile.getAbsolutePath());

	}

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

}