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 a97c53e098f0b4c67b72c1df9b75ee87745e53ee..d25084c8bf1419b8bddb2b88ad4309c6b47d8611 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
@@ -63,7 +63,8 @@ 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";
+ public static final String PROPERTY_VALIDATION_ANALYSIS = "PROP_VAL";
+ public static final String CONTRACT_PROPERTY_VALIDATION_ANALYSIS = "CONT_PROP_VAL";
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 724de08e69705e0fa294845f497856469afbd7d9..b11b0502cb4436a8046718c7c2e9d7d6585ca562 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
@@ -242,4 +242,15 @@ public class FileNamesUtil {
return resPath + File.separator + computeQualifiedName(systemComponent) + "_" +
AnalysisResultUtil.PROPERTY_VALIDATION_ANALYSIS + "_" + getDate() + XML_EXT;
}
+
+ /**
+ * Computes the file name for the Contract Property Validation analysis.
+ * @param systemComponent the root component of the analysis
+ * @return
+ */
+ public String computeContractPropertyValidationFileName(Class systemComponent) {
+ final String resPath = analysisResultUtil.getResultDir();
+ return resPath + File.separator + computeQualifiedName(systemComponent) + "_" +
+ AnalysisResultUtil.CONTRACT_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 02d0ac7d41fe8eaef5aa884b655733609aa2493e..cf32dccc0022d9ea4e9c6c3acd98e8e7a58577bb 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
@@ -147,6 +147,16 @@
name="store_result"
value="true">
</parameter>
+ </command>
+ <command
+ commandId="org.polarsys.chess.verificationService.commands.CheckValidationPropertyCommand2"
+ icon="icons/contract_verification.png"
+ label="Check Validation on Assumption/Guarantee Properties"
+ style="push">
+ <parameter
+ name="store_result"
+ value="true">
+ </parameter>
</command>
</menu>
</menuContribution>
@@ -356,6 +366,11 @@
defaultHandler="org.polarsys.chess.verificationService.ui.commands.CheckValidationContractPropertyCommand"
id="org.polarsys.chess.verificationService.commands.CheckValidationPropertyCommand2"
name="Check Validation on Assumption/Guarantee Properties on selected component">
+ <commandParameter
+ id="store_result"
+ name="storeResult"
+ optional="true">
+ </commandParameter>
</command>
<command
defaultHandler="org.polarsys.chess.verificationService.ui.commands.debug.CheckValidationPropertyOnFileCommand"
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 dfe9ffadfc4db8c8b857a8463e45783651cf4a3c..8249c34c73560cc3fcc185627f58cdc4129141b8 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
@@ -81,12 +81,13 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand
// 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)) {
+ 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);
+ analysisResultUtil.storeResult(AnalysisResultUtil.PROPERTY_VALIDATION_ANALYSIS,
+ conditions[0], resultFilePath, umlSelectedComponent, null);
// Visualize the result
analysisResultUtil.showResult(CheckValidationProperty.FUNCTION_NAME, resultFilePath);
@@ -98,8 +99,8 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
if (!storeResult) {
- ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime, usexTextValidation,showPopups,
- ossFilepath, resultFilePath, monitor, false, null);
+ 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/CheckValidationContractPropertyCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java
index 52143da4eec5180eee8d0b0a081ff98ddee804ff..e473f5f125a02684d4feb6c1699d3cda572ae104 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.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,6 +36,7 @@ public class CheckValidationContractPropertyCommand extends AbstractJobCommand {
private OCRAExecService ocraExecService = OCRAExecService.getInstance(chessToOCRAModelTranslator);
private SelectionUtil selectionUtil = SelectionUtil.getInstance();
private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
+ private AnalysisResultUtil analysisResultUtil = AnalysisResultUtil.getInstance();
public CheckValidationContractPropertyCommand() {
super("Check Validation Property");
@@ -44,25 +49,58 @@ public class CheckValidationContractPropertyCommand 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().computeContractPropertyValidationFileName(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.executeValidationContractProperty(umlSelectedComponent, umlSelectedResource,
+ isDiscreteTime, usexTextValidation,showPopups, ossFilepath, resultFilePath,
+ monitor, true, conditions)) {
+
+ // Store the result
+ analysisResultUtil.storeResult(AnalysisResultUtil.CONTRACT_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.executeValidationContractProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime, usexTextValidation,showPopups,
- ossFilepath, resultFilePath, monitor, false);
-
+ if (!storeResult) {
+ ocraExecService.executeValidationContractProperty(umlSelectedComponent, umlSelectedResource, isDiscreteTime,
+ usexTextValidation, showPopups, ossFilepath, resultFilePath, monitor, false, null);
+ }
}
-
}
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 f0a9f7f2439dabbc07ca998b9f9ebd7bcfbbec70..c570502080ebf93720c0ed895a340656acba3208 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
@@ -234,14 +234,9 @@ public class ResultsGeneratorService {
propertyValidationResultDescriptor.rootClass = EntityUtil.getInstance().getName(resultElement.getRoot());
- final String conditions = resultElement.getConditions();
-
+ // Parse the string containing the analysis details
+ final String conditions = resultElement.getConditions();
final String[] partials = conditions.split("#");
-
- for (String string : partials) {
- System.out.println("partial = " + string);
- }
-
propertyValidationResultDescriptor.validationType = partials[0];
if (partials.length > 1) {
propertyValidationResultDescriptor.selectedComponent = partials[1];
@@ -284,26 +279,23 @@ public class ResultsGeneratorService {
line[1] = "Unknown";
} else {
line[1] = checkValue;
- }
-
+ }
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());
- }
-
+// 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;
@@ -494,6 +486,10 @@ public class ResultsGeneratorService {
final PropertyValidationResultDescriptor propertyValidationResultDescriptor =
createPropertyValidationResultDescriptor(resultElement);
rootContainer.propertyValidationResultDescriptors.add(propertyValidationResultDescriptor);
+ } else if (resultType.equals(AnalysisResultUtil.CONTRACT_PROPERTY_VALIDATION_ANALYSIS)) {
+ final PropertyValidationResultDescriptor contractPropertyValidationResultDescriptor =
+ createPropertyValidationResultDescriptor(resultElement);
+ rootContainer.contractPropertyValidationResultDescriptors.add(contractPropertyValidationResultDescriptor);
}
//TODO: implementare anche gli altri casi...
}