diff --git a/org.polarsys.chess.smvExport/src/org/polarsys/chess/smvExport/services/SmvExportService.java b/org.polarsys.chess.smvExport/src/org/polarsys/chess/smvExport/services/SmvExportService.java
index c2a805cf510497901a6353f47345dfb2e7d208c5..2af1d7690a79061a09eac33360b23308b83bffae 100644
--- a/org.polarsys.chess.smvExport/src/org/polarsys/chess/smvExport/services/SmvExportService.java
+++ b/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));
+ }
}
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/CompositeContractImplementationCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/CompositeContractImplementationCommand.java
index 5b97b198f853ca0650fd20b207fc7658b0b0d93d..7826047bc8823e5d7013b54e738203509e2a674e 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/CompositeContractImplementationCommand.java
+++ b/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());
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 67b695fb609bfa7bc952039bd86a363c2d583db7..99380a3c90bb077a37c5030dc88cc9c5f64d64dc 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
@@ -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);
}
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 93f6848d85d1e9d67d2b0d7cf0b38ae6fc6e2c80..018643c9b97500012d2ad4b0e87a6e29250251a8 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
@@ -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);
}
}
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 ddab6b99e43a3190fdeb664206961906dd2694c9..956bff1a9f02ec8450412e79d090af47e8d8e2a1 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
@@ -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);
}