Merge branch 'develop'

.gitattributes

+# Declare files that will always have LF line endings on checkout.
+*.sh text eol=lf
+gradlew text eol=lf
+
+# Declare files that will always have CRLF line endings on checkout.
+*.{bat,[bB][aA][tT]} text eol=crlf
+*.{cmd,[cC][mM][dD]} text eol=crlf

.gitignore

 **/bin/
 **/target/
+.idea/
 .gradle/
 .metadata/
 **/pom.xml
@@ -9,4 +10,3 @@ updatesite/
 **/lib/dependencies/
 de.prob.core/prob/
 build/
\ No newline at end of file
-de.prob.repository/category.xml
\ No newline at end of file

.gitlab-ci.yml

@@ -6,13 +6,14 @@ build:
   before_script:
     - mvn --version
   script:
-    - ./gradlew prepareMaven
+    - ./gradlew --no-daemon --warning-mode=all prepareMaven
     - mvn -Dmaven.repo.local="$CI_PROJECT_DIR/maven_repo_local" -f de.prob.parent/pom.xml install
     - cp footer.html de.prob.repository/target/repository/
   cache:
     paths:
       - .gradle/caches
       - .gradle/native
+      - .gradle/notifications
       - .gradle/wrapper
       - maven_repo_local
   artifacts:

README.md

