Small changes on v&v tool interaction commands

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

org.polarsys.chess.smvExport/src/org/polarsys/chess/smvExport/services/SmvExportService.java

@@ -13,8 +13,10 @@ package org.polarsys.chess.smvExport.services;
 import java.io.File;
 import java.util.HashMap;
 import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.emf.common.util.EList;
 import org.eclipse.papyrus.uml.tools.model.UmlModel;
 import org.eclipse.uml2.uml.Class;
+import org.eclipse.uml2.uml.Property;
 import org.polarsys.chess.service.internal.model.ChessSystemModel;
 import org.polarsys.chess.smvExport.model.UMLStateMachineModel;
 import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.services.SMVTranslatorService;
@@ -23,8 +25,9 @@ import eu.fbk.eclipse.standardtools.utils.DialogUtil;
 public class SmvExportService {
 
 	private static SmvExportService instance;
-
-	private SMVTranslatorService smvTranslatorService = SMVTranslatorService.getInstance(ChessSystemModel.getInstance(),
+private  ChessSystemModel chessSystemModel = ChessSystemModel.getInstance();
+	
+	private SMVTranslatorService smvTranslatorService = SMVTranslatorService.getInstance(chessSystemModel,
 			UMLStateMachineModel.getInstance());
 	private DialogUtil dialogUtil = DialogUtil.getInstance();
 
@@ -58,7 +61,7 @@ public class SmvExportService {
 
 	}
 
-	public File exportSingleSmv(Class umlSelectedComponent, boolean showPopups, String selectedDirectory,
+	public String exportSingleSmv(Class umlSelectedComponent, boolean showPopups, String selectedDirectory,
 			IProgressMonitor monitor) throws Exception {
 
 		File smvFile = smvTranslatorService.exportSingleSmv(umlSelectedComponent, showPopups, selectedDirectory,
@@ -68,7 +71,7 @@ public class SmvExportService {
 			dialogUtil.showMessage_ExportBehaviourDone(smvFile.getAbsolutePath());
 		}
 
-		return smvFile;
+		return smvFile.getPath();
 
 	}
 
@@ -86,5 +89,9 @@ public class SmvExportService {
 
 	}
 
+	public boolean isLeafComponent(Class umlSelectedComponent){
+		EList<Property> subComponents = chessSystemModel.getSubComponentsInstances(umlSelectedComponent);
+		return ((subComponents==null)||(subComponents.size()==0));
+	}
 	
 }

plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/CompositeContractImplementationCommand.java

@@ -39,7 +39,7 @@ public class CompositeContractImplementationCommand extends AbstractJobCommand {
 		 umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
 		 umlSelectedResource = umlSelectedComponent.eResource();
 		 isDiscreteTime = MessageTimeModelDialog.openQuestion();
-		 showPopups = true;
+		 showPopups = false;
 		 smvMapFilepath = ocraDirectoryUtil.getSmvMapFilePath();
 		 smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
 		 resultFilePath = ocraDirectoryUtil.getCommandCheckImplementationResultPath(umlSelectedComponent.getName());			

plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java

@@ -10,7 +10,7 @@
  ******************************************************************************/
 package org.polarsys.chess.verificationService.commands;
 
-import java.io.File;
+
 
 import org.eclipse.core.commands.ExecutionEvent;
 import org.eclipse.core.runtime.IProgressMonitor;
@@ -45,7 +45,7 @@ public class ContractImplementationCommand extends AbstractJobCommand {
 	private boolean isDiscreteTime;
 	private boolean showPopups;
 	private String ossFilepath;
-	private String smvFilePath;
+	private String smvFileDirectory;
 	private String resultFilePath;
 	
 	@Override
@@ -53,9 +53,9 @@ public class ContractImplementationCommand extends AbstractJobCommand {
 		 umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
 		 umlSelectedResource = umlSelectedComponent.eResource();
 		 isDiscreteTime = MessageTimeModelDialog.openQuestion();
-		 showPopups = true;
+		 showPopups = false;
 		 ossFilepath = ocraDirectoryUtil.getOSSFilePath();
-		 smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
+		 smvFileDirectory = nuXmvDirectoryUtil.getSmvFileDirectory();
 		 resultFilePath = ocraDirectoryUtil.getCommandCheckImplementationResultPath(umlSelectedComponent.getName());			
 	}
 
@@ -64,8 +64,8 @@ public class ContractImplementationCommand extends AbstractJobCommand {
 	@Override
 	public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
 		
-		File smvOutput = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
-		ocraExecService.executeCheckContractImplementation(umlSelectedComponent,umlSelectedResource, smvOutput, isDiscreteTime,showPopups,ossFilepath,resultFilePath,monitor);
+		String smvOutputPath = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFileDirectory, monitor);
+		ocraExecService.executeCheckContractImplementation(umlSelectedComponent,umlSelectedResource, smvOutputPath, isDiscreteTime,showPopups,ossFilepath,resultFilePath,monitor);
 
 	}
 

plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java

@@ -10,7 +10,7 @@
  ******************************************************************************/
 package org.polarsys.chess.verificationService.commands;
 
-import java.io.File;
+
 import java.util.HashMap;
 
 import org.eclipse.core.commands.ExecutionEvent;
@@ -49,7 +49,7 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 
 	private Class umlSelectedComponent;
 	private boolean showPopups;
-	private String smvFilePath;
+	private String smvFileDirectory;
 	private boolean isDiscreteTime;
 	private String monolithicSMVFilePath;
 	private String resultFilePath;
@@ -60,9 +60,9 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 	public void execPreJobOperations(ExecutionEvent event,IProgressMonitor monitor) throws Exception {
 		 umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
 		 umlSelectedResource = umlSelectedComponent.eResource();
-		 showPopups = true;
+		 showPopups = false;
 		 isDiscreteTime = MessageTimeModelDialog.openQuestion();
-		 smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
+		 smvFileDirectory = nuXmvDirectoryUtil.getSmvFileDirectory();
 		 monolithicSMVFilePath = nuXmvDirectoryUtil.getMonolithicSMVFilePath(umlSelectedComponent.getName());
 		 resultFilePath = nuXmvDirectoryUtil.getModelCheckingResultPath(umlSelectedComponent.getName());
 		  smvMapFilepath = ocraDirectoryUtil.getSmvMapFilePath();
@@ -73,12 +73,18 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 	@Override
 	public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
 	
-		//File smvOutput = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
+		String generatedSmvFilePath;
+		
+		if(smvExportService.isLeafComponent(umlSelectedComponent)){
+			generatedSmvFilePath = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFileDirectory, monitor);
+		}else{
+			HashMap<String,String> smvPathComponentNameMap = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFileDirectory, monitor);		
+			ocraExecService.createMonolithicSMV(umlSelectedComponent, umlSelectedResource, smvPathComponentNameMap, isDiscreteTime, showPopups, smvMapFilepath, monolithicSMVFilePath, monitor);
+			generatedSmvFilePath = monolithicSMVFilePath;
+		}
 		//nuXmvExecService.executeModelChecking(smvOutput,resultFilePath);
 		
-		HashMap<String,String> smvPathComponentNameMap = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);		
-		ocraExecService.createMonolithicSMV(umlSelectedComponent, umlSelectedResource, smvPathComponentNameMap, isDiscreteTime, showPopups, smvMapFilepath, monolithicSMVFilePath, monitor);
-		nuXmvExecService.executeModelChecking(new File(monolithicSMVFilePath),resultFilePath);
+		nuXmvExecService.executeModelChecking(generatedSmvFilePath,resultFilePath);
 		}
 
 }

plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java

@@ -68,7 +68,7 @@ public class ModelCheckingOnFileCommand extends AbstractJobCommand {
 			
 			File smvFile = nuXmvDialogUtil.getSmvFileFromFileDialog(nuXmvDirectoryUtil.getSmvFileDirectory());
 			String resultFilePath = nuXmvDirectoryUtil.getModelCheckingResultPath(smvFile.getName());
-		nuXmvService.modelCheckingCommand(smvFile, property, alg_type, check_type,resultFilePath);
+		nuXmvService.modelCheckingCommand(smvFile.getPath(), property, alg_type, check_type,resultFilePath);
 		}