From 76e7de69d6d5873eae2a5d16b4f779caed2c3c66 Mon Sep 17 00:00:00 2001
From: Alberto Debiasi <adebiasi@fbk.eu>
Date: Tue, 6 Feb 2018 11:25:15 +0100
Subject: [PATCH] updates on verification commands
Change-Id: I759e41622ebb2e9902bcfe826cee5cdfe00a22c5
Signed-off-by: Alberto Debiasi <adebiasi@fbk.eu>
---
.../ContractImplementationCommand.java | 4 +-
.../commands/ExportModelToFileCommand.java | 2 +
.../commands/ModelCheckingCommand.java | 5 ++-
.../debug/ModelCheckingOnFileCommand.java | 41 ++++++++++++++-----
4 files changed, 38 insertions(+), 14 deletions(-)
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java
index 11ce86be5..2a369a40b 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java
@@ -32,7 +32,7 @@ public class ContractImplementationCommand extends AbstractJobCommand {
private OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
private SelectionUtil selectionUtil = SelectionUtil.getInstance();
//private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
- private SmvExportService nuXmvService = SmvExportService.getInstance();
+ private SmvExportService smvExportService = SmvExportService.getInstance();
private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
private NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
@@ -64,7 +64,7 @@ public class ContractImplementationCommand extends AbstractJobCommand {
@Override
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
- File smvOutput = nuXmvService.exportSmv(umlSelectedComponent, showPopups,smvFilePath,monitor);
+ File smvOutput = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
ocraExecService.executeCheckContractImplementation(umlSelectedComponent,umlSelectedResource, smvOutput, isDiscreteTime,showPopups,ossFilepath,resultFilePath,monitor);
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ExportModelToFileCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ExportModelToFileCommand.java
index 8bf5f682b..16b328c7a 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ExportModelToFileCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ExportModelToFileCommand.java
@@ -65,6 +65,8 @@ public class ExportModelToFileCommand extends AbstractJobCommand {
ocraTranslatorService.exportModelToOssFile(umlSelectedComponent, umlSelectedResource,
isDiscreteTime,showPopups,ossFilepath, monitor);
+
+
}
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java
index f67091330..020132c0e 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java
@@ -21,6 +21,7 @@ import org.polarsys.chess.smvExport.services.SmvExportService;
//import org.polarsys.chess.verificationService.services.SmvExportService;
import eu.fbk.eclipse.standardtools.commands.AbstractJobCommand;
+import eu.fbk.eclipse.standardtools.dialogs.MessageTimeModelDialog;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvService;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
@@ -42,12 +43,14 @@ public class ModelCheckingCommand extends AbstractJobCommand {
private Class umlSelectedComponent;
private boolean showPopups;
private String smvFilePath;
+ private String resultFilePath;
@Override
public void execGUIOperations(ExecutionEvent event,IProgressMonitor monitor) throws Exception {
umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
showPopups = true;
smvFilePath = nuXmvDirectoryUtil.getSmvFilePath();
+ resultFilePath = nuXmvDirectoryUtil.getCommandModelCheckingResultPath(umlSelectedComponent.getName());
}
@@ -56,7 +59,7 @@ public class ModelCheckingCommand extends AbstractJobCommand {
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
File smvOutput = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
- nuXmvService.executeModelChecking(smvOutput);
+ nuXmvService.executeModelChecking(smvOutput,resultFilePath);
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java
index 6e7634da3..2cbb06715 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java
@@ -15,7 +15,8 @@ import java.io.File;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.runtime.IProgressMonitor;
-import eu.fbk.eclipse.standardtools.commands.AbstractAsyncJobCommand;
+
+import eu.fbk.eclipse.standardtools.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.nuXmvService.dialogs.NuXmvParametersDialog;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvService;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDialogUtil;
@@ -25,7 +26,7 @@ import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
*
*
*/
-public class ModelCheckingOnFileCommand extends AbstractAsyncJobCommand {
+public class ModelCheckingOnFileCommand extends AbstractJobCommand {
private NuXmvService nuXmvService = NuXmvService.getInstance();
@@ -36,22 +37,40 @@ public class ModelCheckingOnFileCommand extends AbstractAsyncJobCommand {
super("Model Checking");
}
+ boolean goAhead = false;
+ String alg_type;
+ String check_type;
+ String property;
+
@Override
- public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
-
- File smvFile = nuXmvDialogUtil.getSmvFileFromFileDialog(nuXmvDirectoryUtil.getSmvFilePath());
+ public void execGUIOperations(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
+
//boolean isDiscreteTime = MessageTimeModelDialog.openQuestion();
final NuXmvParametersDialog dialog = new NuXmvParametersDialog();
dialog.open();
-
- if (dialog.goAhead()) {
- String alg_type = dialog.getAlgorithmType();
- String check_type = dialog.getCheckType();
- String property = dialog.getProperty();
- nuXmvService.modelCheckingCommand(smvFile, property, alg_type, check_type);
+
+ goAhead = dialog.goAhead();
+
+ if (goAhead) {
+ alg_type = dialog.getAlgorithmType();
+ check_type = dialog.getCheckType();
+ property = dialog.getProperty();
+
}
+ }
+
+ @Override
+ public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
+
+ if (goAhead) {
+
+ File smvFile = nuXmvDialogUtil.getSmvFileFromFileDialog(nuXmvDirectoryUtil.getSmvFilePath());
+ String resultFilePath = nuXmvDirectoryUtil.getCommandModelCheckingResultPath(smvFile.getName());
+ nuXmvService.modelCheckingCommand(smvFile, property, alg_type, check_type,resultFilePath);
+ }
+
}
--
GitLab