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.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.Collection;
import java.util.Properties;
import java.util.Set;
import org.apache.commons.io.FileUtils;
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.Assert;
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.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.eclipse.standardtools.utils.core.utils.StringArrayUtil;
import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;

//@Headless
public class TestVAndVOperations 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(TestVAndVOperations.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 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);

		verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
		verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
	}

	@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, 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";
		verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
		verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
	}

	@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";
		verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
		verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
	}

	@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";
		verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
		verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
	}

	@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";
		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;
	}

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

		verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory));
		verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder));
	}

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

		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"
				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,
				// "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
			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;

	}
}