diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/META-INF/MANIFEST.MF b/plugins/contracts/org.polarsys.chess.contracts.verificationService/META-INF/MANIFEST.MF
index c84d8a1173c4897640c3c8b52fddba1a7018d29c..9e7810489d7d54e6ad64ef9d72d77294969f4702 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/META-INF/MANIFEST.MF
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/META-INF/MANIFEST.MF
@@ -20,7 +20,8 @@ Require-Bundle: org.eclipse.core.resources,
  org.polarsys.chess.core,
  org.polarsys.chess.smvExporter,
  org.polarsys.chess.service,
- eu.fbk.eclipse.standardtools.xtextService
+ eu.fbk.eclipse.standardtools.xtextService,
+ eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv
 Import-Package: eu.fbk.eclipse.standardtools.nuXmvService.ui.dialogs,
  eu.fbk.eclipse.standardtools.nuXmvService.ui.services,
  eu.fbk.eclipse.standardtools.nuXmvService.ui.utils,
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
index 912cccd9fa57e6ce3f89b16668f60bdb1aa59135..c414def729baa1ce142c311f93c5067791bc5d73 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CompositeContractImplementationCommand.java
@@ -16,10 +16,11 @@ import org.eclipse.core.runtime.IProgressMonitor;
 import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.uml2.uml.Class;
 import org.polarsys.chess.service.core.model.ChessSystemModel;
+import org.polarsys.chess.service.core.model.UMLStateMachineModel;
 import org.polarsys.chess.service.gui.utils.SelectionUtil;
-import org.polarsys.chess.smvExporter.ui.services.SmvExportServiceUI;
 
 import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.ui.services.SmvExportServiceUI;
 import eu.fbk.eclipse.standardtools.nuXmvService.ui.utils.NuXmvDirectoryUtil;
 import eu.fbk.eclipse.standardtools.utils.ui.commands.AbstractJobCommand;
 import eu.fbk.eclipse.standardtools.utils.ui.dialogs.MessageTimeModelDialog;
@@ -29,7 +30,7 @@ public class CompositeContractImplementationCommand extends AbstractJobCommand {
 
 	private OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
 	private SelectionUtil selectionUtil = SelectionUtil.getInstance();
-	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance();
+	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());
 	private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
 	private NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
 
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ContractImplementationCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ContractImplementationCommand.java
index 1fcae0c6379709d1ba29176ece25ddb684e7ab5d..5a4a023baeff7696b489918ea7935bd7c59a0cad 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ContractImplementationCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ContractImplementationCommand.java
@@ -16,14 +16,15 @@ import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.uml2.uml.Class;
 
 import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.ui.services.SmvExportServiceUI;
 import eu.fbk.eclipse.standardtools.nuXmvService.ui.utils.NuXmvDirectoryUtil;
 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 org.polarsys.chess.service.core.model.ChessSystemModel;
+import org.polarsys.chess.service.core.model.UMLStateMachineModel;
 import org.polarsys.chess.service.gui.utils.SelectionUtil;
-import org.polarsys.chess.smvExporter.ui.services.SmvExportServiceUI;
 
 public class ContractImplementationCommand extends AbstractJobCommand {
 
@@ -31,7 +32,7 @@ public class ContractImplementationCommand extends AbstractJobCommand {
 	private SelectionUtil selectionUtil = SelectionUtil.getInstance();
 	// private OCRADirectoryUtil ocraDirectoryUtil =
 	// OCRADirectoryUtil.getInstance();
-	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance();
+	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());
 	private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
 	private NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
 
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java
index 55ac37d34ec2d39bc310e65bb001a81f1434a695..91641af8a6e1b809241eba0c04de12204b27a219 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java
@@ -15,14 +15,16 @@ import java.util.HashMap;
 import org.apache.log4j.Logger;
 import org.eclipse.core.commands.ExecutionEvent;
 import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.emf.common.util.EList;
 import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.uml2.uml.Class;
 import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil;
 import org.polarsys.chess.service.core.model.ChessSystemModel;
+import org.polarsys.chess.service.core.model.UMLStateMachineModel;
 import org.polarsys.chess.service.gui.utils.SelectionUtil;
-import org.polarsys.chess.smvExporter.ui.services.SmvExportServiceUI;
 
 import eu.fbk.eclipse.standardtools.ExecOcraCommands.ui.services.OCRAExecService;
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.ui.services.SmvExportServiceUI;
 import eu.fbk.eclipse.standardtools.nuXmvService.ui.services.NuXmvExecService;
 import eu.fbk.eclipse.standardtools.nuXmvService.ui.utils.NuXmvDirectoryUtil;
 import eu.fbk.eclipse.standardtools.utils.ui.commands.AbstractJobCommand;
@@ -38,7 +40,7 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 	private static final Logger logger = Logger.getLogger(ModelCheckingCommand.class);
 
 	private SelectionUtil selectionUtil = SelectionUtil.getInstance();
-	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance();
+	private SmvExportServiceUI smvExportService = SmvExportServiceUI.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());
 	private NuXmvExecService nuXmvExecService = NuXmvExecService.getInstance();
 	private static NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
 	private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
@@ -110,7 +112,7 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 		// CommandBuilder.build("org.polarsys.chess.verificationService.commands.TestCommand2");
 		// checkContractImplementation.execute();
 
-		if (smvExportService.isLeafComponent(umlSelectedComponent)) {
+		if (isLeafComponent(umlSelectedComponent)) {
 			generatedSmvFilePath = smvExportService.exportSingleSmv(umlSelectedComponent, showPopups, smvFileDirectory,
 					monitor);
 		} else {
@@ -132,4 +134,10 @@ public class ModelCheckingCommand extends AbstractJobCommand {
 		logger.debug("executeModelChecking done");
 	}
 
+	
+	
+	private boolean isLeafComponent(Class umlSelectedComponent) {
+		EList<org.eclipse.uml2.uml.Property> subComponents = ChessSystemModel.getInstance().getSubComponentsInstances(umlSelectedComponent);
+		return ((subComponents == null) || (subComponents.size() == 0));
+	}
 }
diff --git a/plugins/org.polarsys.chess.service/META-INF/MANIFEST.MF b/plugins/org.polarsys.chess.service/META-INF/MANIFEST.MF
index 5eb829da704b3a6d88084fe82e495f466df34492..82bbd6695dbd8e056f07457a5838b77e06377192 100644
--- a/plugins/org.polarsys.chess.service/META-INF/MANIFEST.MF
+++ b/plugins/org.polarsys.chess.service/META-INF/MANIFEST.MF
@@ -17,7 +17,8 @@ Require-Bundle: org.eclipse.core.runtime,
  org.eclipse.papyrus.cdo.core;bundle-version="1.2.0",
  org.eclipse.papyrus.uml.tools,
  eu.fbk.eclipse.standardtools.utils,
- org.polarsys.chess.contracts.profile
+ org.polarsys.chess.contracts.profile,
+ eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv
 Bundle-RequiredExecutionEnvironment: JavaSE-1.7
 Export-Package: org.polarsys.chess.service.core.exceptions,
  org.polarsys.chess.service.core.model,