diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..0260644433c22d17b209f5af171fa043be4a1a0b --- /dev/null +++ b/.gitattributes @@ -0,0 +1,7 @@ +# 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 diff --git a/.gitignore b/.gitignore index df249aee774e7d3a3655bf22bcff0acb61c1a830..ce254b76353f94069f5ba8135754f818f3bdf290 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ **/bin/ **/target/ +.idea/ .gradle/ .metadata/ **/pom.xml @@ -8,5 +9,4 @@ pom.xml updatesite/ **/lib/dependencies/ de.prob.core/prob/ -build/ -de.prob.repository/category.xml \ No newline at end of file +build/ \ No newline at end of file diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e489897ea655fd33ecbb90c38c6be55d01817277..577d5a4adbca85ba2f7163dac758aa95ac86f145 100644 --- a/.gitlab-ci.yml +++ b/.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: diff --git a/README.md b/README.md index 9456efab49e69645a45f9ec3831937026bccb82d..2be0c47822a85960943cbed66e729e97a9ab570a 100644 --- a/README.md +++ b/README.md @@ -1,41 +1,76 @@ -<img src="https://github.com/hhu-stups/prob-rodinplugin/raw/develop/logo.png" width="500" align="center"> + -[](https://travis-ci.org/hhu-stups/prob-rodinplugin) +# The ProB Model Checker and Animator - plugin for Rodin -# The ProB Model Checker and Animator +## License -[](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). diff --git a/build.gradle b/build.gradle index 515dd15e8e7bf9ada416098335233f0b50a17cc4..c0d0efe936d23800ff5c7b86c7e76190885c5f2a 100644 --- a/build.gradle +++ b/build.gradle @@ -1,3 +1,5 @@ +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 { diff --git a/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF b/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF index 26f4e2947776f9975080604d02d89bcbe55cd212..e88976ea17cc3dddd55d72edba609dc8b417a758 100644 --- a/de.bmotionstudio.gef.editor/META-INF/MANIFEST.MF +++ b/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)", diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java index 20e1197ab3fa999549dd19a371bbc1ec28e6bac4..5715f2acb509fb7b3089971093ede6171aec74fa 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenObserverAction.java +++ b/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."); } diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java index cf5b463c09ec1749919bad45bf2d1ea3a5bbd6aa..2a26f4136988ccf6084062d73d16ce1a618cf0ce 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/action/OpenSchedulerEventAction.java +++ b/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."); } diff --git a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/library/ImportImagesAction.java b/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/library/ImportImagesAction.java index b99001771afae3997a74d8ba9f6bd801fccbb4fd..fe548ec14a5c7a4f6774a8279fe8015a4cde63de 100644 --- a/de.bmotionstudio.gef.editor/src/de/bmotionstudio/gef/editor/library/ImportImagesAction.java +++ b/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(); } diff --git a/de.bmotionstudio.rodin/META-INF/MANIFEST.MF b/de.bmotionstudio.rodin/META-INF/MANIFEST.MF index 40f672e63c4840a78c40d4d8954f952474b2b4df..864bb4c960f80b52f955345600ad7d2da3974f98 100644 --- a/de.bmotionstudio.rodin/META-INF/MANIFEST.MF +++ b/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" diff --git a/de.prob.core.tests/META-INF/MANIFEST.MF b/de.prob.core.tests/META-INF/MANIFEST.MF index 165635844ae7b89c2b59d34abb2d049e1f410169..9960f048edf67d5deb84f9b8d1e60c8fab6dc412 100644 --- a/de.prob.core.tests/META-INF/MANIFEST.MF +++ b/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)", diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath index 683c6f28f6597f49da24767503be55c6f33ba416..060b00c947b5f33cee407fc8aef90a35cfff3541 100644 --- a/de.prob.core/.classpath +++ b/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> diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF index cb64f1bbce279f7a2c673c6e3fa86f25a331ad58..46e38f533ace74782bc90d214d762709f30c26a2 100644 --- a/de.prob.core/META-INF/MANIFEST.MF +++ b/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 diff --git a/de.prob.core/src/de/prob/cli/CliStarter.java b/de.prob.core/src/de/prob/cli/CliStarter.java index bc0f8e1c9d6d743326d53db16f2ec20c201a96df..e11c7c9bbe94c1e4dd775957f282eda58c901eb9 100644 --- a/de.prob.core/src/de/prob/cli/CliStarter.java +++ b/de.prob.core/src/de/prob/cli/CliStarter.java @@ -1,5 +1,5 @@ /** - * (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); - extractCliInformation(input); + 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) { diff --git a/de.prob.core/src/de/prob/cli/clipatterns/PortPattern.java b/de.prob.core/src/de/prob/cli/clipatterns/PortPattern.java index 3878e2cbc7662fb6fbaf5960c56575985f57d2cc..19724b1a772a4da213176fafb3ec610ed545e30f 100644 --- a/de.prob.core/src/de/prob/cli/clipatterns/PortPattern.java +++ b/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"); } } diff --git a/de.prob.core/src/de/prob/core/Animator.java b/de.prob.core/src/de/prob/core/Animator.java index 1d49c94b2ecf95be9d2399d2d66bd8f93285d341..9abaa9de03d222f14eb19743f51f523d84d66137 100644 --- a/de.prob.core/src/de/prob/core/Animator.java +++ b/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; diff --git a/de.prob.core/src/de/prob/core/IConnectionProvider.java b/de.prob.core/src/de/prob/core/IConnectionProvider.java deleted file mode 100644 index 8fab6f07f31b088c6fc72f972fa2208ca2f9c1f3..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/IConnectionProvider.java +++ /dev/null @@ -1,17 +0,0 @@ -/** - * (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(); -} diff --git a/de.prob.core/src/de/prob/core/IServerConnection.java b/de.prob.core/src/de/prob/core/IServerConnection.java deleted file mode 100644 index 5b7dc30444cfc344f2a5c36be818110047fa76ba..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/IServerConnection.java +++ /dev/null @@ -1,47 +0,0 @@ -/** - * (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 diff --git a/de.prob.core/src/de/prob/core/ITrace.java b/de.prob.core/src/de/prob/core/ITrace.java deleted file mode 100644 index eb7647044dd9ef1a1339f11625b52700a4a79e9b..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/ITrace.java +++ /dev/null @@ -1,32 +0,0 @@ -/** - * (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(); - -} diff --git a/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java b/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java index c38986a76313d9eecabb69e96e42b0b4af75c3e0..bbbe41b0e02e55245b74bae159a703dab9fec559 100644 --- a/de.prob.core/src/de/prob/core/ProBJobFinishedListener.java +++ b/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()); } } diff --git a/de.prob.core/src/de/prob/core/ProblemHandler.java b/de.prob.core/src/de/prob/core/ProblemHandler.java index 7a269ea4cd37c9cef509740474908f3b2e6e50dc..9cdd906c569c74f62be9ad92bf0aa712ee48d5ba 100644 --- a/de.prob.core/src/de/prob/core/ProblemHandler.java +++ b/de.prob.core/src/de/prob/core/ProblemHandler.java @@ -10,14 +10,13 @@ import java.util.List; import de.prob.cli.CliException; import de.prob.core.command.CommandException; -import de.prob.core.internal.ResultParserException; import de.prob.logging.Logger; public class ProblemHandler { /** - * Notifies the User about a fatal problem inside a command by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message + * Notifies the User about a fatal problem inside a command by adding an error + * to the log. This method takes a message * describing the problem.<br> * * <b>Note:</b> Calling this method logs the problem and throws a new @@ -37,8 +36,8 @@ public class ProblemHandler { } /** - * Notifies the User about a fatal problem inside a command by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message + * Notifies the User about a fatal problem inside a command by adding an error + * to the log. This method takes a message * describing the problem.<br> * * <b>Note:</b> Calling this method logs the problem and throws a new @@ -74,8 +73,8 @@ public class ProblemHandler { /** * - * Notifies the User about a fatal problem by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message + * Notifies the User about a fatal problem by adding an error + * to the log. This method takes a message * describing the problem and the causing exception. * * Note: Calling this method logs the problem and throws a CliException that @@ -95,8 +94,8 @@ public class ProblemHandler { /** * - * Notifies the User about a fatal problem by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message + * Notifies the User about a fatal problem by adding an error + * to the log. This method takes a message * describing the problem and the causing exception. * * Note: Calling this method logs the problem and throws a CliException that @@ -113,26 +112,4 @@ public class ProblemHandler { Logger.notifyUser(message, t); throw new CliException(message, t, true); } - - /** - * - * Notifies the User about a fatal problem by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message - * describing the problem and the causing exception. - * - * Note: Calling this method logs the problem and throws a CliException that - * wraps the original problem - * - * @param message - * Description of the problem - * @param throwable - * Causing exception - * @throws ResultParserException - */ - public static void handleResultPareserException(final String message, - final Throwable t) throws ResultParserException { - Logger.notifyUser(message, t); - throw new ResultParserException(message, t); - } - } diff --git a/de.prob.core/src/de/prob/core/PrologException.java b/de.prob.core/src/de/prob/core/PrologException.java index c5ce207798b4811f32dd920a52a64f43b8d60aef..8b99996f252a29b67ef3489fb16dad256eeb54b7 100644 --- a/de.prob.core/src/de/prob/core/PrologException.java +++ b/de.prob.core/src/de/prob/core/PrologException.java @@ -26,8 +26,7 @@ public class PrologException extends ProBException { if (!handled) { handled = true; if (onlyWarnings) { - Logger.log(IStatus.WARNING, Logger.NOBUGREPORT, - this.getMessage(), this); + Logger.log(IStatus.WARNING, this.getMessage(), this); } else { Logger.notifyUser(this.getMessage(), this); } diff --git a/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java b/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java index 4561a70602403a57a71c252d8bc2ef849a18e593..35d16e91a5df47d42a3856af1839f7a9c0fc67a5 100644 --- a/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java +++ b/de.prob.core/src/de/prob/core/command/ComputeCoverageCommand.java @@ -14,6 +14,7 @@ import de.prob.core.Animator; import de.prob.exceptions.ProBException; import de.prob.parser.ISimplifiedROMap; import de.prob.prolog.output.IPrologTermOutput; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.IntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; @@ -29,9 +30,16 @@ public final class ComputeCoverageCommand implements IComposableCommand { private final List<String> nodes = new ArrayList<String>(); private final List<String> uncovered = new ArrayList<String>(); + @Deprecated public ComputeCoverageResult(final IntegerPrologTerm totalNumberOfNodes, final IntegerPrologTerm totalNumberOfTransitions, final ListPrologTerm ops, final ListPrologTerm nodes, final ListPrologTerm uncovered) { + this((AIntegerPrologTerm) totalNumberOfNodes, totalNumberOfTransitions, ops, nodes, uncovered); + } + + public ComputeCoverageResult(final AIntegerPrologTerm totalNumberOfNodes, + final AIntegerPrologTerm totalNumberOfTransitions, final ListPrologTerm ops, final ListPrologTerm nodes, + final ListPrologTerm uncovered) { this.totalNumberOfNodes = totalNumberOfNodes.getValue(); this.totalNumberOfTransitions = totalNumberOfTransitions.getValue(); for (PrologTerm op : ops) { @@ -83,8 +91,8 @@ public final class ComputeCoverageCommand implements IComposableCommand { @Override public void processResult(final ISimplifiedROMap<String, PrologTerm> bindings) throws CommandException { - IntegerPrologTerm totalNodeNr = (IntegerPrologTerm) bindings.get("TotalNodeNr"); - IntegerPrologTerm totalTransNr = (IntegerPrologTerm) bindings.get("TotalTransSum"); + AIntegerPrologTerm totalNodeNr = (AIntegerPrologTerm) bindings.get("TotalNodeNr"); + AIntegerPrologTerm totalTransNr = (AIntegerPrologTerm) bindings.get("TotalTransSum"); ListPrologTerm ops = (ListPrologTerm) bindings.get("OpStat"); ListPrologTerm nodes = (ListPrologTerm) bindings.get("NodeStat"); diff --git a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java index 98f0b1e5a27112cbd10cc5a02acf5c297e31823c..b162632661a6467928afdfd23020e666a98d4621 100644 --- a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java +++ b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java @@ -87,12 +87,12 @@ public final class ExploreStateCommand implements IComposableCommand { // only show error message on SETUP_CONSTANTS and // PARTIALLY_SETUP_CONSTANTS if (unsatPropertiesExist) { - Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties.\n" + Logger.notifyUser("ProB could not find valid constants wich satisfy the properties.\n" + unsatPropsCommand.getUnsatPropertiesDescription()); } else if (!initialised && enabledOperations.isEmpty() && !timeoutOccured) { - Logger.notifyUserWithoutBugreport("ProB could not find valid constants/variables. This might be caused by the animation settings (e.g., Integer range or deferred set size) or by an inconsistency in the axioms."); + Logger.notifyUser("ProB could not find valid constants/variables. This might be caused by the animation settings (e.g., Integer range or deferred set size) or by an inconsistency in the axioms."); } Set<String> timeouts = new HashSet<String>( diff --git a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java index 4e81cec31e0a2f345c8a5bfcb53a002cf0f3d1df..9298bc226b6e5ad06d10d54df6e7af9c23ff2925 100644 --- a/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java +++ b/de.prob.core/src/de/prob/core/command/LoadEventBModelCommand.java @@ -104,7 +104,7 @@ public final class LoadEventBModelCommand { + " Typically this means, that your axioms are too complicated for automatic solving. " + "You might create an animation refinement using the context menu to help ProB finding a solution."; } - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser(message); } } catch (CommandException ex) { Logger.notifyUser("Event-B Model or Context could not be loaded due to an exception: " diff --git a/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java b/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java index ed5320eae01d596e0ce88c803e3c3f441ec0617c..59793d7e69275e381416d13baa2590a85c5fcc44 100644 --- a/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java +++ b/de.prob.core/src/de/prob/core/command/LtlCheckingCommand.java @@ -11,8 +11,8 @@ import de.prob.core.domainobjects.Operation; import de.prob.exceptions.ProBException; import de.prob.parser.ISimplifiedROMap; import de.prob.prolog.output.IPrologTermOutput; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.IntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; @@ -206,8 +206,7 @@ public final class LtlCheckingCommand implements IComposableCommand { loopEntry = -1; } else if (loopStatus.hasFunctor("loop", 1)) { pathType = PathType.INFINITE; - loopEntry = ((IntegerPrologTerm) loopStatus.getArgument(1)) - .getValue().intValue(); + loopEntry = ((AIntegerPrologTerm) loopStatus.getArgument(1)).intValueExact(); } else throw new CommandException( "LTL model check returned unexpected loop status: " diff --git a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java index 5e5858fe1c0d3712b7bedcb0ce8755e152405f0f..8b1600092ce5269a673ee6a0d5f8856ab7e73dd3 100644 --- a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java +++ b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java @@ -59,12 +59,9 @@ public final class ModelCheckingCommand implements IComposableCommand { CompoundPrologTerm term = (CompoundPrologTerm) bindings.get("Result"); CompoundPrologTerm stats = (CompoundPrologTerm) bindings.get("Stats"); - int processedTotal = ((IntegerPrologTerm) stats.getArgument(3)) - .getValue().intValue(); - int numStates = ((IntegerPrologTerm) stats.getArgument(1)).getValue() - .intValue(); - int numTransitions = ((IntegerPrologTerm) stats.getArgument(2)) - .getValue().intValue(); + int processedTotal = ((AIntegerPrologTerm) stats.getArgument(3)).intValueExact(); + int numStates = ((AIntegerPrologTerm) stats.getArgument(1)).intValueExact(); + int numTransitions = ((AIntegerPrologTerm) stats.getArgument(2)).intValueExact(); result = new ModelCheckingResult<Result>(Result.class, term, processedTotal, numStates, numTransitions); diff --git a/de.prob.core/src/de/prob/core/domainobjects/Operation.java b/de.prob.core/src/de/prob/core/domainobjects/Operation.java index 16c341bb60471dd9c0fba1595ec8c7c77d90ff46..8c586d7eef7a98877abda61245cbb4ff65cbd250 100644 --- a/de.prob.core/src/de/prob/core/domainobjects/Operation.java +++ b/de.prob.core/src/de/prob/core/domainobjects/Operation.java @@ -12,8 +12,8 @@ import java.util.HashMap; import java.util.List; import java.util.Map; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.IntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; import de.prob.unicode.UnicodeTranslator; @@ -121,9 +121,8 @@ public final class Operation { public static Operation fromPrologTerm(final PrologTerm rawOpTerm) { final CompoundPrologTerm opTerm = (CompoundPrologTerm) rawOpTerm; - final IntegerPrologTerm pInt = (IntegerPrologTerm) opTerm - .getArgument(ID); - final long id = pInt.getValue().longValue(); + final AIntegerPrologTerm pInt = (AIntegerPrologTerm) opTerm.getArgument(ID); + final long id = pInt.longValueExact(); final String name = PrologTerm.atomicString(opTerm.getArgument(NAME)); final EventType type = SPECIAL_EVENTS.get(name); final String destId = getIdFromPrologTerm(opTerm.getArgument(DST)); @@ -171,8 +170,8 @@ public final class Operation { .getArgument(ARGS_PRETTY)); this.hashCode = initHashCode(); - final IntegerPrologTerm pInt = (IntegerPrologTerm) term.getArgument(ID); - this.id = pInt.getValue().longValue(); + final AIntegerPrologTerm pInt = (AIntegerPrologTerm) term.getArgument(ID); + this.id = pInt.longValueExact(); this.eventStack = createEventStack((ListPrologTerm) term .getArgument(INFOS)); } @@ -244,10 +243,8 @@ public final class Operation { } private static String getIdFromPrologTerm(final PrologTerm destTerm) { - if (destTerm instanceof IntegerPrologTerm) { - return ((IntegerPrologTerm) destTerm).getValue().toString(); - } - return ((CompoundPrologTerm) destTerm).getFunctor(); + // integer terms have their string representation as functor + return destTerm.atomicToString(); } public long getId() { diff --git a/de.prob.core/src/de/prob/core/domainobjects/RandomSeed.java b/de.prob.core/src/de/prob/core/domainobjects/RandomSeed.java deleted file mode 100644 index bc6ebb973f7fcb8e51b44f880f3707aa910ac68a..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/domainobjects/RandomSeed.java +++ /dev/null @@ -1,87 +0,0 @@ -/** - * (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.domainobjects; - -import java.math.BigInteger; -import java.util.regex.Matcher; -import java.util.regex.Pattern; - -public class RandomSeed { - - private final BigInteger[] seed; - - public RandomSeed(final BigInteger x, final BigInteger y, - final BigInteger z, final BigInteger b) { - seed = new BigInteger[] { x, y, z, b }; - } - - public BigInteger getSeedX() { - return seed[0]; - } - - public BigInteger getSeedY() { - return seed[1]; - } - - public BigInteger getSeedZ() { - return seed[2]; - } - - public BigInteger getSeedB() { - return seed[3]; - } - - @Override - public String toString() { - return getSeedX() + ":" + getSeedY() + ":" + getSeedZ() + ":" - + getSeedB(); - } - - public static RandomSeed fromString(final String seed) { - Pattern p = Pattern.compile("(\\d*):(\\d*):(\\d*):(\\d*)"); - Matcher m = p.matcher(seed); - if (!m.matches()) { - throw new IllegalArgumentException("Wrong format"); - } - String[] splitSeed = seed.split(":"); - BigInteger x = new BigInteger(splitSeed[0]); - BigInteger y = new BigInteger(splitSeed[1]); - BigInteger z = new BigInteger(splitSeed[2]); - BigInteger b = new BigInteger(splitSeed[3]); - return new RandomSeed(x, y, z, b); - } - - @Override - public boolean equals(final Object obj) { - if (obj instanceof RandomSeed) { - RandomSeed seed = (RandomSeed) obj; - if (!(seed.getSeedX().equals(this.getSeedX()))) { - return false; - } - if (!(seed.getSeedY().equals(this.getSeedY()))) { - return false; - } - if (!(seed.getSeedZ().equals(this.getSeedZ()))) { - return false; - } - if (!(seed.getSeedB().equals(this.getSeedB()))) { - return false; - } - return true; - } - return false; - } - - @Override - public int hashCode() { - final int xHash = getSeedX().hashCode(); - final int yHash = getSeedY().hashCode(); - final int zHash = getSeedZ().hashCode(); - final int bHash = getSeedB().hashCode(); - return xHash + 11 * yHash + 37 * zHash + 43 * bHash; - } -} diff --git a/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java b/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java index 5d3020a19104faa3ec6fe7cf3dc44e222d34c309..399517801ec0ad41b1ce2febfc6d5557cebf93da 100644 --- a/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java +++ b/de.prob.core/src/de/prob/core/domainobjects/ltl/CounterExample.java @@ -9,8 +9,8 @@ import de.prob.core.command.LtlCheckingCommand.PathType; import de.prob.core.command.LtlCheckingCommand.Result; import de.prob.core.domainobjects.Operation; import de.prob.logging.Logger; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.IntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; @@ -98,8 +98,7 @@ public class CounterExample { .getArgument(3); for (int i = 0; i < values.size(); i++) { - int value = ((IntegerPrologTerm) values.get(i)).getValue() - .intValue(); + int value = ((AIntegerPrologTerm) values.get(i)).intValueExact(); // Doesn't have to be a 'predicateValues.get(index)' and not // 'predicateValues.get(i)' (predicateValues is a list of boolean lists) //predicateValues.get(index).add(value == 0 ? false : true); @@ -140,9 +139,9 @@ public class CounterExample { Arrays.asList(values)); } else if (arity == 1) { if (functor.equals("ap") || functor.equals("tp")) { - IntegerPrologTerm atomic = (IntegerPrologTerm) term + AIntegerPrologTerm atomic = (AIntegerPrologTerm) term .getArgument(1); - int atomicId = atomic.getValue().intValue(); + int atomicId = atomic.intValueExact(); final String name = atomicFormulaNames[atomicId]; diff --git a/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java b/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java index 639180e70eb1f2ba2ec190354abab376ef2aa2ea..dd203845f6b80779add1b360b064e165e2d0d07a 100644 --- a/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java +++ b/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java @@ -11,8 +11,6 @@ import java.util.List; import java.util.Map; import de.prob.cli.CliException; -import de.prob.core.IServerConnection; -import de.prob.core.ITrace; import de.prob.core.LanguageDependendAnimationPart; import de.prob.core.ProblemHandler; import de.prob.core.command.CommandException; @@ -22,12 +20,17 @@ import de.prob.core.command.IComposableCommand; import de.prob.core.domainobjects.History; import de.prob.core.domainobjects.HistoryItem; import de.prob.core.domainobjects.MachineDescription; -import de.prob.core.domainobjects.RandomSeed; import de.prob.core.domainobjects.State; -import de.prob.core.sablecc.node.Start; +import de.prob.core.sablecc.node.ACallBackResult; +import de.prob.core.sablecc.node.AProgressResult; +import de.prob.core.sablecc.node.AYesResult; +import de.prob.core.sablecc.node.PResult; import de.prob.exceptions.ProBException; import de.prob.logging.Logger; import de.prob.parser.BindingGenerator; +import de.prob.parser.PrologTermGenerator; +import de.prob.parser.ResultParserException; +import de.prob.parser.SimplifiedROMap; import de.prob.prolog.output.PrologTermStringOutput; import de.prob.prolog.term.PrologTerm; @@ -40,9 +43,7 @@ public class AnimatorImpl { private final History history = new History(); - private IServerConnection connector; - - private RandomSeed seed; + private ServerConnection connector; private MachineDescription description; @@ -50,8 +51,7 @@ public class AnimatorImpl { private LanguageDependendAnimationPart langdep; - public AnimatorImpl(final IServerConnection serverConnection, - final File file) { + public AnimatorImpl(final ServerConnection serverConnection, final File file) { this.file = file; setConnector(serverConnection); } @@ -78,32 +78,16 @@ public class AnimatorImpl { return item == null ? null : item.getState(); } - public synchronized Start sendCommandImpl(final String command) - throws ProBException { - String input = connector.sendCommand(command); - return parseResult(input); - } - - private Start parseResult(final String input) throws CliException, - ResultParserException { - if (input == null) - return null; - else - return ProBResultParser.parse(input); - } - public History getHistoryImpl() { return history; } - private synchronized void setConnector( - final IServerConnection serverConnection) { + private synchronized void setConnector(final ServerConnection serverConnection) { this.connector = serverConnection; try { connector.startup(file); } catch (CliException e) { - // The user has been notified by the underlying implementation, so - // we only invalidate the connector + e.notifyUserOnce(); connector = null; } } @@ -112,26 +96,6 @@ public class AnimatorImpl { return true; } - public synchronized final ITrace getTraceImpl() { - final ITrace trace; - if (connector != null && connector instanceof ServerTraceConnection) { - ServerTraceConnection conn = (ServerTraceConnection) connector; - conn.preferenceToTrace("seed: " + getSeed().toString()); - trace = conn.getTrace(); - } else { - trace = null; - } - return trace; - } - - public void setSeed(final RandomSeed seed) { - this.seed = seed; - } - - public RandomSeed getSeed() { - return seed; - } - public synchronized void setMachineDescription( final MachineDescription machineDescription) { this.description = machineDescription; @@ -186,13 +150,29 @@ public class AnimatorImpl { PrologTermStringOutput pto = new PrologTermStringOutput(); command.writeCommand(pto); final String query = pto.fullstop().toString(); - final Start ast = sendCommandImpl(query); Map<String, PrologTerm> bindings; try { - bindings = BindingGenerator.createBindingMustNotFail(query, ast); - } catch (de.prob.parser.ResultParserException e) { - Logger.notifyUser(e.getMessage()); - throw new CommandException(e.getMessage()); + PResult topnode; + synchronized (this) { + topnode = connector.sendCommand(query); + } + // If probcli doesn't return anything, sendCommand throws an exception. + assert topnode != null; + // Progress and callback results are handled inside sendCommand. + assert !(topnode instanceof AProgressResult); + assert !(topnode instanceof ACallBackResult); + + if (!(topnode instanceof AYesResult)) { + String queryForMessage = query; + if (queryForMessage.length() > 400) { + queryForMessage = queryForMessage.substring(0, 400) + "..."; + } + throw new ResultParserException("Prolog query failed - received " + topnode.getClass().getSimpleName() + " in response to query: " + queryForMessage, null); + } + bindings = BindingGenerator.createBinding(PrologTermGenerator.toPrologTerm(topnode)); + } catch (ResultParserException e) { + Logger.notifyUser(e.getMessage(), e); + throw new CommandException(e.getMessage(), e); } return new SimplifiedROMap<String, PrologTerm>(bindings); } diff --git a/de.prob.core/src/de/prob/core/internal/Message.java b/de.prob.core/src/de/prob/core/internal/Message.java deleted file mode 100644 index 7172c5fd7333a9f3679f681fe48d90eaa0426689..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/Message.java +++ /dev/null @@ -1,32 +0,0 @@ -/** - * (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.internal; - -public class Message { - - public static enum Type { - QUERY, ANSWER, LOG, PREFERENCE - }; - - private final Type type; - - private final String message; - - public Message(final Type type, final String message) { - this.message = message; - this.type = type; - } - - public String getMessage() { - return message; - } - - public Type getType() { - return type; - } - -} diff --git a/de.prob.core/src/de/prob/core/internal/ProBResultParser.java b/de.prob.core/src/de/prob/core/internal/ProBResultParser.java deleted file mode 100644 index 85eb4960e745ef475fc138e34932bdfd5fdf114b..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/ProBResultParser.java +++ /dev/null @@ -1,61 +0,0 @@ -/** - * (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.internal; - -import java.io.IOException; -import java.io.PushbackReader; -import java.io.StringReader; - -import de.prob.core.ProblemHandler; -import de.prob.core.sablecc.lexer.Lexer; -import de.prob.core.sablecc.lexer.LexerException; -import de.prob.core.sablecc.node.Start; -import de.prob.core.sablecc.parser.Parser; -import de.prob.core.sablecc.parser.ParserException; -import de.prob.exceptions.ProBAssertionFailed; -import de.prob.logging.Logger; - -public final class ProBResultParser { - - private ProBResultParser() { - throw new UnsupportedOperationException( - "not intended for instantiation"); - } - - public static Start parse(final String prologAnswer) - throws ResultParserException, ProBAssertionFailed { - - Logger.assertProB("prologAnswer.length() != 0", - prologAnswer.length() != 0); - - final PushbackReader codeReader = new PushbackReader(new StringReader( - prologAnswer), prologAnswer.length()); - final Lexer lexer = new Lexer(codeReader); - final Parser parser = new Parser(lexer); - Start parseResult = null; - try { - parseResult = parser.parse(); - } catch (final ParserException e) { - String message = "Internal Error while parsing ProB Answer. This ist most likly a bug in the Resultparser. String was: '" - + prologAnswer - + "'. Last Token was '" - + e.getToken() - + "': " + e.getLocalizedMessage(); - ProblemHandler.handleResultPareserException(message, e); - } catch (final LexerException e) { - String message = "Internal Error while parsing ProB Answer. This ist most likly a bug in the Resultparser String was: '" - + prologAnswer + "': " + e.getLocalizedMessage(); - ProblemHandler.handleResultPareserException(message, e); - } catch (final IOException e) { - String message = "Internal Error while parsing ProB Answer. This ist most likly a bug in the Resultparser String was: " - + prologAnswer + "': " + e.getLocalizedMessage(); - ProblemHandler.handleResultPareserException(message, e); - } - - return parseResult; - } -} \ No newline at end of file diff --git a/de.prob.core/src/de/prob/core/internal/ResultParserException.java b/de.prob.core/src/de/prob/core/internal/ResultParserException.java deleted file mode 100644 index 5b3b0aa5b1701a441ec386a256c173d5795b60b3..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/ResultParserException.java +++ /dev/null @@ -1,18 +0,0 @@ -/** - * (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.internal; - -import de.prob.exceptions.ProBException; - -public class ResultParserException extends ProBException { - private static final long serialVersionUID = 4607280354438003272L; - - public ResultParserException(final String message, final Throwable t) { - super(message, t, true); - } - -} diff --git a/de.prob.core/src/de/prob/core/internal/ServerConnection.java b/de.prob.core/src/de/prob/core/internal/ServerConnection.java index a593d273f35faff3ce93117d418c1c64cefe1951..c317ef494aa0fbeb1c8b9456d7c25de1f2c566f3 100644 --- a/de.prob.core/src/de/prob/core/internal/ServerConnection.java +++ b/de.prob.core/src/de/prob/core/internal/ServerConnection.java @@ -16,35 +16,27 @@ import java.nio.charset.Charset; import de.prob.cli.CliException; import de.prob.cli.CliStarter; -import de.prob.core.IServerConnection; import de.prob.core.ProblemHandler; +import de.prob.core.sablecc.node.ACallBackResult; +import de.prob.core.sablecc.node.AProgressResult; +import de.prob.core.sablecc.node.PResult; import de.prob.exceptions.ProBException; import de.prob.logging.Logger; +import de.prob.parser.ProBResultParser; -public class ServerConnection implements IServerConnection { - +public class ServerConnection { private Socket socket = null; private BufferedInputStream inputStream = null; private PrintStream outputStream = null; private CliStarter cli = null; - private String lastCommand; - private volatile boolean shutdown = true; - // private static final ScheduledExecutorService exec = new - // ScheduledThreadPoolExecutor( - // 1); - private void startcli(final File file) throws CliException { cli = new CliStarter(file); } - public String getLastCommand() { - return lastCommand; - } - private void establishConnection(final int port) throws CliException { try { socket = new Socket(InetAddress.getByName(null), port); @@ -62,24 +54,29 @@ public class ServerConnection implements IServerConnection { outputStream = null; } } - ProblemHandler.handleCliException( - "Opening connection to ProB server failed", e); + throw new CliException("Opening connection to ProB server failed", e, false); } } - @Override - public String sendCommand(final String commandString) throws ProBException { + public PResult sendCommand(final String commandString) throws ProBException { if (shutdown) { final String message = "probcli is currently shutting down"; ProblemHandler.raiseCliException(message); } checkState(); sendQuery(commandString); - return getAnswer(); + PResult topnode = ProBResultParser.parse(getAnswer()).getPResult(); + // Skip over all progress and callback results, which we don't support here (yet?). + while (topnode instanceof AProgressResult || topnode instanceof ACallBackResult) { + if (topnode instanceof ACallBackResult) { + sendQuery("call_back_not_supported."); + } + topnode = ProBResultParser.parse(getAnswer()).getPResult(); + } + return topnode; } private void sendQuery(final String commandString) throws ProBException { - lastCommand = commandString; Logger.assertProB("commandString.trim().endsWith(\".\")", commandString .trim().endsWith(".")); @@ -103,24 +100,6 @@ public class ServerConnection implements IServerConnection { return input; } - // private String timedRun(final Callable<String> r, final long timeOut, - // final TimeUnit unit) throws InterruptedException, ProBException { - // String s = null; - // Future<String> task = exec.submit(r); - // try { - // s = task.get(timeOut, unit); - // } catch (TimeoutException e) { - // final String message = "Timeout while waiting for ProB's answer"; - // ProblemHandler.handleCliException(message, e); - // } catch (ExecutionException e) { - // final String message = e.getCause().getLocalizedMessage(); - // ProblemHandler.handleCliException(message, e.getCause()); - // } finally { - // task.cancel(true); - // } - // return s; - // } - protected String readAnswer() throws IOException { final StringBuilder result = new StringBuilder(); final byte[] buffer = new byte[1024]; @@ -157,7 +136,6 @@ public class ServerConnection implements IServerConnection { return result.length() > 0 ? result.toString() : null; } - @Override public void startup(final File file) throws CliException { if (shutdown) { startcli(file); @@ -165,12 +143,10 @@ public class ServerConnection implements IServerConnection { shutdown = false; } else { // This should never happen - final String message = "Tried to start a server that is already running"; - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser("Tried to start a server that is already running"); } } - @Override public void shutdown() { if (!shutdown) { if (socket != null) { @@ -197,12 +173,6 @@ public class ServerConnection implements IServerConnection { } } - @Override - public int getCliPortNumber() { - return cli.getPort(); - } - - @Override public void sendUserInterruptSignal() { if (cli != null) { cli.sendUserInterruptReference(); diff --git a/de.prob.core/src/de/prob/core/internal/ServerTraceConnection.java b/de.prob.core/src/de/prob/core/internal/ServerTraceConnection.java deleted file mode 100644 index 4eaea64c06a770f77a8b0a52a75df0ac010367b4..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/ServerTraceConnection.java +++ /dev/null @@ -1,124 +0,0 @@ -/** - * (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.internal; - -import java.io.File; -import java.io.IOException; -import java.text.SimpleDateFormat; - -import org.eclipse.core.runtime.ILogListener; -import org.eclipse.core.runtime.IStatus; - -import de.prob.cli.CliException; -import de.prob.core.ITrace; -import de.prob.core.internal.Message.Type; -import de.prob.exceptions.ProBException; -import de.prob.logging.Logger; - -public class ServerTraceConnection extends ServerConnection implements - ILogListener { - - private static final int TRACE_SIZE_LIMIT = 100; - - private Trace trace; - - @Override - public void startup(final File file) throws CliException { - super.startup(file); - trace = new Trace(TRACE_SIZE_LIMIT); - logToTrace("ServerTraceConnection.startup(): " + getCurrentTime()); - Logger.addListener(this); - } - - @Override - public void shutdown() { - super.shutdown(); - logToTrace("ServerTraceConnection.shutdown(): " + getCurrentTime()); - } - - @Override - public String sendCommand(final String commandString) throws ProBException { - sendMessage(commandString); - return super.sendCommand(commandString); - } - - @Override - protected String readAnswer() throws IOException { - String answer = super.readAnswer(); - receiveMessage(answer); - return answer; - - } - - private void sendMessage(final String content) { - trace.addMessage(Type.QUERY, content); - } - - private void receiveMessage(final String content) { - trace.addMessage(Type.ANSWER, content); - } - - private final String getCurrentTime() { - SimpleDateFormat date = new SimpleDateFormat( - "yyyy.MM.dd ' - ' HH:mm:ss"); - Long timemillis = System.currentTimeMillis(); - - return "Time: " + Long.toString(timemillis) + " - " - + date.format(timemillis); - } - - /** - * Adds a {@link Message} with the Type = LOG to the actual Tracing - * {@link ITrace} - * - * @param String - * message - */ - public final void logToTrace(final String message) { - trace.addMessage(Type.LOG, message); - } - - /** - * Adds a {@link Message} with the Type = PREFERENCE to the actual Tracing - * {@link ITrace} - * - * @param String - * message - */ - public final void preferenceToTrace(final String message) { - trace.addMessageOnTop(Type.PREFERENCE, message); - } - - /** - * - * @return {@link ITrace}, containing all Logs, Queries and Answers that - * passed this ServerTraceConnection - */ - - public final ITrace getTrace() { - logToTrace(getCurrentTime()); - return trace; - } - - /** - * Adds a Error-Log-Message to the trace - */ - public void logging(final IStatus status, final String plugin) { - if (status.getSeverity() == IStatus.ERROR) { - StringBuffer message = new StringBuffer(); - message.append(status.getMessage()); - - if (status.getException() != null) { - message.append("\n"); - message.append(status.getException().getLocalizedMessage()); - } - logToTrace(message.toString()); - - } - - } -} diff --git a/de.prob.core/src/de/prob/core/internal/SimplifiedROMap.java b/de.prob.core/src/de/prob/core/internal/SimplifiedROMap.java deleted file mode 100644 index 4fab4610a338dd222de919d0eb14e38d977da2a4..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/SimplifiedROMap.java +++ /dev/null @@ -1,41 +0,0 @@ -/** - * - */ -package de.prob.core.internal; - -import java.util.Map; -import java.util.Map.Entry; -import java.util.Set; - -import de.prob.parser.ISimplifiedROMap; - -/** - * The default implementation of {@link SimplifiedROMap}, which is just a - * wrapper around a {@link Map}. - * - * @author plagge - */ -public class SimplifiedROMap<K, V> implements ISimplifiedROMap<K, V> { - private final Map<K, V> map; - - public SimplifiedROMap(final Map<K, V> map) { - this.map = map; - } - - public V get(final K key) { - return map.get(key); - } - - @Override - public String toString() { - StringBuffer sb = new StringBuffer(); - Set<Entry<K, V>> entrySet = map.entrySet(); - for (Entry<K, V> entry : entrySet) { - sb.append(entry.getKey()); - sb.append("->"); - sb.append(entry.getValue()); - sb.append(" "); - } - return sb.toString(); - } -} diff --git a/de.prob.core/src/de/prob/core/internal/Trace.java b/de.prob.core/src/de/prob/core/internal/Trace.java deleted file mode 100644 index 1fa86cdfe0149f4b626f89ec205980da7c1f552c..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/Trace.java +++ /dev/null @@ -1,170 +0,0 @@ -/** - * (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.internal; - -import java.io.BufferedReader; -import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; -import java.util.Collections; -import java.util.LinkedList; -import java.util.List; - -import de.prob.core.ITrace; -import de.prob.core.internal.Message.Type; - -/** - * TODO: Maybe a part of the trace should be dumped to a file, to prevent a high - * memory consumption. - */ -public class Trace implements ITrace { - - private final LinkedList<Message> list = new LinkedList<Message>(); - private Integer maximum; - - public Trace() { - this(null); - } - - public Trace(final int maximum) { - this(Integer.valueOf(maximum)); - } - - private Trace(final Integer maximum) { - this.maximum = maximum; - } - - /** - * @return the List of logged messages as unmodifiable List of Strings - */ - public final List<Message> getTraceAsList() { - return Collections.unmodifiableList(list); - } - - /** - * @return the List of logged messages as a String - */ - public final String getTraceAsString() { - StringBuffer buffer = new StringBuffer(); - - for (Message message : list) { - buffer.append(starterString(message.getType())); - buffer.append(message.getMessage()); - buffer.append(stopperString(message.getType())); - } - return buffer.toString(); - } - - public final void addMessage(final Type type, final String message) { - list.add(new Message(type, message)); - limit(); - } - - public final void addMessageOnTop(final Type type, final String message) { - list.add(1, new Message(type, message)); - limit(); - } - - private final String starterString(final Type type) { - return "@START " + type + "\n"; - } - - private final String stopperString(final Type type) { - return "\n@END " + type + "\n"; - } - - public static final ITrace traceFromStream(final InputStream stream) { - final Trace trace = new Trace(); - BufferedReader reader = null; - try { - reader = new BufferedReader(new InputStreamReader(stream)); - iterateOverLines(trace, reader); - } catch (IOException e) { - System.out.println(trace.getClass().getName() - + ": IOException at Filehandling"); - e.printStackTrace(); - } finally { - if (reader != null) { - try { - reader.close(); - } catch (IOException e) { - // IGNORE - } - } - } - return trace; - } - - private static void iterateOverLines(final Trace trace, - final BufferedReader reader) throws IOException { - StringBuffer buffer = new StringBuffer(); - - String line = reader.readLine(); - while (null != line) { - final boolean restartBuffer = collect(line, trace, buffer); - if (restartBuffer) { - buffer = new StringBuffer(); - } - line = reader.readLine(); - } - } - - private static final boolean collect(final String line, final Trace trace, - final StringBuffer buffer) { - final boolean restartBuffer; - if (line.startsWith("@START")) { - restartBuffer = true; - } else { - restartBuffer = false; - Type type; - if (line.startsWith("@END ")) { - final String typeString = line.substring(5); - try { - type = Type.valueOf(typeString); - } catch (IllegalArgumentException e) { - // the string does not represent one of our types - type = null; - } - } else { - type = null; - } - if (type != null) { - trace.addMessage(type, buffer.toString()); - } else { - buffer.append(line); - } - } - return restartBuffer; - } - - public int size() { - return list == null ? 0 : list.size(); - } - - @Override - public void setMaximum(final Integer max) { - if (max != null && max < 0) - throw new IllegalArgumentException("Non-negative maximum expected"); - maximum = max; - limit(); - } - - private void limit() { - if (maximum != null && list != null) { - final int toRemove = list.size() - maximum; - for (int i = 0; i < toRemove; i++) { - list.removeFirst(); - } - } - } - - @Override - public Integer getMaximum() { - return maximum; - } - -} diff --git a/de.prob.core/src/de/prob/core/internal/TraceConnectionProvider.java b/de.prob.core/src/de/prob/core/internal/TraceConnectionProvider.java deleted file mode 100644 index 25676a1c2e5c326ce925fd8d9d0b4ab849fbc5a4..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/core/internal/TraceConnectionProvider.java +++ /dev/null @@ -1,26 +0,0 @@ -/** - * (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.internal; - -import de.prob.core.IConnectionProvider; -import de.prob.core.IServerConnection; - -/** - * Provides a new {@link ServerTraceConnection} - */ -public class TraceConnectionProvider implements IConnectionProvider { - - /** - * - * @return new {@link ServerTraceConnection} - */ - public final IServerConnection getISeverConnection() { - ServerTraceConnection conn = new ServerTraceConnection(); - return conn; - } - -} diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java index 8fa94a5de2e41f821f52d679f6f7ee00ded78da1..fffe0da3d4e3a4cfd2375b77f9cbe0f3cb3f13ef 100644 --- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java @@ -15,6 +15,8 @@ import java.util.Map; import org.eclipse.core.runtime.Assert; import org.eclipse.core.runtime.CoreException; +import org.eventb.core.EventBAttributes; +import org.eventb.core.IAxiom; import org.eventb.core.IContextRoot; import org.eventb.core.IEventBRoot; import org.eventb.core.IExtendsContext; @@ -45,6 +47,7 @@ import de.be4.classicalb.core.parser.node.AAbstractConstantsContextClause; import de.be4.classicalb.core.parser.node.AAxiomsContextClause; import de.be4.classicalb.core.parser.node.AConstantsContextClause; import de.be4.classicalb.core.parser.node.ADeferredSetSet; +import de.be4.classicalb.core.parser.node.ADescriptionPredicate; import de.be4.classicalb.core.parser.node.AEventBContextParseUnit; import de.be4.classicalb.core.parser.node.AExtendsContextClause; import de.be4.classicalb.core.parser.node.AIdentifierExpression; @@ -56,6 +59,7 @@ import de.be4.classicalb.core.parser.node.PExpression; import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.PSet; import de.be4.classicalb.core.parser.node.TIdentifierLiteral; +import de.be4.classicalb.core.parser.node.TPragmaFreeText; import de.hhu.stups.sablecc.patch.SourcePosition; import de.prob.core.translator.TranslationFailedException; import de.prob.eventb.translator.internal.EProofStatus; @@ -373,8 +377,18 @@ public final class ContextTranslator extends AbstractComponentTranslator { for (final ISCAxiom element : predicates) { if (element.isTheorem() == theorems) { final PPredicate predicate = translatePredicate(ff, te, element); - list.add(predicate); - labelMapping.put(predicate, element); + final IAxiom uca = (IAxiom) element.getSource(); // comments only attached in unchecked source + if (uca.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) { + final String commentString = uca.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE); + //System.out.println("Axiom/theorem " + element + " has description " + commentString); + final TPragmaFreeText desc = new TPragmaFreeText(commentString); + final ADescriptionPredicate dpred = new ADescriptionPredicate(desc,predicate); + list.add(dpred); + labelMapping.put(dpred, element); + } else { + list.add(predicate); + labelMapping.put(predicate, element); + } // proofspragmas.add(new ClassifiedPragma("discharged", // predicate, // Arrays.asList(new String[0]), Arrays diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java index 453e0c833a5859a01020060307df62b9cfebde78..499958e35518b32e799274d8e064d305ab0def16 100644 --- a/de.prob.core/src/de/prob/eventb/translator/Theories.java +++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java @@ -15,6 +15,7 @@ import org.eclipse.core.runtime.CoreException; import org.eclipse.core.runtime.IPath; import org.eclipse.core.runtime.Path; import org.eventb.core.IEventBProject; +import org.eventb.core.EventBAttributes; import org.eventb.core.ISCIdentifierElement; import org.eventb.core.ast.Expression; import org.eventb.core.ast.Formula; @@ -245,15 +246,8 @@ public class Theories { private static void printMappings(Collection<OperatorMapping> mappings, IPrologTermOutput pto) { pto.openList(); - // Currently, we support only one kind of operator mapping, just tagging - // an operator to indicate that an optimized ProB implementation should - // be used. We do not invest any effort in preparing future kinds of - // other operator mappings. for (OperatorMapping mapping : mappings) { - pto.openTerm("tag"); - pto.printAtom(mapping.getOperatorName()); - pto.printAtom(mapping.getSpec()); - pto.closeTerm(); + mapping.printProlog(pto); } pto.closeList(); } @@ -288,7 +282,7 @@ public class Theories { pto.closeList(); pto.openList(); for (ISCDatatypeConstructor cons : def.getConstructors()) { - printConstructor(cons, ff, pto); + printConstructor(cons, def, ff, pto); } pto.closeList(); pto.closeTerm(); @@ -296,12 +290,13 @@ public class Theories { } private static void printConstructor(ISCDatatypeConstructor cons, + ISCDatatypeDefinition def, FormulaFactory ff, IPrologTermOutput pto) throws CoreException { pto.openTerm("constructor"); pto.printAtom(cons.getIdentifierString()); pto.openList(); for (ISCConstructorArgument arg : cons.getConstructorArguments()) { - printTypedIdentifier("destructor", arg, ff, pto); + printTypedIdentifierForRecursiveDataTypeDef("destructor", arg, def, ff, pto); } pto.closeList(); pto.closeTerm(); @@ -322,7 +317,7 @@ public class Theories { throws CoreException { prologOutput.openTerm("operator"); - prologOutput.printAtom(opDef.getLabel()); + prologOutput.printAtom(opDef.getLabel()); // Name of the operator final FormulaFactory ff = theory.getFormulaFactory(); final ITypeEnvironment teFromFF = theory.getTypeEnvironment(ff); @@ -337,6 +332,10 @@ public class Theories { } // WD Condition + // TODO: does not seem to get the user-defined WD conditions + // we should probably call in INewOperatorDefinition.java : IOperatorWDCondition[] getOperatorWDConditions() throws RodinDBException; + // and convert this to a Predicate + // but above we have ISCNewOperatorDefinition and not INewOperatorDefinition Predicate wdCondition = opDef.getWDCondition(ff, te); printPredicate(prologOutput, wdCondition); @@ -377,13 +376,12 @@ public class Theories { prologOutput.openTerm("case"); prologOutput.printAtom(indArg); prologOutput.openList(); - if(ex==null) { - throw new IllegalStateException("Empty expression for axiomatic recursive definition case " + es + - " and inductive argument " + indArg); + if (ex == null) { + throw new IllegalStateException("Empty expression for axiomatic recursive definition case " + es + " and inductive argument " + indArg); } else { - for (FreeIdentifier fi : ex.getFreeIdentifiers()) { - prologOutput.printAtom(fi.getName()); - } + for (FreeIdentifier fi : ex.getFreeIdentifiers()) { + prologOutput.printAtom(fi.getName()); + } } prologOutput.closeList(); printExpression(prologOutput, ex); @@ -420,6 +418,7 @@ public class Theories { Predicate pp = (Predicate) scFormula; printPredicate(prologOutput, pp); } + // TODO: we could insert the result type in the Prolog term; or at least if we have a pred or expr if (scFormula instanceof Expression) { Expression pp = (Expression) scFormula; printExpression(prologOutput, pp); @@ -428,13 +427,57 @@ public class Theories { } } + private static void printTypedIdentifierForRecursiveDataTypeDef(final String functor, + final ISCIdentifierElement id, + final ISCDatatypeDefinition def, + final FormulaFactory ff, + final IPrologTermOutput pto) throws CoreException { + pto.openTerm(functor); + pto.printAtom(id.getIdentifierString()); + final String typeString = id.getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE); + // todo: is there a better way to check if type refers recursively to def? do we need to trim typeString? + // System.out.println("Inductive datatype: " + def.getIdentifierString() + " destructor arg has type: " + typeString); + if (def.getIdentifierString().equals(typeString)) { + // the checked theory files tcf no longer contain the type paras + // the tuf file may contain org.eventb.theory.core.type="Baum(L)" + // the tcf file now contains org.eventb.theory.core.type="Baum" + // getType would lead to a CoreException + // we print the type of the recursive data type directly + printTypeOfDataType(def,ff,pto); + } else { + Type type = id.getType(ff); + printType(type, pto); + } + pto.closeTerm(); + } + + // print the base type of a data type definition as an extended_expr + private static void printTypeOfDataType( + final ISCDatatypeDefinition def, + final FormulaFactory ff, + final IPrologTermOutput pto) throws CoreException { + pto.openTerm("extended_expr"); + pto.printAtom("none"); + pto.printAtom(def.getIdentifierString()); + pto.openList(); + for (ISCTypeArgument arg : def.getTypeArguments()) { + printType(arg.getSCGivenType(ff), pto); + } + pto.closeList(); + pto.openList(); // empty list of predicate args + pto.closeList(); + pto.closeTerm(); + } + private static void printTypedIdentifier(final String functor, final ISCIdentifierElement id, final FormulaFactory ff, final IPrologTermOutput pto) throws CoreException { pto.openTerm(functor); pto.printAtom(id.getIdentifierString()); + Type type = id.getType(ff); printType(type, pto); + pto.closeTerm(); } @@ -492,6 +535,7 @@ public class Theories { pto.openList(); // WD condition missing pto.closeList(); + // Result type is not written; we can maybe get it from: Formula<?> scFormula = def.getSCFormula(ff, te); pto.closeTerm(); } pto.closeList(); diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java index 7cf350f8108d9236c0cef6b0349c268096c1757a..0843445fe39450edd6f8a013355fba14ab111d0a 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java @@ -1,5 +1,5 @@ /** - * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich + * (c) 2009-2024 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) * */ @@ -12,6 +12,8 @@ import java.util.LinkedList; import java.util.List; import org.eclipse.core.runtime.CoreException; +import org.eventb.core.EventBAttributes; +import org.eventb.core.ICommentedElement; import org.eventb.core.IConvergenceElement.Convergence; import org.eventb.core.ILabeledElement; import org.eventb.core.IMachineRoot; @@ -19,7 +21,10 @@ import org.eventb.core.IPOSequent; import org.eventb.core.IPOSource; import org.eventb.core.IPSRoot; import org.eventb.core.IPSStatus; +import org.eventb.core.IPredicateElement; import org.eventb.core.ISCAction; +import org.eventb.core.IEvent; +import org.eventb.core.IInvariant; import org.eventb.core.ISCEvent; import org.eventb.core.ISCGuard; import org.eventb.core.ISCInternalContext; @@ -47,6 +52,8 @@ import org.rodinp.core.RodinDBException; import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus; import de.be4.classicalb.core.parser.node.AConvergentEventstatus; +import de.be4.classicalb.core.parser.node.ADescriptionEvent; +import de.be4.classicalb.core.parser.node.ADescriptionPredicate; import de.be4.classicalb.core.parser.node.AEvent; import de.be4.classicalb.core.parser.node.AEventBModelParseUnit; import de.be4.classicalb.core.parser.node.AEventsModelClause; @@ -68,6 +75,7 @@ import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.PSubstitution; import de.be4.classicalb.core.parser.node.PWitness; import de.be4.classicalb.core.parser.node.TIdentifierLiteral; +import de.be4.classicalb.core.parser.node.TPragmaFreeText; import de.prob.core.translator.TranslationFailedException; import de.prob.eventb.translator.AbstractComponentTranslator; import de.prob.logging.Logger; @@ -114,8 +122,7 @@ public class ModelTranslator extends AbstractComponentTranslator { public AEventBModelParseUnit getModelAST() { if (broken) { - final String message = "The machine contains Rodin Problems. ProB will continue, but you may observe unexpected behaviour"; - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser("The machine contains Rodin Problems. ProB will continue, but you may observe unexpected behaviour"); return model; } return model; @@ -349,7 +356,24 @@ public class ModelTranslator extends AbstractComponentTranslator { event.setTheorems(theorems); event.setWitness(extractWitnesses(revent, localEnv)); event.setAssignments(extractActions(revent, localEnv)); - eventsList.add(event); + // Events have comments, but they are no longer present in the statically checked events + // hence we get the original unchecked source: + final IEvent ucevent = (IEvent) revent.getSource(); + // this also works to access comment field; not sure which version is better: + //if((ucevent instanceof ICommentedElement) && ((ICommentedElement) ucevent).hasComment()) { + // System.out.println("Description 1 of " + revent.getLabel() + ": " + ((ICommentedElement) ucevent).getComment()); + //} + if (ucevent.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) { + final String commentString = ucevent.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE); + System.out.println("Event " + revent.getLabel() + " has description " + commentString); + final ADescriptionEvent devent = new ADescriptionEvent(); + devent.setEvent(event); + final TPragmaFreeText desc = new TPragmaFreeText(commentString); + devent.setContent(desc); + eventsList.add(devent); // we add the event with a description node around it; requires new probcli + } else { + eventsList.add(event); + } } clause.setEvent(eventsList); return clause; @@ -513,8 +537,18 @@ public class ModelTranslator extends AbstractComponentTranslator { if (isDefinedHere(evPredicate)) { final PPredicate predicate = translatePredicate(ff, te, evPredicate); - list.add(predicate); - labelMapping.put(predicate, evPredicate); + final IInvariant ucp = (IInvariant) evPredicate.getSource(); // comments only attached in unchecked source + if (ucp.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) { + final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE); + //System.out.println("Invariant/theorem " + predicate + " has description " + commentString); + final TPragmaFreeText desc = new TPragmaFreeText(commentString); + final ADescriptionPredicate dpred = new ADescriptionPredicate(desc,predicate); + list.add(dpred); + labelMapping.put(dpred, evPredicate); + } else { + list.add(predicate); + labelMapping.put(predicate, evPredicate); + } } } return list; diff --git a/de.prob.core/src/de/prob/logging/Logger.java b/de.prob.core/src/de/prob/logging/Logger.java index 678c5ddce1eba6f6d1eb83772c35177e8e8b3258..2893acd1d4090b9807eacf575455e122579236f9 100644 --- a/de.prob.core/src/de/prob/logging/Logger.java +++ b/de.prob.core/src/de/prob/logging/Logger.java @@ -23,13 +23,6 @@ import de.prob.parser.BindingGenerator; * */ public final class Logger { - - public static final int DEBUG = 0; - public static final int INFO = 1; - public static final int WARNING = 2; - public static final int BUGREPORT = 4; - public static final int NOBUGREPORT = 8; - /** * Registers a new {@link ILogListener}. The listener's * {@link ILogListener#logging(IStatus, String)} method is called, if @@ -42,8 +35,8 @@ public final class Logger { } /** - * Notifies the User about a fatal problem by adding a - * {@link Logger#FATALERROR} to the log. This method takes a message + * Notifies the User about a fatal problem by adding an error + * to the log. This method takes a message * describing the problem as well as an exception. * <p> * Note: Use this only if you don't want to throw an exception. If you want @@ -59,22 +52,13 @@ public final class Logger { */ public static void notifyUser(final String message, final Throwable throwable) { - log(IStatus.ERROR, BUGREPORT, message, throwable); + log(IStatus.ERROR, message, throwable); } public static void notifyUser(final String message) { notifyUser(message, null); } - public static void notifyUserWithoutBugreport(final String message, - final Throwable throwable) { - log(IStatus.ERROR, NOBUGREPORT, message, throwable); - } - - public static void notifyUserWithoutBugreport(final String message) { - notifyUserWithoutBugreport(message, null); - } - /** * Check a property. The method notifies the user and throws an exception if * the assertion fails. <br> @@ -131,10 +115,8 @@ public final class Logger { assertProB(assertion, false); } - public static void log(final int severity, final int code, - final String message, final Throwable exception) { - final IStatus status = new Status(severity, Activator.PLUGIN_ID, code, - message, exception); + public static void log(final int severity, final String message, final Throwable exception) { + final IStatus status = new Status(severity, Activator.PLUGIN_ID, message, exception); log(status); } @@ -151,8 +133,4 @@ public final class Logger { private static void log(final IStatus status) { Activator.getDefault().getLog().log(status); } - - public static void notifyUserAboutWarningWithoutBugreport(String string) { - log(IStatus.WARNING, NOBUGREPORT, string, null); - } } diff --git a/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java b/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java index 8d5d92358fd835a438dd28cebd1ae54d89d8c967..e1c43110ac4e67f75d4f3a167b351bba08ad1e1e 100644 --- a/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java +++ b/de.prob.core/src/de/prob/sap/commands/GenerateLocalTestcasesCommand.java @@ -12,7 +12,7 @@ import de.prob.core.command.IComposableCommand; import de.prob.exceptions.ProBException; import de.prob.parser.ISimplifiedROMap; import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.IntegerPrologTerm; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.PrologTerm; public class GenerateLocalTestcasesCommand implements IComposableCommand { @@ -41,10 +41,8 @@ public class GenerateLocalTestcasesCommand implements IComposableCommand { public void processResult( final ISimplifiedROMap<String, PrologTerm> bindings) throws CommandException { - final int sat = ((IntegerPrologTerm) bindings.get("SAT")).getValue() - .intValue(); - final int unsat = ((IntegerPrologTerm) bindings.get("UNSAT")) - .getValue().intValue(); + final int sat = ((AIntegerPrologTerm) bindings.get("SAT")).intValueExact(); + final int unsat = ((AIntegerPrologTerm) bindings.get("UNSAT")).intValueExact(); result = new LocalTestcasesResult(sat, unsat); } diff --git a/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java b/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java index 3ba18c58aaab0d92c024335c5091706a02ffa718..5cfa51cedb7abb4c4c114254d459880e73eb597b 100644 --- a/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java +++ b/de.prob.core/src/de/prob/sap/commands/GenerateTestcaseCommand.java @@ -25,7 +25,7 @@ import de.prob.core.command.LoadEventBModelCommand; import de.prob.exceptions.ProBException; import de.prob.parser.ISimplifiedROMap; import de.prob.prolog.output.IPrologTermOutput; -import de.prob.prolog.term.IntegerPrologTerm; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; import de.prob.sap.exceptions.ParseProblemException; @@ -133,9 +133,9 @@ public class GenerateTestcaseCommand implements IComposableCommand { public void processResult( final ISimplifiedROMap<String, PrologTerm> bindings) throws CommandException { - final IntegerPrologTerm pNumberTests = (IntegerPrologTerm) bindings + final AIntegerPrologTerm pNumberTests = (AIntegerPrologTerm) bindings .get(NUMBER_TESTCASES); - final int numberOfTests = pNumberTests.getValue().intValue(); + final int numberOfTests = pNumberTests.intValueExact(); final ListPrologTerm pEvents = (ListPrologTerm) bindings .get(UNCOVERED_EVENTS); diff --git a/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF b/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF index d945ff3db1f745f286662a85397c2096eb8f03cf..5c576f965f2a02bbf5e545be8f726771ab48f6e1 100644 --- a/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF +++ b/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF @@ -2,9 +2,9 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: ProB Disprover Core for EventB Bundle-SymbolicName: de.prob.eventb.disprover.core;singleton:=true -Bundle-Version: 2.1.0.qualifier +Bundle-Version: 2.1.1.qualifier Bundle-Vendor: Heinrich-Heine University Dusseldorf -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.runtime;bundle-version="[3.20.0,4.0.0)", org.eventb.core;bundle-version="[3.5.0,4.0.0)", org.eventb.core.ast;bundle-version="[3.5.0,4.0.0)", diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java index d4074c2b254fd2011d14741a2640c46190c22abb..0e9309ca46bf6bfdea5c4da1fb35db282824d47b 100644 --- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java +++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java @@ -3,7 +3,17 @@ package de.prob.eventb.disprover.core; import java.util.HashSet; import java.util.Set; -import org.eclipse.core.runtime.Status; +import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; +import de.be4.classicalb.core.parser.node.AEventBContextParseUnit; +import de.prob.core.Animator; +import de.prob.eventb.disprover.core.internal.DisproverCommand; +import de.prob.eventb.disprover.core.internal.ICounterExample; +import de.prob.eventb.disprover.core.translation.DisproverContextCreator; +import de.prob.eventb.translator.internal.TranslationVisitor; +import de.prob.logging.Logger; +import de.prob.prolog.output.PrologTermStringOutput; + +import org.eclipse.core.runtime.IStatus; import org.eventb.core.IEventBProject; import org.eventb.core.IPOSequent; import org.eventb.core.ast.Predicate; @@ -22,16 +32,6 @@ import org.eventb.core.seqprover.SerializeException; import org.rodinp.core.IRodinProject; import org.rodinp.core.RodinDBException; -import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; -import de.be4.classicalb.core.parser.node.AEventBContextParseUnit; -import de.prob.core.Animator; -import de.prob.eventb.disprover.core.internal.DisproverCommand; -import de.prob.eventb.disprover.core.internal.ICounterExample; -import de.prob.eventb.disprover.core.translation.DisproverContextCreator; -import de.prob.eventb.translator.internal.TranslationVisitor; -import de.prob.logging.Logger; -import de.prob.prolog.output.PrologTermStringOutput; - public class DisproverReasoner implements IReasoner { static final String DISPROVER_CONTEXT = "disprover_context"; @@ -62,7 +62,7 @@ public class DisproverReasoner implements IReasoner { timeoutFactor, pm); return createDisproverResult(ce, sequent, input); } catch (RodinDBException e) { - Logger.log(Logger.WARNING, Status.WARNING, e.getMessage(), e); + Logger.log(IStatus.WARNING, e.getMessage(), e); return ProverFactory.reasonerFailure(this, input, e.getMessage()); } catch (InterruptedException e) { return ProverFactory.reasonerFailure(this, input, e.getMessage()); diff --git a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF index c6dc929b64e23aa7f604c7a4592bdb5343d4111f..0a1957bc7ef479c7b3b00a6cbd52eebf4ec38f96 100644 --- a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF +++ b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF @@ -2,11 +2,11 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: ProB Disprover UI for EventB Bundle-SymbolicName: de.prob.eventb.disprover.ui;singleton:=true -Bundle-Version: 2.1.0.qualifier +Bundle-Version: 2.1.1.qualifier Bundle-Vendor: Heinrich-Heine University Dusseldorf -Require-Bundle: de.prob.core;bundle-version="[9.5.0,9.6.0)", - de.prob.eventb.disprover.core;bundle-version="[2.1.0,2.2.0)", - de.prob.ui;bundle-version="[7.5.0,7.6.0)", +Require-Bundle: de.prob.core;bundle-version="[9.5.1,9.6.0)", + de.prob.eventb.disprover.core;bundle-version="[2.1.1,2.2.0)", + de.prob.ui;bundle-version="[7.5.1,7.6.0)", org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)", org.eclipse.osgi;bundle-version="[3.16.0,4.0.0)", org.eclipse.ui;bundle-version="[3.118.0,4.0.0)", diff --git a/de.prob.plugin/META-INF/MANIFEST.MF b/de.prob.plugin/META-INF/MANIFEST.MF index 2806e06b0fad64ce2bf8dffb00ee977a33398566..1f14ba3395a4099bb25ad45877545300c9fce4f9 100644 --- a/de.prob.plugin/META-INF/MANIFEST.MF +++ b/de.prob.plugin/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: ProB Rodin2 UI Bindings Bundle-SymbolicName: de.prob.plugin;singleton:=true -Bundle-Version: 2.4.0.qualifier -Fragment-Host: de.prob.ui;bundle-version="[7.5.0,7.6.0)" +Bundle-Version: 2.4.1.qualifier +Fragment-Host: de.prob.ui;bundle-version="[7.5.1,7.6.0)" Bundle-RequiredExecutionEnvironment: JavaSE-11 Bundle-Vendor: HHU Düsseldorf STUPS Group diff --git a/de.prob.repository/category.xml b/de.prob.repository/category.xml new file mode 100644 index 0000000000000000000000000000000000000000..c4aa4d78350a3dc5be190fbf32415b8847478e74 --- /dev/null +++ b/de.prob.repository/category.xml @@ -0,0 +1,30 @@ +<?xml version="1.0" encoding="UTF-8"?> +<site> + + <feature id="de.prob2.disprover.feature" version="0.0.0"> + <category name="de.prob2.feature.category"/> + </feature> + + <feature id="de.prob2.feature" version="0.0.0"> + <category name="de.prob2.feature.category"/> + </feature> + + <feature id="de.prob2.symbolic.feature" version="0.0.0"> + <category name="de.prob2.feature.category"/> + </feature> + + <category-def name="de.prob2.feature.category" label="ProB for Rodin"> + <description> +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. + + </description> + </category-def> + +</site> diff --git a/de.prob.symbolic/META-INF/MANIFEST.MF b/de.prob.symbolic/META-INF/MANIFEST.MF index dab73e15140e3350149d415c125fb6ffd72836d5..64d027615331925583b685cee674cbc7fd03a8a6 100644 --- a/de.prob.symbolic/META-INF/MANIFEST.MF +++ b/de.prob.symbolic/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: ProB Symbolic Evaluation Support Bundle-SymbolicName: de.prob.symbolic;singleton:=true -Bundle-Version: 7.5.0.qualifier +Bundle-Version: 7.5.1.qualifier Bundle-Activator: de.prob.symbolic.Activator Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)", org.eclipse.ui;bundle-version="[3.118.0,4.0.0)", diff --git a/de.prob.ui/META-INF/MANIFEST.MF b/de.prob.ui/META-INF/MANIFEST.MF index 32157f7964fce02c82478482ea6c8f8050935305..5b62231a74b2ccec7e3311233ca296dc1b1929b8 100644 --- a/de.prob.ui/META-INF/MANIFEST.MF +++ b/de.prob.ui/META-INF/MANIFEST.MF @@ -2,8 +2,8 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: ProB Ui Plug-in Bundle-SymbolicName: de.prob.ui;singleton:=true -Bundle-Version: 7.5.0.qualifier -Require-Bundle: de.prob.core;bundle-version="[9.5.0,9.6.0)", +Bundle-Version: 7.5.1.qualifier +Require-Bundle: de.prob.core;bundle-version="[9.5.1,9.6.0)", org.eclipse.core.expressions;bundle-version="[3.7.0,4.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)", diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index fe42b2a1dc7b85af4ec8cee548048af2f3843c6a..19428acddec4b510d4274d03eba54bd8d0bbfda6 100644 --- a/de.prob.ui/plugin.xml +++ b/de.prob.ui/plugin.xml @@ -71,13 +71,6 @@ name="History" restorable="true"> </view> - <view - category="de.hhu.stups.prob" - class="de.prob.ui.ticket.LogView" - id="de.prob.ui.log" - name="ProB Log View" - restorable="true"> - </view> <view category="de.hhu.stups.prob" class="de.prob.ui.ltl.CounterExampleViewPart" diff --git a/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java b/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java index 8ffededed69fa0c2dc2986a8e82707f91fd97330..7562adf19fc3539f594b4172733fc5d76d93e606 100644 --- a/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java +++ b/de.prob.ui/src/de/prob/ui/ProBGeneralPreferences.java @@ -35,8 +35,8 @@ import de.prob.core.command.GetPreferencesCommand; import de.prob.core.domainobjects.ProBPreference; import de.prob.exceptions.ProBException; import de.prob.logging.Logger; +import de.prob.prolog.term.AIntegerPrologTerm; import de.prob.prolog.term.CompoundPrologTerm; -import de.prob.prolog.term.IntegerPrologTerm; import de.prob.prolog.term.ListPrologTerm; import de.prob.prolog.term.PrologTerm; @@ -154,12 +154,12 @@ public class ProBGeneralPreferences extends FieldEditorPreferencePage implements BooleanFieldEditor.SEPARATE_LABEL, parent); } else if (type.hasFunctor("range", 2)) { final CompoundPrologTerm range = (CompoundPrologTerm) type; - final BigInteger lower = ((IntegerPrologTerm) range.getArgument(1)) + final BigInteger lower = ((AIntegerPrologTerm) range.getArgument(1)) .getValue(); - final BigInteger upper = ((IntegerPrologTerm) range.getArgument(2)) + final BigInteger upper = ((AIntegerPrologTerm) range.getArgument(2)) .getValue(); - field = createIntField(name, desc, parent, lower.intValue(), upper - .intValue()); + field = createIntField(name, desc, parent, lower.intValueExact(), upper + .intValueExact()); } else if (type.isList()) { final ListPrologTerm typelist = (ListPrologTerm) type; final String[][] comboEntries = new String[typelist.size()][2]; diff --git a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java index 6a3b4744a75fa558a81e4f407442c2aa074d469c..d3b2c16f4aba64452cd443a20fb99adbbb051b44 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java +++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java @@ -47,9 +47,7 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter { ModelCheckingJob ccJob = (ModelCheckingJob) job; showResult(ccJob.getModelCheckingResult()); } else { - final String message = "The job has a wrong type. Expected ModelCheckingJob but got " - + job.getClass(); - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser("The job has a wrong type. Expected ModelCheckingJob but got " + job.getClass()); } } diff --git a/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java b/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java index c5832a0687232e40289c3e77577f165e4283a9a7..dc2f3e06c4b46ad77f24e014d05fb167c60c13fd 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/OpenClassicHandler.java @@ -36,7 +36,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { final String prob_location = getBinaryLocation(); if (prob_location == null) { - Logger.notifyUserWithoutBugreport("You need to specify a location for" + PROB_STANDALONE_NAME +". See Preferences -> ProB Standalone."); + Logger.notifyUser("You need to specify a location for" + PROB_STANDALONE_NAME +". See Preferences -> ProB Standalone."); } else { final IEventBRoot root = getSelection(); if (root != null) { @@ -53,7 +53,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { runProBClassic(prob_location, tmp); } } else { - Logger.notifyUserWithoutBugreport("You need to select a context or machine to open with " + PROB_STANDALONE_NAME); + Logger.notifyUser("You need to select a context or machine to open with " + PROB_STANDALONE_NAME); } } return null; @@ -97,7 +97,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { new Thread(new ClassicConsole(output)).start(); } catch (IOException e) { - Logger.notifyUserWithoutBugreport("You need to specify a correct location for " + Logger.notifyUser("You need to specify a correct location for " + PROB_CLASSIC_NAME + ". See Preferences -> ProB Standalone.\n" + PROB_CLASSIC_NAME + " location: "+ probBinary + "\nModel file: " + modelFile + @@ -121,7 +121,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { new Thread(new ClassicConsole(voutput)).start(); vprocess.waitFor(); // this blocks Rodin if (vprocess.exitValue() != 0) { - Logger.notifyUserWithoutBugreport("Failed to start java -version. Exit code: " + vprocess.exitValue()); + Logger.notifyUser("Failed to start java -version. Exit code: " + vprocess.exitValue()); } final String[] command = {"java", "-jar", probBinary, "--machine-file", modelFile}; @@ -136,7 +136,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { } catch (IOException | InterruptedException e) { // } catch (IOException e) { - Logger.notifyUserWithoutBugreport("You need to specify a correct location for " + Logger.notifyUser("You need to specify a correct location for " + PROB2_NAME + ". See Preferences -> ProB Standalone.\n" + PROB2_NAME + " location: "+ probBinary + "\nModel file: " + modelFile + @@ -157,7 +157,7 @@ public class OpenClassicHandler extends AbstractHandler implements IHandler { temp = File.createTempFile("prob_", ".eventb"); temp.deleteOnExit(); } catch (IOException e) { - Logger.notifyUserWithoutBugreport("Something went wrong while saving temp file.\n" + Logger.notifyUser("Something went wrong while saving temp file.\n" + e.getLocalizedMessage()); } return temp; diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java index 7ad28d5974a24fd3fbabc4499a96b1f97fbe733c..88c9ed078678e552a7402401b7a7f3c3a6d80a6c 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java @@ -17,6 +17,7 @@ import org.eclipse.core.resources.IResourceDelta; import org.eclipse.core.resources.ResourcesPlugin; import org.eclipse.core.runtime.CoreException; import org.eclipse.core.runtime.IPath; +import org.eclipse.core.runtime.IStatus; import org.eclipse.jface.action.IAction; import org.eclipse.jface.viewers.ISelection; import org.eclipse.jface.viewers.IStructuredSelection; @@ -92,10 +93,9 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler { Logger.info(stringBuffer.toString()); LimitedLogger.getLogger().log(stringBuffer.toString(),rootElement.getElementName(), null); } else if (realError) - Logger.notifyUserWithoutBugreport(stringBuffer.toString()); + Logger.notifyUser(stringBuffer.toString()); else - Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer - .toString()); + Logger.log(IStatus.WARNING, stringBuffer.toString(), null); } else { Animator.getAnimator().resetRodinProjectHasErrorsOrWarnings(); } diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java index c0c52be3bf8551c8a736b964f679c66295289773..2fc868c1599a8642dad1f9c994d2ea5026680c17 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartDistributedModelcheckHandler.java @@ -68,8 +68,7 @@ public class StartDistributedModelcheckHandler extends AbstractHandler implement final IFile resource = extractResource(rootElement); if (!checkErrorMarkers(resource)) { - String message = "A model/context in your project contains Errors or Warnings. This can lead to unexpected behavior (e.g. missing variables) when animating."; - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser("A model/context in your project contains Errors or Warnings. This can lead to unexpected behavior (e.g. missing variables) when animating."); } ; @@ -83,7 +82,7 @@ public class StartDistributedModelcheckHandler extends AbstractHandler implement s = new Socket("localhost", 4444); new ObjectOutputStream(s.getOutputStream()).writeObject(output); } catch (IOException e) { - Logger.notifyUserWithoutBugreport("unable to connect to master", e); + Logger.notifyUser("unable to connect to master", e); } finally { if (s != null) { try { diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java index 0860779f1f4078267f51ca61d5bd48cf6cd19233..78be9b348aa76d005238be8f0dc1671d7f1becfa 100644 --- a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java +++ b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingDialog.java @@ -14,6 +14,7 @@ import java.io.FileReader; import java.io.IOException; import java.io.ObjectInputStream; import java.io.ObjectOutputStream; +import java.nio.file.NoSuchFileException; import java.util.ArrayList; import java.util.Arrays; import java.util.HashSet; @@ -405,7 +406,7 @@ public final class LtlCheckingDialog extends TrayDialog { formulas.select(0); close(); - } catch (FileNotFoundException e) { + } catch (FileNotFoundException | NoSuchFileException e) { Logger.notifyUser("File not found", e); } catch (IOException e) { Logger.notifyUser("Unexpected IO exception", e); diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java index 4bef5235041480ed300081c61d6b055ce1a6e62f..d3b1b1da953961dc0bc1e190147932c9fd00cbd9 100644 --- a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java +++ b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingFinishedListener.java @@ -34,9 +34,7 @@ public class LtlCheckingFinishedListener extends JobChangeAdapter { showResult(ltlJob.getModelCheckingResult()); } } else { - final String message = "The job has a wrong type. Expected LtlCheckingJob but got " - + job.getClass(); - Logger.notifyUserWithoutBugreport(message); + Logger.notifyUser("The job has a wrong type. Expected LtlCheckingJob but got " + job.getClass()); } } diff --git a/de.prob.ui/src/de/prob/ui/ticket/LogView.java b/de.prob.ui/src/de/prob/ui/ticket/LogView.java deleted file mode 100644 index dd46ac764ed84884f284153e754aaa7fdba6e796..0000000000000000000000000000000000000000 --- a/de.prob.ui/src/de/prob/ui/ticket/LogView.java +++ /dev/null @@ -1,42 +0,0 @@ -/** - * (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.ui.ticket; - -import org.eclipse.swt.SWT; -import org.eclipse.swt.widgets.Composite; -import org.eclipse.swt.widgets.Text; -import org.eclipse.ui.part.ViewPart; - -public class LogView extends ViewPart { - - private static LogView instance = new LogView(); - private Text text; - - @Override - public void createPartControl(final Composite parent) { - text = new Text(parent, SWT.WRAP | SWT.MULTI); - } - - public static void writeToLog(final String s) { - if (instance != null) { - instance.write(s); - } - } - - private synchronized void write(final String s) { - if (text != null) { - text.append(s); - text.append("\n"); - } - } - - @Override - public void setFocus() { - - } - -} diff --git a/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java b/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java index f11341d1073f334b83ecbed3f1472fe3fc6d91d0..44f5b4828d0af10d29b9efc06c096e001bcfc4ca 100644 --- a/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java +++ b/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java @@ -11,8 +11,6 @@ import org.eclipse.core.runtime.IStatus; import org.eclipse.jface.dialogs.ErrorDialog; import org.eclipse.swt.widgets.Display; -import de.prob.logging.Logger; - public final class ProBLogListener implements ILogListener { private static final Display display = Display.getDefault(); @@ -25,9 +23,7 @@ public final class ProBLogListener implements ILogListener { return; } - final int code = status.getCode(); - - if (code == Logger.BUGREPORT || code == Logger.NOBUGREPORT) { + if (status.getSeverity() == IStatus.ERROR || status.getSeverity() == IStatus.WARNING) { display.asyncExec(new Runnable() { public void run() { String title = (status.getSeverity() == IStatus.ERROR) ? "An Error occured" @@ -37,12 +33,5 @@ public final class ProBLogListener implements ILogListener { } }); } - - display.asyncExec(new Runnable() { - public void run() { - LogView.writeToLog(status.getMessage()); - } - }); - } } diff --git a/de.prob2.disprover.feature/feature.xml b/de.prob2.disprover.feature/feature.xml index 54cfc58b0b926d9309ab211ee76b20497f11dadb..8a0cd587dde486b7e0de63cd17c218df9add17b6 100644 --- a/de.prob2.disprover.feature/feature.xml +++ b/de.prob2.disprover.feature/feature.xml @@ -2,7 +2,7 @@ <feature id="de.prob2.disprover.feature" label="ProB for Rodin3 - (Dis)Prover" - version="3.1.0.qualifier" + version="3.1.1.qualifier" provider-name="HHU Düsseldorf STUPS Group"> <description url="http://www.stups.uni-duesseldorf.de/ProB"> @@ -228,9 +228,9 @@ litigation. </license> <requires> - <import plugin="de.prob.core" version="9.5.0" match="equivalent"/> - <import plugin="de.prob.eventb.disprover.core" version="2.1.0" match="equivalent"/> - <import plugin="de.prob.ui" version="7.5.0" match="equivalent"/> + <import plugin="de.prob.core" version="9.5.1" match="equivalent"/> + <import plugin="de.prob.eventb.disprover.core" version="2.1.1" match="equivalent"/> + <import plugin="de.prob.ui" version="7.5.1" match="equivalent"/> <import plugin="org.eclipse.core.runtime" version="3.2.0" match="compatible"/> <import plugin="org.eclipse.osgi" version="3.16.0" match="compatible"/> <import plugin="org.eclipse.ui" version="3.118.0" match="compatible"/> diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml index cc058f0ac5b9e5659abdc9682d4b15bcbc345a6b..fa3195af51a69016099fa03750043d52064a751b 100644 --- a/de.prob2.feature/feature.xml +++ b/de.prob2.feature/feature.xml @@ -2,7 +2,7 @@ <feature id="de.prob2.feature" label="ProB for Rodin3" - version="3.1.0.qualifier" + version="3.1.1.qualifier" provider-name="HHU Düsseldorf STUPS Group"> <description url="http://www.stups.uni-duesseldorf.de/ProB"> @@ -228,9 +228,9 @@ litigation. </license> <requires> - <import plugin="de.bmotionstudio.gef.editor" version="5.6.0" match="equivalent"/> - <import plugin="de.prob.core" version="9.5.0" match="equivalent"/> - <import plugin="de.prob.ui" version="7.5.0" match="equivalent"/> + <import plugin="de.bmotionstudio.gef.editor" version="5.6.1" match="equivalent"/> + <import plugin="de.prob.core" version="9.5.1" match="equivalent"/> + <import plugin="de.prob.ui" version="7.5.1" match="equivalent"/> <import plugin="org.eclipse.core.databinding" version="1.10.0" match="compatible"/> <import plugin="org.eclipse.core.databinding.beans" version="1.7.0" match="compatible"/> <import plugin="org.eclipse.core.expressions" version="3.7.0" match="compatible"/> diff --git a/de.prob2.symbolic.feature/feature.xml b/de.prob2.symbolic.feature/feature.xml index 3ad3119dc5fdd1f19f2bb29630616bd11a1ba6ae..3554d9302de9ccbc1a486428fef698ea495ca1e8 100644 --- a/de.prob2.symbolic.feature/feature.xml +++ b/de.prob2.symbolic.feature/feature.xml @@ -2,7 +2,7 @@ <feature id="de.prob2.symbolic.feature" label="ProB for Rodin3 - Symbolic Constants Support" - version="3.1.0.qualifier" + version="3.1.1.qualifier" provider-name="HHU Düsseldorf STUPS Group"> <description url="http://www.stups.uni-duesseldorf.de/ProB"> diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index c1962a79e29d3e0ab67b14947c167a862655af9b..d64cd4917707c1f8861d8cb53dd15194d4248596 100644 Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 37aef8d3f0c9fffa920a8290320a6c78095e1591..a80b22ce5cffec8b48ee79b11c67945e91f99d5f 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,6 +1,7 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.6-bin.zip networkTimeout=10000 +validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/gradlew b/gradlew index aeb74cbb43e3931a2455a838345c3f6b8131aaa2..1aa94a4269074199e6ed2c37e8db3e0826030965 100755 --- a/gradlew +++ b/gradlew @@ -83,7 +83,8 @@ done # This is normally unused # shellcheck disable=SC2034 APP_BASE_NAME=${0##*/} -APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit +# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036) +APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit # Use the maximum available, or set MAX_FD != -1 to use that value. MAX_FD=maximum @@ -130,10 +131,13 @@ location of your Java installation." fi else JAVACMD=java - which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. + if ! command -v java >/dev/null 2>&1 + then + die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. Please set the JAVA_HOME variable in your environment to match the location of your Java installation." + fi fi # Increase the maximum file descriptors if we can. @@ -141,7 +145,7 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then case $MAX_FD in #( max*) # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 + # shellcheck disable=SC2039,SC3045 MAX_FD=$( ulimit -H -n ) || warn "Could not query maximum file descriptor limit" esac @@ -149,7 +153,7 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then '' | soft) :;; #( *) # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 + # shellcheck disable=SC2039,SC3045 ulimit -n "$MAX_FD" || warn "Could not set maximum file descriptor limit to $MAX_FD" esac @@ -198,11 +202,11 @@ fi # Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' -# Collect all arguments for the java command; -# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of -# shell script including quotes and variable substitutions, so put them in -# double quotes to make sure that they get re-expanded; and -# * put everything else in single quotes, so that it's not re-expanded. +# Collect all arguments for the java command: +# * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments, +# and any embedded shellness will be escaped. +# * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be +# treated as '${Hostname}' itself on the command line. set -- \ "-Dorg.gradle.appname=$APP_BASE_NAME" \ diff --git a/gradlew.bat b/gradlew.bat index 6689b85beecde676054c39c2408085f41e6be6dc..7101f8e4676fcad8adc961e929ea3bcb37b5262f 100644 --- a/gradlew.bat +++ b/gradlew.bat @@ -43,11 +43,11 @@ set JAVA_EXE=java.exe %JAVA_EXE% -version >NUL 2>&1 if %ERRORLEVEL% equ 0 goto execute -echo. -echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. -echo. -echo Please set the JAVA_HOME variable in your environment to match the -echo location of your Java installation. +echo. 1>&2 +echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. 1>&2 +echo. 1>&2 +echo Please set the JAVA_HOME variable in your environment to match the 1>&2 +echo location of your Java installation. 1>&2 goto fail @@ -57,11 +57,11 @@ set JAVA_EXE=%JAVA_HOME%/bin/java.exe if exist "%JAVA_EXE%" goto execute -echo. -echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% -echo. -echo Please set the JAVA_HOME variable in your environment to match the -echo location of your Java installation. +echo. 1>&2 +echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% 1>&2 +echo. 1>&2 +echo Please set the JAVA_HOME variable in your environment to match the 1>&2 +echo location of your Java installation. 1>&2 goto fail diff --git a/tycho_build.gradle b/tycho_build.gradle index 136ec052e42a77e43d64291cf15d12f30010707a..7fabe74f09d017faa8cb5a0d22e0e382f208f3c2 100644 --- a/tycho_build.gradle +++ b/tycho_build.gradle @@ -308,9 +308,6 @@ subprojects { content.eachLine(printFileLine) - println artifactId - println "\t" + versionNumber - def f = new File(workspacePath + artifactId + '/pom.xml') f.delete() @@ -330,9 +327,6 @@ subprojects { versionNumber = parsedXml.attribute("version") versionNumber = versionNumber.replace(".qualifier", "-SNAPSHOT") - println artifactId - println "\t" + versionNumber - def f = new File(workspacePath + artifactId + '/pom.xml') f.delete() f << feature(artifactId, versionNumber) @@ -376,29 +370,7 @@ clean.dependsOn(deleteParent) // define Repository task createRepository() { doLast{ - new File(workspacePath + "${repositoryName}").mkdir() - - String versionNumber = '1.0.0.qualifier' - String artifactId = repositoryName - String featureVersionNumber = '1.0.0.qualifier' - String featureArtifactId - def f = new File(workspacePath + artifactId + '/category.xml') - f.delete() - f << categoryHead() - for (int i = 0; i < features.size(); i++) { - def parsedXml = new XmlParser().parse("${workspacePath}${features[i]}/feature.xml") - - featureVersionNumber = parsedXml.attribute("version") - featureArtifactId = parsedXml.attribute("id") - - f << categoryFeature(categoryId, featureArtifactId.replace(workspacePath, ''), featureVersionNumber) - } - - f << categoryDef(categoryId, categoryLabel, categoryDescription) - - f << categoryEnd() - - def pom = new File(workspacePath + artifactId + '/pom.xml') + def pom = new File(workspacePath + repositoryName + '/pom.xml') pom.delete() pom << reposi() } @@ -573,31 +545,6 @@ def reposi() {"""\ </project> """} -// creates a category in -def categoryHead() {"""\ -<?xml version="1.0" encoding="UTF-8"?> -<site> -"""} - -def categoryFeature(category, artifactId, versionNumber) {""" - <feature url="features/${artifactId}_${versionNumber}.jar" id="${artifactId}" version="${versionNumber}"> - <category name="${category}"/> - </feature> -"""} - -def categoryDef(id, label, categorydescription) {""" - <category-def name="${id}" label="${label}"> - <description> -${categorydescription} - </description> - </category-def> -"""} - -def categoryEnd() {""" -</site> -"""} -// end of category definition - // feature pom def feature(artifactId, versionNumber) {"""\ <?xml version="1.0" encoding="UTF-8"?>