Skip to content
Snippets Groups Projects
Commit f941b822 authored by Luca Cristoforetti's avatar Luca Cristoforetti
Browse files

Implemented Assume/Guarantee check report.

parent bcd46648
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 100 additions and 38 deletions
plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/AnalysisResultUtil.java
+ 2
− 1
View file @ f941b822
......@@ -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();
......
plugins/contracts/org.polarsys.chess.contracts.transformations/src/org/polarsys/chess/contracts/transformations/utils/FileNamesUtil.java
+ 11
− 0
View file @ f941b822
......@@ -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;
}
}
plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
+ 15
− 0
View file @ f941b822
......@@ -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"
......
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java
+ 7
− 6
View file @ f941b822
......@@ -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);
}
}
}
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java
+ 45
− 7
View file @ f941b822
......@@ -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);
}
}
}
plugins/org.polarsys.chess.diagram.ui/src/org/polarsys/chess/diagram/ui/services/ResultsGeneratorService.java
+ 20
− 24
View file @ f941b822
......@@ -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...
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent