Merge branch 'release/2.3.1'

.gitignore

 **/bin/
+**/target/
+.gradle/
+.metadata/
+**/pom.xml
+.DS_Store
+pom.xml
+updatesite/
+de.prob.core/prob/
+build/
+de.prob.repository/category.xml
\ No newline at end of file

README.md

+<img src="https://github.com/bendisposto/prob/raw/develop/logo.png" width="500" align="center">
+
 # The ProB Model Checker and Animator
 
 The ProB source code is distributed under the EPL license (http://www.eclipse.org/org/documents/epl-v10.html).

build.gradle

+groupID			=	"de.prob"
+features		=	["de.prob2.feature"]		// must be the same as the folder name
+
+descriptions	=	[["de.prob2.feature": "ProB Rodin Plugin"],["de.prob2.feature": """ProB is an animator and model checker for the B-Method. It allows
+fully automatic animation of many B specifications, and can be
+used to systematically check a specification for errors. 
+Part of the research and development was conducted within the
+EPSRC funded projects ABCD and iMoc, and within the EU funded
+project Rodin. 
+Development is continued under the EU funded project Deploy and
+the DFG project Gepavas. 
+ProB has been successfully used on various industrial specifications
+and is now being used within Siemens."""] ]		// label and descriptions of the features
+
+repositoryName	=	groupID+".repository"		// will be the folder name
+parentID		= 	groupID+".parent"			// will be the same as the folder name
+
+targetRepositories = ["http://cobra.cs.uni-duesseldorf.de/prob_dev_target/","http://download.eclipse.org/releases/indigo/"]		// ps Repository with Target Definition File
+
+apply from: 'tycho_build.gradle'
+
+// Local tasks
+def download(address,target) {
+	    def file = new FileOutputStream(target)
+	    def out = new BufferedOutputStream(file)
+	    out << new URL(address).openStream()
+	    out.close()
+}
+
+task downloadCli << {
+		dir = 'de.prob.core/prob/'
+		delete file(dir)
+	    new File(dir).mkdirs() 
+	
+		['leopard':'macos','linux':'linux','linux64':'linux64','win32':'windows'].each {
+		n = it.getKey()
+	
+		targetdir = dir+it.getValue()
+		targetzip = dir+"probcli_${n}.zip"
+		url = "http://nightly.cobra.cs.uni-duesseldorf.de/cli/probcli_${n}.zip"
+		download(url,targetzip)
+	    FileTree zip = zipTree(targetzip)
+	    copy {
+		   from zip
+		   into targetdir
+	    }
+		delete file(targetzip)
+	}
+
+	targetdir = dir+"windows/"
+	targetzip = targetdir+"windowslib.zip"
+	download("http://nightly.cobra.cs.uni-duesseldorf.de/cli/windowslib.zip",targetzip)
+	FileTree zip = zipTree(targetzip)
+	    copy {
+		   from zip
+		   into targetdir
+	    }
+	delete file(targetzip)
+	
+}
+
+task collectArtifacts(type:Copy) {
+	    from groupID+'.repository/target/repository/'
+	    into 'updatesite'
+}

de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF

@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: BMotion Studio Editor Plug-in
 Bundle-SymbolicName: de.bmotionstudio.gef.editor;singleton:=true
-Bundle-Version: 5.3.0
+Bundle-Version: 5.3.1.qualifier
 Bundle-Activator: de.bmotionstudio.gef.editor.BMotionEditorPlugin
 Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
  org.eclipse.ui.ide;bundle-version="[3.5.0,4.0.0)",
@@ -14,7 +14,7 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
  org.eclipse.core.databinding.beans;bundle-version="[1.1.1,2.0.0)",
  org.eclipse.gef;bundle-version="[3.7.0,4.0.0)",
  de.prob.core;bundle-version="[9.2.0,9.3.0)",
- org.eventb.core;bundle-version="[2.1.0,2.5.0)"
+ org.eventb.core;bundle-version="[2.1.0,2.6.0)"
 Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-1.6
 Eclipse-BuddyPolicy: registered

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/EditorImageRegistry.java

@@ -23,6 +23,8 @@ public class EditorImageRegistry implements IBMotionStudioImageRegistry {
 	public static final String IMG_ICON_DOWN = "icon_down";
 	public static final String IMG_ICON_CONNECTION16 = "icon_connection16";
 	public static final String IMG_ICON_CONNECTION24 = "icon_connection24";
+	public static final String IMG_ICON_NEW_WIZ = "icon_new_wiz";
+	public static final String IMG_ICON_DELETE_EDIT = "icon_delete_edit";
 
 	public static final String IMG_ICON_JPG = "icon_jpg";
 	public static final String IMG_ICON_GIF = "icon_gif";
@@ -59,6 +61,10 @@ public class EditorImageRegistry implements IBMotionStudioImageRegistry {
 				BMotionEditorPlugin.PLUGIN_ID, "icons/icon_connection16.gif");
 		BMotionStudioImage.registerImage(IMG_ICON_CONNECTION24,
 				BMotionEditorPlugin.PLUGIN_ID, "icons/icon_connection24.gif");
+		BMotionStudioImage.registerImage(IMG_ICON_NEW_WIZ, "org.eclipse.ui",
+				"$nl$/icons/full/etool16/new_wiz.gif");
+		BMotionStudioImage.registerImage(IMG_ICON_DELETE_EDIT,
+				"org.eclipse.ui", "$nl$/icons/full/etool16/delete_edit.gif");
 
 		BMotionStudioImage.registerImage(IMG_ICON_JPG,
 				BMotionEditorPlugin.PLUGIN_ID, "icons/icon_jpg.gif");

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/BMotionAbstractWizard.java

@@ -67,7 +67,8 @@ public abstract class BMotionAbstractWizard extends WizardDialog {
 	}
 
 	private Control createDeleteControl(Composite parent) {
-		return createDeleteImageButton(parent, BMotionStudioImage
+		return createDeleteImageButton(parent,
+				BMotionStudioImage
 						.getImage(EditorImageRegistry.IMG_ICON_DELETE21));
 	}
 

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/BMotionObserverWizard.java

@@ -8,6 +8,7 @@ package de.bmotionstudio.gef.editor.action;
 
 import org.eclipse.jface.dialogs.MessageDialog;
 import org.eclipse.jface.wizard.IWizard;
+import org.eclipse.swt.SWT;
 import org.eclipse.swt.widgets.Display;
 import org.eclipse.ui.IWorkbenchPart;
 
@@ -15,6 +16,7 @@ public class BMotionObserverWizard extends BMotionAbstractWizard {
 
 	public BMotionObserverWizard(IWorkbenchPart workbenchPart, IWizard newWizard) {
 		super(workbenchPart, newWizard);
+		setShellStyle(SWT.CLOSE);
 		setDeleteToolTip("Delete Observer");
 	}
 

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/ObserverAction.java

@@ -28,6 +28,7 @@ public class ObserverAction extends SelectionAction {
 	private String className;
 	private Observer clonedObserver;
 	private Observer newObserver;
+	private BControl actionControl;
 
 	public ObserverAction(IWorkbenchPart part) {
 		super(part);
@@ -44,11 +45,14 @@ public class ObserverAction extends SelectionAction {
 		return true;
 	}
 
+	@Override
 	public void run() {
 
 		clonedObserver = null;
 
-		if (getControl() != null) {
+		actionControl = getControl();
+
+		if (actionControl != null) {
 
 			newObserver = getControl().getObserver(getClassName());
 
@@ -115,7 +119,7 @@ public class ObserverAction extends SelectionAction {
 				} else if (status == WizardDialog.CANCEL) {
 
 					if (clonedObserver != null)
-						getControl().addObserver(clonedObserver);
+						actionControl.addObserver(clonedObserver);
 
 				} else if (status == BMotionObserverWizard.DELETE) {
 					RemoveObserverAction action = new RemoveObserverAction(
@@ -137,7 +141,7 @@ public class ObserverAction extends SelectionAction {
 	public ObserverCommand createObserverCommandCommand() {
 		ObserverCommand command = new ObserverCommand();
 		command.setClassName(getClassName());
-		command.setControl(getControl());
+		command.setControl(actionControl);
 		return command;
 	}
 
@@ -163,4 +167,5 @@ public class ObserverAction extends SelectionAction {
 		return null;
 
 	}
+
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/attribute/BAttributeConnection.java

@@ -6,6 +6,7 @@
 
 package de.bmotionstudio.gef.editor.attribute;
 
+import org.eclipse.jface.viewers.LabelProvider;
 import org.eclipse.ui.views.properties.PropertyDescriptor;
 
 public class BAttributeConnection extends AbstractAttribute {
@@ -16,7 +17,14 @@ public class BAttributeConnection extends AbstractAttribute {
 
 	@Override
 	public PropertyDescriptor preparePropertyDescriptor() {
-		return new PropertyDescriptor(getID(), getName());
+		PropertyDescriptor descriptor = new PropertyDescriptor(getID(),
+				getName());
+		descriptor.setLabelProvider(new LabelProvider() {
+			public String getText(Object element) {
+				return "";
+			}
+		});
+		return descriptor;
 	}
 
 	@Override

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/edit/AttributeExpressionEdittingSupport.java

@@ -16,6 +16,7 @@ import org.eclipse.ui.views.properties.PropertyDescriptor;
 import de.bmotionstudio.gef.editor.attribute.AbstractAttribute;
 import de.bmotionstudio.gef.editor.model.BControl;
 import de.bmotionstudio.gef.editor.observer.ObserverEvalObject;
+import de.bmotionstudio.gef.editor.util.WizardObserverUtil;
 
 public class AttributeExpressionEdittingSupport extends EditingSupport {
 
@@ -39,7 +40,7 @@ public class AttributeExpressionEdittingSupport extends EditingSupport {
 
 	@Override
 	protected boolean canEdit(Object element) {
-		return true;
+		return WizardObserverUtil.isEditElement(getViewer());
 	}
 
 	@Override

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/edit/OperationValueEditingSupport.java

@@ -23,6 +23,7 @@ import de.bmotionstudio.gef.editor.eventb.MachineContentObject;
 import de.bmotionstudio.gef.editor.eventb.MachineOperation;
 import de.bmotionstudio.gef.editor.model.BControl;
 import de.bmotionstudio.gef.editor.scheduler.PredicateOperation;
+import de.bmotionstudio.gef.editor.util.WizardObserverUtil;
 
 public class OperationValueEditingSupport extends EditingSupport {
 
@@ -37,7 +38,7 @@ public class OperationValueEditingSupport extends EditingSupport {
 
 	@Override
 	protected boolean canEdit(Object element) {
-		return true;
+		return WizardObserverUtil.isEditElement(getViewer());
 	}
 
 	@Override
@@ -71,4 +72,5 @@ public class OperationValueEditingSupport extends EditingSupport {
 		}
 		return cellEditor;
 	}
+
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/edit/PredicateEditingSupport.java

@@ -19,6 +19,7 @@ import org.eclipse.swt.widgets.Composite;
 import org.eclipse.swt.widgets.Shell;
 
 import de.bmotionstudio.gef.editor.model.Visualization;
+import de.bmotionstudio.gef.editor.util.WizardObserverUtil;
 
 /**
  * @author Lukas Ladenberger
@@ -54,4 +55,9 @@ public class PredicateEditingSupport extends ObservableValueEditingSupport {
 		return cellEditor;
 	}
 
+	@Override
+	protected boolean canEdit(Object element) {
+		return WizardObserverUtil.isEditElement(getViewer());
+	}
+
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/edit/TextEditingSupport.java

@@ -18,6 +18,8 @@ import org.eclipse.jface.viewers.ViewerCell;
 import org.eclipse.swt.SWT;
 import org.eclipse.swt.widgets.Composite;
 
+import de.bmotionstudio.gef.editor.util.WizardObserverUtil;
+
 public class TextEditingSupport extends ObservableValueEditingSupport {
 
 	private TextCellEditor cellEditor;
@@ -50,4 +52,9 @@ public class TextEditingSupport extends ObservableValueEditingSupport {
 		return cellEditor;
 	}
 
+	@Override
+	protected boolean canEdit(Object element) {
+		return WizardObserverUtil.isEditElement(getViewer());
+	}
+
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/figure/BMSImageFigure.java

@@ -6,27 +6,32 @@
 
 package de.bmotionstudio.gef.editor.figure;
 
-import org.eclipse.draw2d.Graphics;
+import java.io.File;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
 import org.eclipse.draw2d.ImageFigure;
 import org.eclipse.draw2d.StackLayout;
 import org.eclipse.draw2d.geometry.Rectangle;
 import org.eclipse.swt.graphics.Image;
+import org.eclipse.swt.graphics.ImageData;
+import org.eclipse.swt.graphics.ImageLoader;
+import org.eclipse.swt.widgets.Display;
 
 public class BMSImageFigure extends AbstractBMotionFigure {
 
 	private ImageFigure imageFigure;
 
+	final ImageLoader loader = new ImageLoader();
+
+	private Map<String, List<Image>> images = new HashMap<String, List<Image>>();
+	private GIFThread currentGIFThread;
+
 	public BMSImageFigure() {
 		setLayoutManager(new StackLayout());
-		imageFigure = new ImageFigure() {
-			public void paintFigure(Graphics g) {
-				if (getImage() == null)
-					return;
-				Rectangle rectangle = getClientArea();
-				g.drawImage(getImage(), new Rectangle(getImage().getBounds()),
-						rectangle);
-			}
-		};
+		imageFigure = new ImageFigure();
 		add(imageFigure);
 	}
 
@@ -34,10 +39,33 @@ public class BMSImageFigure extends AbstractBMotionFigure {
 		getParent().setConstraint(imageFigure, rect);
 	}
 
-	public void setImage(Image image) {
-		if (imageFigure.getImage() != null)
-			imageFigure.getImage().dispose();
-		imageFigure.setImage(image);
+	public void setImage(String myPath) {
+
+		if (currentGIFThread != null)
+			currentGIFThread.interrupt();
+
+		if (new File(myPath).exists()) {
+
+			loader.load(myPath);
+
+			List<Image> imgList = images.get(myPath);
+			if (imgList == null) {
+				imgList = new ArrayList<Image>();
+				for (ImageData imageData : loader.data)
+					imgList.add(new Image(Display.getDefault(), imageData));
+				images.put(myPath, imgList);
+			}
+
+			if (loader.data.length > 1) { // GIF file
+				currentGIFThread = new GIFThread(this.imageFigure, myPath,
+						imgList);
+				currentGIFThread.start();
+			} else { // Non GIF file
+				imageFigure.setImage(imgList.get(0));
+			}
+
+		}
+
 	}
 
 	/*
@@ -47,8 +75,68 @@ public class BMSImageFigure extends AbstractBMotionFigure {
 	 */
 	@Override
 	public void deactivateFigure() {
+		if (currentGIFThread != null)
+			currentGIFThread.interrupt();
 		if (imageFigure.getImage() != null)
 			imageFigure.getImage().dispose();
+		for (List<Image> l : images.values())
+			for (Image img : l)
+				img.dispose();
+	}
+
+	class GIFThread extends Thread {
+
+		ImageFigure imgFigure;
+		int imageNumber;
+		final ImageLoader loader = new ImageLoader();
+		boolean stopped = false;
+		List<Image> imgList;
+
+		public GIFThread(ImageFigure imgFigure, String imgPath,
+				List<Image> imgList) {
+			this.imgFigure = imgFigure;
+			this.imgList = imgList;
+			loader.load(imgPath);
+		}
+
+		@Override
+		public void run() {
+
+			stopped = false;
+
+			while (!stopped) {
+
+				int delayTime = loader.data[imageNumber].delayTime;
+
+				try {
+					Thread.sleep(delayTime * 10);
+				} catch (InterruptedException e) {
+					// e.printStackTrace();
+				}
+
+				Display.getDefault().asyncExec(new Runnable() {
+					public void run() {
+						// Increase the variable holding the frame
+						// number
+						imageNumber = imageNumber == loader.data.length - 1 ? 0
+								: imageNumber + 1;
+						Image image = imgList.get(imageNumber);
+						if (image != null && !image.isDisposed() && !stopped) {
+							imgFigure.setImage(image);
+						}
+					}
+				});
+
+			}
+
+		}
+
+		@Override
+		public void interrupt() {
+			stopped = true;
+			super.interrupt();
+		}
+
 	}
 
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/internal/Animation.java

@@ -157,4 +157,8 @@ public class Animation implements IAnimationListener {
 		return evaluationElement;
 	}
 
+	public Map<String, Operation> getCurrentStateOperations() {
+		return currentStateOperations;
+	}
+	
 }

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/ListenOperationByPredicate.java

@@ -63,13 +63,16 @@ public class ListenOperationByPredicate extends Observer {
 			}
 
 			String fPredicate = pop.getPredicate();
+			String fOpName = pop.getOperationName();
+
+			if (fOpName != null && fPredicate != null) {
+
+				if (animation.getCurrentStateOperations().containsKey(fOpName)) {
 
 					if (fPredicate.length() > 0) {
 						fPredicate = parseControls(fPredicate, control);
 					}
 
-			String fOpName = pop.getOperationName();
-			if (fOpName != null && fPredicate != null) {
 					try {
 						if (fPredicate.equals(""))
 							fPredicate = "1=1";
@@ -89,7 +92,8 @@ public class ListenOperationByPredicate extends Observer {
 								String strAtrVal = parseExpression(
 										attributeVal.toString(), control,
 										animation, pop);
-							String er = attributeObj.validateValue(strAtrVal, null);
+								String er = attributeObj.validateValue(
+										strAtrVal, null);
 								if (er != null) {
 									addError(
 											control,
@@ -119,9 +123,7 @@ public class ListenOperationByPredicate extends Observer {
 
 						}
 					} catch (ProBException e) {
-					addError(
-							control,
-							animation,
+						addError(control, animation,
 								"An error occurred while evaluating. Reason: "
 										+ e.getMessage());
 					} catch (BException e) {
@@ -132,6 +134,8 @@ public class ListenOperationByPredicate extends Observer {
 
 			}
 
+		}
+
 		// Restore attribute values
 		for (PredicateOperation obj : list) {
 			if (!setAttributes.contains(obj.getAttribute())) {

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/ListenOperationObject.java

@@ -13,6 +13,12 @@ public class ListenOperationObject extends BindingObject implements Cloneable {
 	private String operationName;
 	private String predicate;
 
+	public ListenOperationObject() {
+		super();
+		this.operationName = "";
+		this.predicate = "";
+	}
+
 	public ListenOperationObject clone() throws CloneNotSupportedException {
 		return (ListenOperationObject) super.clone();
 	}

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/ObserverEvalObject.java

@@ -29,6 +29,7 @@ public class ObserverEvalObject extends BindingObject implements Cloneable {
 	private transient Boolean hasError;
 
 	public ObserverEvalObject() {
+		this.isExpressionMode = false;
 	}
 
 	public ObserverEvalObject(String type, String eval, Boolean isExpressionMode) {

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/ToggleObjectCoordinates.java

@@ -6,16 +6,19 @@
 
 package de.bmotionstudio.gef.editor.observer;
 
-
 public class ToggleObjectCoordinates extends ObserverEvalObject implements
 		Cloneable {
 
 	private String bcontrol;
 	private String x;
 	private String y;
-	private Boolean animate = false;
+	private Boolean animate;
 
 	public ToggleObjectCoordinates() {
+		super();
+		this.x = "";
+		this.y = "";
+		this.animate = false;
 	}
 
 	public ToggleObjectCoordinates(String type, String bcontrol, String x,

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/observer/wizard/WizardObserverAddItemAction.java

+/** 
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, 
+ * Heinrich Heine Universitaet Duesseldorf
+ * This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) 
+ * */
+
+package de.bmotionstudio.gef.editor.observer.wizard;
+
+import org.eclipse.core.databinding.observable.list.WritableList;
+import org.eclipse.jface.action.Action;
+import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.jface.viewers.TableViewer;
+
+import de.bmotionstudio.gef.editor.BMotionStudioImage;
+
+public class WizardObserverAddItemAction extends Action {
+
+	private TableViewer viewer;
+	private Class<?> itemClass;
+
+	public WizardObserverAddItemAction(TableViewer viewer, Class<?> itemClass) {
+		this.viewer = viewer;
+		this.itemClass = itemClass;
+		setText("Add new item");
+		setImageDescriptor(BMotionStudioImage.getImageDescriptor(
+				"org.eclipse.ui", "$nl$/icons/full/etool16/new_wiz.gif"));
+	}
+
+	@Override
+	public void run() {
+
+		try {
+			IStructuredSelection sel = (IStructuredSelection) viewer
+					.getSelection();
+			Object firstElement = sel.getFirstElement();
+			WritableList list = (WritableList) viewer.getInput();
+			int indexOf = list.size();
+			if (firstElement != null)
+				indexOf = list.indexOf(firstElement) + 1;
+			Object newInstance = itemClass.newInstance();
+			list.add(indexOf, newInstance);
+		} catch (InstantiationException e) {
+			e.printStackTrace();
+		} catch (IllegalAccessException e) {
+			e.printStackTrace();
+		}
+
+	}
+
+}