Add block2k2 command, update UMLStateMachineModel.
Change-Id: I024fa883ac0106d1d316cb5e6a8c746b531d8142
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml b/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
index 3bb458a..cb3e6cf 100644
--- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
@@ -14,6 +14,11 @@
icon="icons/export.gif"
style="push">
</command>
+ <command
+ commandId="org.polarsys.chess.verificationService.commands.ExportBlockToK2FileCommand"
+ icon="icons/export.gif"
+ style="push">
+ </command>
</menu>
<menu
id="org.eclipse.ui.main.diagramEditorMenu.CHESS.validation"
@@ -371,5 +376,10 @@
optional="true">
</commandParameter>
</command>
+ <command
+ defaultHandler="org.polarsys.chess.verificationService.ui.commands.ExportBlockToK2FileCommand"
+ id="org.polarsys.chess.verificationService.commands.ExportBlockToK2FileCommand"
+ name="Export block as .k2 file">
+ </command>
</extension>
</plugin>
diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ExportBlockToK2FileCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ExportBlockToK2FileCommand.java
new file mode 100644
index 0000000..ea693c0
--- /dev/null
+++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ExportBlockToK2FileCommand.java
@@ -0,0 +1,68 @@
+/*******************************************************************************
+ * Copyright (C) 2017 Fondazione Bruno Kessler.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * Alberto Debiasi - initial API and implementation
+ ******************************************************************************/
+/**
+ *
+ */
+package org.polarsys.chess.verificationService.ui.commands;
+
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.core.runtime.NullProgressMonitor;
+import org.eclipse.uml2.uml.Class;
+
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.ui.services.K2ExportServiceUI;
+import eu.fbk.eclipse.standardtools.utils.ui.commands.AbstractJobCommand;
+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;
+
+/**
+ *
+ *
+ */
+public class ExportBlockToK2FileCommand extends AbstractJobCommand {
+
+ private SelectionUtil selectionUtil = SelectionUtil.getInstance();
+ private K2ExportServiceUI k2ExportService = K2ExportServiceUI
+ .getInstance(ChessSystemModel.getInstance(),UMLStateMachineModel.getInstance());
+ private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
+
+ public ExportBlockToK2FileCommand() {
+ super("Export Model To .K2 File");
+ }
+
+ private String ossFilepath;
+ private boolean showPopups;
+ private Class umlSelectedComponent;
+
+ @Override
+ public void execPreJobOperations(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
+ umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
+ ossFilepath = ocraDirectoryUtil.getOSSDirPath();
+ showPopups = true;
+ }
+
+ @Override
+ public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
+
+ k2ExportService.exportSingleBlock(umlSelectedComponent, showPopups, ossFilepath, monitor);
+
+ }
+
+ @Override
+ public void execPostJobOperations(ExecutionEvent event, NullProgressMonitor nullProgressMonitor) throws Exception {
+ // TODO Auto-generated method stub
+
+ }
+
+}
diff --git a/plugins/org.polarsys.chess.service/src/org/polarsys/chess/service/core/model/UMLStateMachineModel.java b/plugins/org.polarsys.chess.service/src/org/polarsys/chess/service/core/model/UMLStateMachineModel.java
index c417a1c..eaa93a6 100644
--- a/plugins/org.polarsys.chess.service/src/org/polarsys/chess/service/core/model/UMLStateMachineModel.java
+++ b/plugins/org.polarsys.chess.service/src/org/polarsys/chess/service/core/model/UMLStateMachineModel.java
@@ -16,7 +16,6 @@
import org.eclipse.emf.common.util.EList;
import org.eclipse.papyrus.sysml.portandflows.FlowDirection;
import org.eclipse.papyrus.uml.tools.model.UmlModel;
-import org.eclipse.uml2.uml.Constraint;
import org.eclipse.uml2.uml.Element;
import org.eclipse.uml2.uml.Port;
import org.eclipse.uml2.uml.Property;
@@ -242,4 +241,23 @@
public EList<String> getNonInitTransitionsNameList(Object stateMachine) throws Exception {
return entityUtil.getTransitionNameList(entityUtil.getNonInitialTransitions((StateMachine) stateMachine));
}
+
+ @Override
+ public EList<?> getNonInitStates(Object stateMachine) {
+ EList<Object> states = new BasicEList<Object>();
+ states.addAll(entityUtil.getIntermediateStates((StateMachine)stateMachine));
+ return states;
+ }
+
+ @Override
+ public EList<?> getInitStates(Object stateMachine) {
+ EList<Object> initStates = new BasicEList<Object>();
+ initStates.add(entityUtil.getInitialState((StateMachine)stateMachine));
+ return initStates;
+ }
+
+ @Override
+ public EList<?> getOutTransitions(Object state) {
+ return entityUtil.getOutgoingTransitions((Vertex) state);
+ }
}
