updates on verification commands

Change-Id: I759e41622ebb2e9902bcfe826cee5cdfe00a22c5
Signed-off-by: Alberto Debiasi <adebiasi@fbk.eu>

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

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);
+	
+	
 	}
 
 }

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

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);
+		}
+			
 
 		}