diff --git a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/AnalysisResultUtil.java b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/AnalysisResultUtil.java
index 791a7b192a64cfce24efc689a1246bac364607a8..3e5dd00aadd1fe41e96adecc5209245e2336a586 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/AnalysisResultUtil.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/AnalysisResultUtil.java
@@ -66,6 +66,7 @@ public class AnalysisResultUtil {
public static final String CONTRACT_BASED_FTA_ANALYSIS = "CONTRACT_FTA";
public static final String CONTRACT_REFINEMENT_ANALYSIS = "CONTRACT_REF";
public static final String CONTRACT_IMPLEMENTATION_ANALYSIS = "CONTRACT_IMPL";
+ public static final String PROPERTY_VALIDATION_ANALYSIS = "PROP_VALIDATION";
private static AnalysisResultUtil packageUtilInstance;
private final EntityUtil entityUtil = EntityUtil.getInstance();
diff --git a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/FileNamesUtil.java b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/FileNamesUtil.java
index c3da391466a8af588c47b66e2c6ae17c9de82789..9b77e175f8ab6ca8c09913ebf53374d903c89ad1 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/FileNamesUtil.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/FileNamesUtil.java
@@ -230,4 +230,15 @@ public class FileNamesUtil {
return resPath + File.separator + computeQualifiedName(systemComponent) + "_" +
AnalysisResultUtil.CONTRACT_IMPLEMENTATION_ANALYSIS + "_" + getDate() + XML_EXT;
}
+
+ /**
+ * Computes the file name for the Property Validation analysis.
+ * @param systemComponent the root component of the analysis
+ * @return
+ */
+ public String computePropertyValidationFileName(Class systemComponent) {
+ final String resPath = AnalysisResultUtil.getInstance().getResultDir();
+ return resPath + File.separator + computeQualifiedName(systemComponent) + "_" +
+ AnalysisResultUtil.PROPERTY_VALIDATION_ANALYSIS + "_" + getDate() + XML_EXT;
+ }
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml b/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
index 2f8ce73b3edd92d2e514dfc46db7f4f1de83759b..02d0ac7d41fe8eaef5aa884b655733609aa2493e 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
@@ -137,6 +137,16 @@
name="store_result"
value="true">
</parameter>
+ </command>
+ <command
+ commandId="org.polarsys.chess.verificationService.ui.commands.CheckValidationAssertionPropertyCommand"
+ icon="icons/contract_verification.png"
+ label="Check Validation on Properties"
+ style="push">
+ <parameter
+ name="store_result"
+ value="true">
+ </parameter>
</command>
</menu>
</menuContribution>
@@ -371,6 +381,11 @@
defaultHandler="org.polarsys.chess.verificationService.ui.commands.CheckValidationAssertionPropertyCommand"
id="org.polarsys.chess.verificationService.ui.commands.CheckValidationAssertionPropertyCommand"
name="Check Validation on Properties on selected component">
+ <commandParameter
+ id="store_result"
+ name="storeResult"
+ optional="true">
+ </commandParameter>
</command>
</extension>
</plugin>
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java
index 3f2abc6f666559a74325244a4bc497460d544217..dfe9ffadfc4db8c8b857a8463e45783651cf4a3c 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java
@@ -14,6 +14,9 @@ import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.uml2.uml.Class;
+import org.polarsys.chess.contracts.transformations.utils.AnalysisResultUtil;
+import org.polarsys.chess.contracts.transformations.utils.FileNamesUtil;
+import org.polarsys.chess.service.core.exceptions.NoComponentException;
import org.polarsys.chess.service.core.model.ChessSystemModel;
import org.polarsys.chess.service.gui.utils.SelectionUtil;
@@ -21,6 +24,7 @@ import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService
import eu.fbk.eclipse.standardtools.utils.ui.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.utils.ui.dialogs.MessageTimeModelDialog;
import eu.fbk.eclipse.standardtools.utils.ui.utils.OCRADirectoryUtil;
+import eu.fbk.tools.adapter.ocra.CheckValidationProperty;
/**
*
@@ -32,7 +36,8 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand
private OCRAExecService ocraExecService = OCRAExecService.getInstance(chessToOCRAModelTranslator);
private SelectionUtil selectionUtil = SelectionUtil.getInstance();
private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
-
+ private AnalysisResultUtil analysisResultUtil = AnalysisResultUtil.getInstance();
+
public CheckValidationAssertionPropertyCommand() {
super("Check Validation Property");
}
@@ -44,25 +49,57 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand
private boolean usexTextValidation;
private String ossFilepath;
private String resultFilePath;
-
+ private boolean storeResult;
+
@Override
public void execPreJobOperations(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
- umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
+ final String storeResultParam = "store_result";
+
+ // The user could select a component or a package containing an architecture
+ // In the latter case, extract the system component from that package
+ try {
+ umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
+ } catch (NoComponentException e) {
+ umlSelectedComponent = analysisResultUtil.getSystemComponentFromEvent(event);
+ }
+// umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
umlSelectedResource = umlSelectedComponent.eResource();
isDiscreteTime = MessageTimeModelDialog.openQuestion(false);
showPopups = false;
usexTextValidation=true;
ossFilepath = ocraDirectoryUtil.getOSSFilePath();
- resultFilePath = ocraDirectoryUtil.getCommandCheckPropertyResultPath(umlSelectedComponent.getName());
+
+ storeResult = (event.getParameter(storeResultParam) != null &&
+ event.getParameter(storeResultParam).equals("true")) ? true : false;
+ if (storeResult) {
+ resultFilePath = FileNamesUtil.getInstance().computePropertyValidationFileName(umlSelectedComponent);
+ } else {
+ resultFilePath = ocraDirectoryUtil.getCommandCheckPropertyResultPath(umlSelectedComponent.getName());
+ }
+
+ // If requested to store the data, execute the command here, cannot be called later
+ if (storeResult) {
+ String[] conditions = new String[1]; // It will be filled by the method
+ if(ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime, usexTextValidation,showPopups,
+ ossFilepath, resultFilePath, monitor, true, conditions)) {
+
+ // Store the result
+ analysisResultUtil.storeResult(AnalysisResultUtil.PROPERTY_VALIDATION_ANALYSIS, conditions[0],
+ resultFilePath, umlSelectedComponent, null);
+
+ // Visualize the result
+ analysisResultUtil.showResult(CheckValidationProperty.FUNCTION_NAME, resultFilePath);
+ }
+ }
}
@Override
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
- ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime, usexTextValidation,showPopups,
- ossFilepath, resultFilePath, monitor);
-
+ if (!storeResult) {
+ ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime, usexTextValidation,showPopups,
+ ossFilepath, resultFilePath, monitor, false, null);
+ }
}
-
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
index b3c097457c183c0ebb75e639f3270ec651adb475..9075e9225a85ad667b353968f8759702bb07b986 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
@@ -29,7 +29,6 @@ import eu.fbk.eclipse.standardtools.utils.ui.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.utils.ui.dialogs.MessageTimeModelDialog;
import eu.fbk.eclipse.standardtools.utils.ui.utils.OCRADirectoryUtil;
import eu.fbk.tools.adapter.ocra.CheckContractCompositeImplementation;
-import eu.fbk.tools.adapter.ocra.ComputeContractFaultTree;
public class CompositeContractImplementationCommand extends AbstractJobCommand {
diff --git a/plugins/org.polarsys.chess.diagram.ui/src/org/polarsys/chess/diagram/ui/services/ResultsGeneratorService.java b/plugins/org.polarsys.chess.diagram.ui/src/org/polarsys/chess/diagram/ui/services/ResultsGeneratorService.java
index 838243103b383533fe107aa49b2ca9325c84176a..4b809c11d6d964b6d5e7e7612ed321ff5772ec11 100644
--- a/plugins/org.polarsys.chess.diagram.ui/src/org/polarsys/chess/diagram/ui/services/ResultsGeneratorService.java
+++ b/plugins/org.polarsys.chess.diagram.ui/src/org/polarsys/chess/diagram/ui/services/ResultsGeneratorService.java
@@ -55,10 +55,12 @@ import eu.fbk.eclipse.standardtools.diagram.ContractRefinementResultDescriptor;
import eu.fbk.eclipse.standardtools.diagram.DocumentGenerator;
import eu.fbk.eclipse.standardtools.diagram.FmeaResultDescriptor;
import eu.fbk.eclipse.standardtools.diagram.FtaResultDescriptor;
+import eu.fbk.eclipse.standardtools.diagram.PropertyValidationResultDescriptor;
import eu.fbk.tools.adapter.ocra.CheckContractResultBuilder;
import eu.fbk.tools.adapter.results.CheckResult;
import eu.fbk.tools.adapter.ocra.OcraOutput;
import eu.fbk.tools.adapter.results.ContractCheckResult;
+import eu.fbk.tools.adapter.results.ContractPropertyValidationResult;
import eu.fbk.tools.adapter.results.ModelCheckResult;
import eu.fbk.tools.adapter.xsap.ComputeFmeaTableResultBuilder;
import eu.fbk.tools.adapter.xsap.table.FmeaTable;
@@ -161,7 +163,6 @@ public class ResultsGeneratorService {
// System.out.println("\tcheckResult.getProofType() = " + checkResult.getProofType());
// System.out.println("\tcheckResult.getValue() = " + checkResult.getValue());
// }
-
}
return contractRefinementResultDescriptor;
@@ -222,6 +223,60 @@ public class ResultsGeneratorService {
return contractImplementationResultDescriptor;
}
+ /**
+ * Creates a PropertyValidationResultDescriptor from the given ResultElement.
+ * @param resultElement the element containing the data
+ * @return the newly created descriptor
+ */
+ private PropertyValidationResultDescriptor createPropertyValidationResultDescriptor(ResultElement resultElement) {
+ final PropertyValidationResultDescriptor propertyValidationResultDescriptor =
+ new PropertyValidationResultDescriptor();
+
+ propertyValidationResultDescriptor.rootClass = EntityUtil.getInstance().getName(resultElement.getRoot());
+
+ final File resultFile = new File(resultElement.getFile());
+ final CheckContractResultBuilder resultBuilder = new CheckContractResultBuilder();
+ final OcraOutput ocraOutput = resultBuilder.unmarshalResult(resultFile);
+ if(ocraOutput == null || ocraOutput.getOcraResult() == null || ocraOutput.getOcraResult().isEmpty()) {
+ logger.debug("Error while unmarshalling the result. For more info see the console");
+ return null;
+ }
+
+ final ModelCheckResult contractCheckResult = resultBuilder.buildResult(ocraOutput);
+ if(contractCheckResult == null) {
+ logger.debug("Internal error while building the result. For more info see the console");
+ return null;
+ }
+
+ final List<ContractPropertyValidationResult> propertyValidationResults =
+ contractCheckResult.getPropertyValidationResults();
+ for (ContractPropertyValidationResult result : propertyValidationResults) {
+ if (result.getCheckType().equals("ocra_check_validation_prop")) {
+// final String[] line = new String[2];
+// line[0] = "[" + result.getComponentType() + "] " + result.getContractName();
+// line[1] = result.getFailed()? "NOT OK": "Success";
+// propertyValidationResultDescriptor.lines.add(line);
+ }
+
+ System.out.println("\nresult.getCheckType() = " + result.getCheckType());
+ System.out.println("result.getModelName() = " + result.getModelName());
+ System.out.println("result.getName() = " + result.getName());
+
+ System.out.println("result.getFailed() = " + result.getFailed());
+
+ EList<CheckResult> checkResults = result.getCheckResults();
+ for (CheckResult checkResult : checkResults) {
+ checkResult.getContractName();
+ System.out.println("\tcheckResult.getContractName() = " + checkResult.getContractName());
+ System.out.println("\tcheckResult.getProofType() = " + checkResult.getProofType());
+ System.out.println("\tcheckResult.getValue() = " + checkResult.getValue());
+ }
+
+ }
+
+ return propertyValidationResultDescriptor;
+ }
+
/**
* Computes the EMFTA name from the given XML file.
* @param fullPath the full name of the XML file
@@ -402,6 +457,10 @@ public class ResultsGeneratorService {
rootContainer.contractRefinementResultDescriptors.clear(); // There can be only one of this kind
rootContainer.contractRefinementResultDescriptors.add(contractRefinementResultDescriptor);
}
+ } else if (resultType.equals(AnalysisResultUtil.PROPERTY_VALIDATION_ANALYSIS)) {
+ final PropertyValidationResultDescriptor propertyValidationResultDescriptor =
+ createPropertyValidationResultDescriptor(resultElement);
+ rootContainer.propertyValidationResultDescriptors.add(propertyValidationResultDescriptor);
}
//TODO: implementare anche gli altri casi...
}