-<img src="https://github.com/hhu-stups/prob-rodinplugin/raw/develop/logo.png" width="500" align="center">
+![ProB logo](https://github.com/hhu-stups/prob-rodinplugin/raw/develop/logo.png)
 
-[![Build Status](https://travis-ci.org/hhu-stups/prob-rodinplugin.svg?branch=develop)](https://travis-ci.org/hhu-stups/prob-rodinplugin)
+# The ProB Model Checker and Animator - plugin for Rodin
 
-# The ProB Model Checker and Animator
+## License
 
-[![Build Status](https://travis-ci.org/hhu-stups/prob-rodinplugin.svg?branch=develop)](https://travis-ci.org/hhu-stups/prob-rodinplugin)
-
-The ProB source code is distributed under the EPL license (http://www.eclipse.org/org/documents/epl-v10.html).
-(C) 2000-2021 Michael Leuschel and many others.
+The ProB source code is distributed under the [EPL 1.0 license](https://www.eclipse.org/org/documents/epl-v10.html).
+(C) 2000-2024 Michael Leuschel and many others.
 
 For updates please visit the ProB website: https://prob.hhu.de/w/
 
 ProB comes with ABSOLUTELY NO WARRANTY OF ANY KIND! This software is distributed in the hope that it will be useful but WITHOUT ANY WARRANTY. The author(s) do not accept responsibility to anyone for the consequences of using it or for whether it serves any particular purpose or works at all. No warranty is made about the software or its performance.
 
-The ProB binary and source distributions contain the nauty library (http://cs.anu.edu.au/~bdm/nauty/) which imply further restrictions: the ProB model checker with nauty symmetry reduction cannot be used for applications with nontrivial military significance.
+The ProB binary and source distributions contain the [nauty](https://users.cecs.anu.edu.au/~bdm/nauty/) library, which imply further restrictions: the ProB model checker with nauty symmetry reduction cannot be used for applications with nontrivial military significance.
+
+For availability of commercial support, please contact [Michael Leuschel](https://www.cs.hhu.de/en/research-groups/software-engineering-and-programming-languages/our-team/team/michael-leuschel).
 
-For availability of commercial support, please contact Michael Leuschel (http://www.stups.uni-duesseldorf.de/~leuschel).
+## Bugs
 
-# Bugs
-Please report bugs and feature requests at the new site https://github.com/hhu-stups/prob-issues
+Please report bugs and feature requests on the [ProB issue tracker](https://github.com/hhu-stups/prob-issues).
+
+## Prolog Source Code
 
-# Prolog Source Code
 The latest source code of the Prolog binary can be downloaded from https://stups.hhu-hosting.de/downloads/prob/source/.
-To build the Prolog binaries you require a SICStus 4 (http://sicstus.sics.se/index.html) licence.
+To build the Prolog binaries you require a [SICStus 4](https://sicstus.sics.se/) licence.
+
+## Setting up the development environment
+
+### Requirements
+
+* Java 11 or later
+* Maven 3 or later (Maven 3.9 recommended)
+* Gradle (will be downloaded automatically by the Gradle wrapper)
+
+### Building without Eclipse
+
+After cloning the repository, run these commands in the repository root:
+
+```sh
+$ ./gradlew prepareMaven
+$ mvn -f de.prob.parent/pom.xml install
+```
+
+Adding the -U flag to force re-loading dependencies does not (seem to) work.
+Run ```./gradlew prepareMaven``` before running the mvn command to update.
+
+This will build the plugin into a local Eclipse plugin repository.
+To test your build of the plugin, you need to configure this repository in Rodin:
+
+* Open the Rodin preferences and go to Install/Update > Available Software Sites
+* Click on "Add..."
+* Enter "ProB local" as the name
+* Click on "Local..." and select the directory .../prob-rodinplugin/de.prob.repository/target/repository
+* Click on "Add"
+* Make sure that the "ProB local" repository is checked
+
+Once the repository is configured, use Help > Check for Updates to update the ProB plugin to your locally built version.
 
+Note that if you have both "ProB nightly" and "ProB local" enabled, Rodin will prefer whichever one was built more recently.
+To ensure that only your local build is used, you can temporarily uncheck "ProB nightly".
 
-# Setting up the development environment
+To revert to the official build of the plugin, uncheck the "ProB local" plugin repository, re-check either "ProB" or "ProB nightly", then use Help > Check for Updates again.
+(If this doesn't work, you might need to completely uninstall and reinstall the ProB plugin.)
 
-- Clone the repository (https://github.com/hhu-stups/prob-rodinplugin)
-  We suggest to fork the project on github (see https://help.github.com/articles/fork-a-repo)
+### Building with Eclipse
 
-- We use gradle to manage the dependencies to the libraries, thus you will need gradle installed on your computer.
-  (see http://www.gradle.org/)
+This requires Eclipse for RCP Development.
 
-- In the workspace directory run the completeInstall task (```gradle completeInstall```), alternatively you can also run the downloadCli and collectDependencies tasks (```gradle downloadCli collectDependencies```). This will download the latest nightly build of the Prolog binary and the required Java libraries (such as the parser libraries).
+After cloning the repository, run this command in the repository root
 
-- Install Eclipse for RCP Development
+```sh
+$ ./gradlew prepareMaven
+```
 
 - Import the projects into Eclipse. At this point Eclipse will complain about errors, the reason is that the target platform (i.e., Rodin) hasn't been setup yet).
 

build.gradle

+import java.util.concurrent.TimeUnit
+
 // to trigger a full tycho build please use 'gradle deleteFromClassPath completeInstall'
 
 project.ext {
@@ -8,33 +10,30 @@ project.ext {
 	]
 
 	groupID = "de.prob"
-
-	categoryId = "de.prob2.feature.category"
-	categoryLabel = "ProB for Rodin"
-	// When editing the description here,
-	// also update the descriptions in all feature.xml files!
-	categoryDescription = """\
-	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
-	projects Rodin and Deploy and the DFG projects Gepavas and Gepavas II.
-	ProB has been successfully used on various industrial specifications
-	and is now being used e.g. within Siemens, Alstom, Thales and ClearSy.
-	""".stripIndent()
 }
 
 apply from: 'tycho_build.gradle'
 
+allprojects {
+	configurations.all {
+		resolutionStrategy {
+			cacheChangingModulesFor(0, TimeUnit.SECONDS)
+		}
+	}
+}
+
 project(':de.prob.core') {
 	apply plugin: "java"
 
 	repositories {
 		mavenCentral()
+		maven {
+			name "Sonatype snapshots"
+			url "https://oss.sonatype.org/content/repositories/snapshots/"
+		}
 	}
 
-	def parser_version = "2.12.7"
+	def parser_version = "2.13.0"
 
 	dependencies {
 		// Note: After changing/updating dependencies or their versions here,
@@ -88,7 +87,7 @@ task downloadCli {
 
 			def targetdir = dir + it.getValue()
 			def targetzip = dir + "probcli_${n}.zip"
-			def url = "https://stups.hhu-hosting.de/downloads/prob/cli/releases/1.12.2/probcli_${n}.zip"
+			def url = "https://stups.hhu-hosting.de/downloads/prob/cli/releases/1.13.0/probcli_${n}.zip"
 			download(url, targetzip)
 			FileTree zip = zipTree(targetzip)
 			copy {

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

@@ -2,9 +2,9 @@ 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.6.0.qualifier
+Bundle-Version: 5.6.1.qualifier
 Bundle-Activator: de.bmotionstudio.gef.editor.BMotionEditorPlugin
-Require-Bundle: de.prob.core;bundle-version="[9.5.0,9.6.0)";visibility:=reexport,
+Require-Bundle: de.prob.core;bundle-version="[9.5.1,9.6.0)";visibility:=reexport,
  org.eclipse.core.databinding;bundle-version="[1.10.0,2.0.0)",
  org.eclipse.core.databinding.beans;bundle-version="[1.7.0,2.0.0)",
  org.eclipse.core.resources;bundle-version="[3.13.0,4.0.0)",

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

@@ -123,7 +123,7 @@ public class OpenObserverAction extends SelectionAction {
 				}
 
 			} else {
-				Logger.notifyUserWithoutBugreport("The Observer \""
+				Logger.notifyUser("The Observer \""
 						+ observer.getName()
 						+ "\" does not support a wizard.");
 			}

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

@@ -124,7 +124,7 @@ public class OpenSchedulerEventAction extends SelectionAction {
 					}
 
 				} else {
-					Logger.notifyUserWithoutBugreport("The Scheduler Event \""
+					Logger.notifyUser("The Scheduler Event \""
 							+ newSchedulerEvent.getName()
 							+ "\" does not support a wizard.");
 				}

de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/library/ImportImagesAction.java

@@ -8,7 +8,7 @@ package de.bmotionstudio.gef.editor.library;
 
 import java.io.File;
 import java.io.FileInputStream;
-import java.io.FileNotFoundException;
+import java.io.IOException;
 
 import org.eclipse.core.resources.IFile;
 import org.eclipse.core.resources.IFolder;
@@ -90,7 +90,7 @@ public class ImportImagesAction extends AbstractLibraryAction {
 
 		} catch (CoreException e1) {
 			e1.printStackTrace();
-		} catch (FileNotFoundException e) {
+		} catch (IOException e) {
 			e.printStackTrace();
 		}
 

de.bmotionstudio.rodin/META-INF/MANIFEST.MF

@@ -2,8 +2,8 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: BMotion Studio Rodin Integration
 Bundle-SymbolicName: de.bmotionstudio.rodin;singleton:=true
-Bundle-Version: 1.3.0.qualifier
-Fragment-Host: de.bmotionstudio.gef.editor;bundle-version="[5.6.0,5.7.0)"
+Bundle-Version: 1.3.1.qualifier
+Fragment-Host: de.bmotionstudio.gef.editor;bundle-version="[5.6.1,5.7.0)"
 Bundle-RequiredExecutionEnvironment: JavaSE-11
 Bundle-Vendor: HHU Düsseldorf STUPS Group
 Require-Bundle: org.eclipse.ui.navigator;bundle-version="3.5.0"

de.prob.core.tests/META-INF/MANIFEST.MF

@@ -4,7 +4,7 @@ Bundle-Name: Tests
 Bundle-SymbolicName: de.prob.core.tests
 Bundle-Version: 1.0.0.qualifier
 Bundle-Activator: de.prob.core.tests.Activator
-Require-Bundle: de.prob.core;bundle-version="[9.5.0,9.6.0)",
+Require-Bundle: de.prob.core;bundle-version="[9.5.1,9.6.0)",
  org.eclipse.core.resources;bundle-version="[3.13.0,4.0.0)",
  org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)",
  org.eventb.core;bundle-version="[3.5.0,4.0.0)",

de.prob.core/.classpath

@@ -4,12 +4,12 @@
 	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
 	<classpathentry kind="src" path="src"/>
 	<classpathentry kind="output" path="bin"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/sablecc-runtime-3.6.0.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.12.7.jar"/>
-	<classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.12.7.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/sablecc-runtime-3.7.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.13.0.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.13.0.jar"/>
 </classpath>

de.prob.core/META-INF/MANIFEST.MF

@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: ProB Animator Core
 Bundle-SymbolicName: de.prob.core;singleton:=true
-Bundle-Version: 9.5.0.qualifier
+Bundle-Version: 9.5.1.qualifier
 Require-Bundle: org.eclipse.core.filesystem;bundle-version="[1.7.0,2.0.0)",
  org.eclipse.core.resources;bundle-version="[3.13.0,4.0.0)",
  org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)",
@@ -76,11 +76,11 @@ Bundle-Activator: de.prob.core.internal.Activator
 Eclipse-BuddyPolicy: registered
 Bundle-RequiredExecutionEnvironment: JavaSE-11
 Bundle-ClassPath: .,
- lib/dependencies/answerparser-2.12.7.jar,
- lib/dependencies/bparser-2.12.7.jar,
- lib/dependencies/ltlparser-2.12.7.jar,
- lib/dependencies/parserbase-2.12.7.jar,
- lib/dependencies/prologlib-2.12.7.jar,
- lib/dependencies/sablecc-runtime-3.6.0.jar,
- lib/dependencies/theorymapping-2.12.7.jar,
- lib/dependencies/unicode-2.12.7.jar
+ lib/dependencies/answerparser-2.13.0.jar,
+ lib/dependencies/bparser-2.13.0.jar,
+ lib/dependencies/ltlparser-2.13.0.jar,
+ lib/dependencies/parserbase-2.13.0.jar,
+ lib/dependencies/prologlib-2.13.0.jar,
+ lib/dependencies/sablecc-runtime-3.7.0.jar,
+ lib/dependencies/theorymapping-2.13.0.jar,
+ lib/dependencies/unicode-2.13.0.jar

de.prob.core/src/de/prob/cli/CliStarter.java

 /** 
- * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, 
+ * (c) 2009-2023 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) 
  * */
@@ -21,9 +21,6 @@ import de.prob.core.internal.Activator;
 import de.prob.logging.Logger;
 
 public final class CliStarter {
-	private static final String[] JARS = new String[] { "BParser.jar",
-			"ParserAspects.jar", "aspectjrt.jar", "prolog.jar" };
-
 	private Process prologProcess;
 
 	private int port = -1;
@@ -70,14 +67,26 @@ public final class CliStarter {
 		}
 	}
 
+	/**
+	 * Return {@code process}'s exit code as an {@link Integer}, or {@link Optional#empty()} if it is still running.
+	 *
+	 * @param process the process whose exit code to get
+	 * @return {@code process}'s exit code, or {@link Optional#empty()} if it is still running
+	 */
+	private static Optional<Integer> getProcessExitCode(Process process) {
+		try {
+			return Optional.of(process.exitValue());
+		} catch (final IllegalThreadStateException ignored) {
+			return Optional.empty();
+		}
+	}
+
 	private void startProlog(final File file) throws CliException {
 		prologProcess = null;
 
 		final String os = Platform.getOS();
 		final File applicationPath = getCliPath();
 
-		final String fullcp = createFullClasspath(os, applicationPath);
-
 		final OsSpecificInfo osInfo = getOsInfo(os);
 
 		final String osPath = applicationPath + File.separator + osInfo.subdir;
@@ -90,14 +99,23 @@ public final class CliStarter {
 		}
 
 		List<String> command = new ArrayList<String>();
+		if (Platform.OS_MACOSX.equals(os)) {
+			// Run universal probcli as arm64 if possible (i. e. if the host processor is arm64),
+			// even if Rodin/Eclipse is running as x86_64.
+			// (The macOS default behavior is to match the architecture of the parent process,
+			// which is bad in our case,
+			// because x86_64 probcli under Rosetta 2 is much slower than native arm64 probcli.)
+			command.add("arch");
+			command.add("-arm64");
+			command.add("-x86_64");
+		}
 		command.add(executable);
 		// command.add("-ll");
 		command.add("-sf");
 		command.add("-p");command.add("use_safety_ltl_model_checker");command.add("false");
-		command.add("-parsercp");
+		command.add("-prob_application_type");command.add("rodin"); // supported as of 9/11/2023
 		 // disable LTL safety model check as the counter examples lead to assertion failures 
 		 // in CounterExampleProposition in CounterExample.java
-		command.add(fullcp);
 
 		if (file != null) {
 			command.add(file.getAbsolutePath());
@@ -105,14 +123,12 @@ public final class CliStarter {
 
 		final ProcessBuilder pb = new ProcessBuilder();
 		pb.command(command);
+		pb.environment().put("NO_COLOR", "1");
 		pb.environment().put("PROB_HOME", osPath);
 		try {
 			prologProcess = pb.start();
 		} catch (IOException e) {
-			final String message = "Problem while starting up ProB CLI. Tried to execute:"
-					+ executable;
-			Logger.notifyUser(message, e);
-			throw new CliException(message, e, true);
+			throw new CliException("Problem while starting up ProB CLI. Tried to execute:" + executable, e, false);
 		}
 
 		Assert.isNotNull(prologProcess);
@@ -124,7 +140,19 @@ public final class CliStarter {
 
 		startErrorLogger(output);
 
+		try {
 			extractCliInformation(input);
+		} catch (CliException e) {
+			// Check if the CLI exited while extracting the information.
+			final Optional<Integer> exitCode = getProcessExitCode(prologProcess);
+			if (exitCode.isPresent()) {
+				// CLI exited, report the exit code.
+				throw new CliException("ProB CLI exited with status " + exitCode.get() + " before socket connection could be opened", e, false);
+			} else {
+				// CLI didn't exit, just rethrow the error.
+				throw e;
+			}
+		}
 		// log output from Prolog
 		startOutputLogger(input);
 
@@ -151,10 +179,7 @@ public final class CliStarter {
 			} else if (os.equals(Platform.OS_LINUX)) {
 				subdir = "linux64";
 			} else {
-				final CliException cliException = new CliException(
-						"ProB does not support the plattform: " + os);
-				cliException.notifyUserOnce();
-				throw cliException;
+				throw new CliException("ProB does not support the plattform: " + os);
 			}
 
 			return new OsSpecificInfo(subdir, "probcli.sh",
@@ -162,7 +187,6 @@ public final class CliStarter {
 		}
 	}
 
-	@SuppressWarnings("unchecked")
 	private void extractCliInformation(final BufferedReader input)
 			throws CliException {
 		final PortPattern portPattern = new PortPattern();
@@ -172,32 +196,13 @@ public final class CliStarter {
 		userInterruptReference = intPattern.getValue();
 	}
 
-	private static String createFullClasspath(final String os, final File path)
-			throws CliException {
-		final File base = new File(path.getParentFile().getParentFile(),
-				"de.prob.common");
-		final File common = new File(base, "common");
-		final File lib = new File(common, "lib");
-		final StringBuilder sb = new StringBuilder();
-		boolean isFirst = true;
-		for (final String jar : JARS) {
-			final File entry = new File(lib, jar);
-			if (!isFirst) {
-				sb.append(File.pathSeparator);
-			}
-			sb.append(entry.getPath());
-			isFirst = false;
-		}
-		return sb.toString();
-	}
-
 	private void startOutputLogger(final BufferedReader input) {
-		stdLogger = new OutputLoggerThread("(Output " + port + ")", input);
+		stdLogger = new OutputLoggerThread("(Output " + port + ")", input, false);
 		stdLogger.start();
 	}
 
 	private void startErrorLogger(final BufferedReader output) {
-		errLogger = new OutputLoggerThread("(Error " + port + ")", output);
+		errLogger = new OutputLoggerThread("(Error " + port + ")", output, true);
 		errLogger.start();
 	}
 
@@ -208,14 +213,13 @@ public final class CliStarter {
 			String line;
 			boolean endReached = false;
 			while (!endReached && (line = input.readLine()) != null) {
+				Logger.info("probcli startup output: " + line);
 				applyPatterns(patterns, line);
 				endReached = patterns.isEmpty()
 						|| line.contains("starting command loop"); // printed in prob_socketserver.pl
 			}
 		} catch (IOException e) {
-			final String message = "Problem while starting ProB. Cannot read from input stream.";
-			Logger.notifyUser(message, e);
-			throw new CliException(message, e, true);
+			throw new CliException("Problem while starting ProB. Cannot read from input stream.", e, true);
 		}
 		for (CliPattern<?> p : patterns) {
 			p.notFound();
@@ -236,29 +240,29 @@ public final class CliStarter {
 
 	private File getCliPath() throws CliException {
 		final Bundle bundle = Activator.getDefault().getBundle();
-		final String fileURL = "prob";
-		final URL entry = bundle.getEntry(fileURL);
+		final URL entry = bundle.getEntry("prob");
 
 		if (entry == null) {
 			throw new CliException(
 					"Unable to find directory with prob executables.");
 		}
 
+		URL fileUrl;
 		try {
-			URL resolvedUrl = FileLocator.find(bundle, new Path(fileURL), null);
-
-			// We need to use the 3-arg constructor of URI in order to properly
-			// escape file system chars.
-			URI resolvedUri = new URI("file", FileLocator
-					.toFileURL(resolvedUrl).getPath(), null);
+			fileUrl = FileLocator.toFileURL(entry);
+		} catch (IOException e) {
+			throw new CliException("Input/output error when trying to find '" + entry + "'", e, false);
+		}
 
-			return new File(resolvedUri);
+		try {
+			// Eclipse has a long-standing bug where Bundle.getEntry etc. don't correctly escape spaces, non-ASCII characters, etc. in file URLs.
+			// This makes it impossible to use the standard URL.toURI() method - it will throw an URISyntaxException for these unescaped characters.
+			// As a workaround, use Eclipse's URIUtil.toURI(URL), which escapes such unescaped characters.
+			// https://bugs.eclipse.org/bugs/show_bug.cgi?id=145096
+			// https://probjira.atlassian.net/browse/PROBPLUGIN-87
+			return new File(URIUtil.toURI(fileUrl));
 		} catch (URISyntaxException e) {
-			throw new CliException("Unable to construct file '"
-					+ entry.getPath() + "'");
-		} catch (IOException e2) {
-			throw new CliException("Input/output error when trying t find '"
-					+ fileURL + "'");
+			throw new CliException("Unable to construct file '" + entry.getPath() + "'", e, false);
 		}
 	}
 
@@ -268,12 +272,15 @@ public final class CliStarter {
 
 		private final String prefix;
 
+		private final boolean logToLog;
+
 		private volatile boolean shutingDown = false;
 
-		public OutputLoggerThread(final String name, final BufferedReader in) {
+		public OutputLoggerThread(final String name, final BufferedReader in, boolean logToLog) {
 			super();
 			prefix = "[" + name + "] ";
 			this.in = in;
+			this.logToLog = logToLog;
 		}
 
 		@Override
@@ -285,14 +292,15 @@ public final class CliStarter {
 					if (line == null) {
 						break;
 					}
-					// Logger.log(IStatus.INFO, IStatus.OK, prefix + line,
-					// null);
+					if (logToLog) {
+						Logger.log(IStatus.INFO, prefix + line, null);
+					}
 					System.err.println(prefix + line);
 				}
 			} catch (IOException e) {
 				if (!"Stream closed".equals(e.getMessage())) {
 					final String message = "OutputLogger died with error";
-					Logger.log(IStatus.INFO, Logger.DEBUG, message, e);
+					Logger.log(IStatus.INFO, message, e);
 				}
 			} finally {
 				if (in != null) {

de.prob.core/src/de/prob/cli/clipatterns/PortPattern.java

@@ -39,14 +39,7 @@ public class PortPattern extends CliPattern<Integer> {
 
 	@Override
 	public void notFound() throws CliException {
-		// final String message = "Could not determine port of ProB server";
-		// Logger.notifyUser(message);
-		// throw new CliException(message);
-
-		CliException cliException = new CliException(
-				"Could not determine port of ProB server");
-		cliException.notifyUserOnce();
-		throw cliException;
+		throw new CliException("Could not determine port of ProB server");
 	}
 
 }

de.prob.core/src/de/prob/core/Animator.java

@@ -10,20 +10,17 @@ import java.io.File;
 import java.util.HashMap;
 import java.util.Map;
 
-import org.osgi.service.prefs.Preferences;
-
 import de.prob.core.command.IComposableCommand;
 import de.prob.core.domainobjects.History;
 import de.prob.core.domainobjects.MachineDescription;
 import de.prob.core.domainobjects.Operation;
-import de.prob.core.domainobjects.RandomSeed;
 import de.prob.core.domainobjects.State;
 import de.prob.core.internal.Activator;
 import de.prob.core.internal.AnimatorImpl;
-import de.prob.core.internal.ServerTraceConnection;
-import de.prob.core.internal.TraceConnectionProvider;
+import de.prob.core.internal.ServerConnection;
 import de.prob.exceptions.ProBException;
 
+import org.osgi.service.prefs.Preferences;
 
 /**
  * Animator is a singleton Proxy used to communicate with ProB. The method
@@ -41,10 +38,6 @@ public final class Animator {
 	private static Animator animator = new Animator();
 	private static Animator auxanimator = null;
 
-	/**
-	 * 
-	 */
-	private IConnectionProvider connectionProvider = null;
 	private volatile boolean dirty;
 	private volatile boolean rodinProjectHasErrorsOrWarnings;
 	private final Map<Object, Object> dataStore = new HashMap<Object, Object>();
@@ -98,7 +91,7 @@ public final class Animator {
 	}
 
 	private final synchronized void createNewImplementation(final File file) {
-		final AnimatorImpl impl = new AnimatorImpl(getIServerConnection(), file);
+		final AnimatorImpl impl = new AnimatorImpl(new ServerConnection(), file);
 		setImplementation(impl);
 		StaticListenerRegistry.registerComputationListener(getHistory());
 	}
@@ -212,48 +205,6 @@ public final class Animator {
 		return implementation;
 	}
 
-	/**
-	 * 
-	 * @param {@link IConnectionProvider} provider
-	 */
-	public final synchronized void setConnectionProvider(
-			final IConnectionProvider provider) {
-		connectionProvider = provider;
-	}
-
-	/**
-	 * @return {@link IServerConnection}, by default (that means
-	 *         <code>connectionProvider == null</code>) the
-	 *         {@link ServerTraceConnection}. If a {@link IConnectionProvider}
-	 *         is set, it is asked to provide a new IServerConnection
-	 * 
-	 */
-	private final synchronized IServerConnection getIServerConnection() {
-		if (connectionProvider == null) {
-			connectionProvider = new TraceConnectionProvider();
-		}
-		return connectionProvider.getISeverConnection();
-	}
-
-	/**
-	 * 
-	 * @return {@link ITrace}, or null if the IServerConnection is not a
-	 *         {@link ServerTraceConnection}
-	 */
-	public final synchronized ITrace getTrace() {
-		if (implementation != null)
-			return implementation.getTraceImpl();
-		return null;
-	}
-
-	public final synchronized RandomSeed getRandomSeed() {
-		return getImplementation().getSeed();
-	}
-
-	public final synchronized void setRandomSeed(final RandomSeed seed) {
-		getImplementation().setSeed(seed);
-	}
-
 	// just for testing
 	private Preferences customConfiguration;
 

de.prob.core/src/de/prob/core/IConnectionProvider.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.prob.core;
-
-
-
-public interface IConnectionProvider {
-	/**
-	 * 
-	 * @return new {@link IServerConnection}
-	 */
-	public IServerConnection getISeverConnection();
-}

de.prob.core/src/de/prob/core/IServerConnection.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.prob.core;
-
-import java.io.File;
-
-import de.prob.cli.CliException;
-import de.prob.exceptions.ProBException;
-
-/**
- * This interface can be used to mock up a connection to ProB for testing. Don't
- * use this in productive code.
- * 
- * An example of such a mock is
- * 
- * <pre>
- * IServerConnection mock = EasyMock.createMock(IServerConnection.class);
- * mock.startup();
- * EasyMock.expect(mock.sendCommand(COMMAND)).andReturn(
- * 		ProBResultParser.parse(EXPECTED_ANSWER));
- * GetErrorsHelper.expectGetErrors(mock);
- * EasyMock.replay(mock);
- * Animator animator = new AnimatorImpl(mock);
- * EasyMock.verify(mock);
- * // [ ... Assertions ...]
- * </pre>
- * 
- * @author Jens Bendisposto
- * 
- */
-public interface IServerConnection {
-
-	public abstract int getCliPortNumber();
-
-	public abstract String sendCommand(final String commandString)
-			throws ProBException;
-
-	public abstract void shutdown();
-
-	public abstract void startup(File file) throws CliException;
-
-	void sendUserInterruptSignal();
-}
\ No newline at end of file

de.prob.core/src/de/prob/core/ITrace.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.prob.core;
-
-import java.util.List;
-
-import de.prob.core.internal.Message;
-
-public interface ITrace {
-
-	/**
-	 * @return the List of logged messages as a String
-	 */
-	public String getTraceAsString();
-
-	/**
-	 * @return the List of logged messages as unmodifiable List of
-	 *         {@link Message}
-	 */
-	public List<Message> getTraceAsList();
-
-	public int size();
-
-	void setMaximum(Integer max);
-
-	Integer getMaximum();
-
-}

de.prob.core/src/de/prob/core/ProBJobFinishedListener.java

@@ -23,9 +23,8 @@ public abstract class ProBJobFinishedListener extends JobChangeAdapter {
 				showResult(checkJob.getCommand(), checkJob.getAnimator());
 			}
 		} else {
-			final String message = "The job has a wrong type. Expected ProBCommandJob but got "
-					+ job.getClass();
-			Logger.notifyUserWithoutBugreport(message);
+			Logger.notifyUser("The job has a wrong type. Expected ProBCommandJob but got "
+					+ job.getClass());
 		}
 	}