diff --git a/README.md b/README.md index 583826b9cef94faa77f341d9adfa97f44c018eed..a01a8b1eeff5b81bf8c6aecd56bf330f4e9428e0 100644 --- a/README.md +++ b/README.md @@ -13,28 +13,23 @@ The ProB binary and source distributions contain the nauty library (http://cs.an For availability of commercial support, please contact Formal Mind (http://www.formalmind.com). -# Contributing - -## Setting up the development environment +# Setting up the development environment - Clone the repository (http://github.com/bendisposto/prob) We suggest to fork the project on github (see https://help.github.com/articles/fork-a-repo) -- We use gradle to manage the dependencies to the libraries, so you will need gradle installed on your computer. +- We use gradle to manage the dependencies to the libraries, thus you will need gradle installed on your computer. (see http://www.gradle.org/) -- Open a shell and cd into the de.prob.releng directory - -- Run the downloadCli task (gradle downloadCli). This will download the latest nightly build of the Prolog binary. - -- Run the collectDependencies task (gradle collectDependencies). This will download the required libraries (such as apache commons, etc.) +- In the de.prob.releng directory 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 apache commons, etc.) - Install Eclipse (Indigo/Juno) for RCP Development -- Import the projects into Eclipse (note that de.prob.releng is not an Eclipse project, it can be left out). At this point Eclipse will show many errors, the reason is that the Target platform (i.e., Rodin hasn't been setup yet) +- Import the projects into Eclipse. You can leave out de.prob.releng. At this point Eclipse will complain about errors, the reason is that the target platform (i.e., Rodin) hasn't been setup yet). - Open the file prob_target.target from the de.prob.core project and click on "Set as Target Platform". Grab a coffee. +- After the target platform was installed and the workspace has been compiled you can run the project as an Eclipse application (use org.rodinp.platform.product as the product in the run configuration) diff --git a/de.prob.core/build.properties b/de.prob.core/build.properties index e6c247370fcec6bdd5a804d721b2a3627d8c4f25..0a0b45bd564599a42834dd45e0bf74c1ad95c26b 100644 --- a/de.prob.core/build.properties +++ b/de.prob.core/build.properties @@ -4,15 +4,6 @@ bin.includes = META-INF/,\ plugin.xml,\ .,\ prob/,\ - lib/dependencies,\ - lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/bparser-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/commons-lang-2.6.jar,\ - lib/dependencies/jgrapht-0.8.3.jar,\ - lib/dependencies/jsr305-1.3.9.jar,\ - lib/dependencies/ltlparser-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/parserbase-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/prologlib-2.4.8-SNAPSHOT.jar,\ - lib/dependencies/unicode-2.4.8-SNAPSHOT.jar + lib/ + diff --git a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java index c1b4f6e03846aef0b90698396e5d5ba22b941f6c..7094ecabecf5f2ed6abe1799ca4bca63ff594463 100644 --- a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java +++ b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java @@ -8,7 +8,6 @@ package de.prob.eventb.translator; // NOPMD // High number of imports because it depends on AST import java.util.ArrayList; -import java.util.Collections; import java.util.LinkedList; import java.util.List; @@ -26,7 +25,6 @@ import org.eventb.core.ast.RelationalPredicate; import org.eventb.core.ast.SimplePredicate; import org.eventb.core.ast.UnaryPredicate; -import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma; import de.be4.classicalb.core.parser.node.AConjunctPredicate; import de.be4.classicalb.core.parser.node.ADisjunctPredicate; import de.be4.classicalb.core.parser.node.AEqualPredicate; @@ -52,7 +50,6 @@ import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate; import de.be4.classicalb.core.parser.node.ATruthPredicate; import de.be4.classicalb.core.parser.node.PExpression; import de.be4.classicalb.core.parser.node.PPredicate; -import de.hhu.stups.sablecc.patch.SourcePosition; import de.prob.eventb.translator.internal.SimpleVisitorAdapter; public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD diff --git a/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java index f5f0faa9f9fe6f509bf0a85ddaf2b251f6ab6d4e..828469e7652b0f8453cf1c43a1404e66ee8cd8c1 100644 --- a/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator2/EMFEventBTranslator.java @@ -9,7 +9,6 @@ import org.eclipse.emf.common.util.EList; import org.eventb.core.IEventBRoot; import org.eventb.emf.core.EventBNamedCommentedComponentElement; import org.eventb.emf.core.Project; -import org.eventb.emf.core.context.Axiom; import org.eventb.emf.core.context.CarrierSet; import org.eventb.emf.core.context.Context; import org.eventb.emf.core.machine.Machine; @@ -54,10 +53,6 @@ public class EMFEventBTranslator { s.getName()) })); setList.add(deferredSet); } - - EList<Axiom> axioms = c.getAxioms(); - - } diff --git a/de.prob.core/src/de/prob/logging/Logger.java b/de.prob.core/src/de/prob/logging/Logger.java index 8780aa3023a0cd5596b3b27bcbaf5dc30151347c..678c5ddce1eba6f6d1eb83772c35177e8e8b3258 100644 --- a/de.prob.core/src/de/prob/logging/Logger.java +++ b/de.prob.core/src/de/prob/logging/Logger.java @@ -78,7 +78,8 @@ public final class Logger { /** * Check a property. The method notifies the user and throws an exception if * the assertion fails. <br> - * <b>Examples:</b><br>{@code Logger.assertProB(this.getClass(),"x != null", x + * <b>Examples:</b><br> + * {@code Logger.assertProB(this.getClass(),"x != null", x * != null); } <br> * {@code Logger.assertProB(this.getClass(),"x should not be null", x != null); } * <br> @@ -112,7 +113,8 @@ public final class Logger { /** * Failed assertion. The method notifies the user and throws an exception. <br> - * <b>Examples:</b><br>{@code if (!file.exists()) String message = + * <b>Examples:</b><br> + * {@code if (!file.exists()) String message = * "Called open on nonexisting file " + file; * Logger.assertProB(EditorPlugin.class, message); } * @@ -149,4 +151,8 @@ 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.ui/src/de/prob/ui/eventb/StartAnimationHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java index 3635bc29a0290ab49569005982bd1e4a98fb5532..bad71c487cf3bcc693af280eae6889e452261296 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java @@ -1,5 +1,8 @@ package de.prob.ui.eventb; +import java.util.ArrayList; +import java.util.List; + import org.eclipse.core.commands.AbstractHandler; import org.eclipse.core.commands.ExecutionEvent; import org.eclipse.core.commands.ExecutionException; @@ -67,9 +70,22 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler { final IEventBRoot rootElement = getRootElement(); 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); + ArrayList<String> errors = new ArrayList<String>(); + boolean realError = checkErrorMarkers(resource, errors); + if (!errors.isEmpty()) { + String message = "Some components in your project contain " + + (realError ? "errors" : "warnings") + + ". This can lead to unexpected behavior (e.g. missing variables) when animating.\n\nDetails:\n"; + StringBuffer stringBuffer = new StringBuffer(message); + for (String string : errors) { + stringBuffer.append(string); + stringBuffer.append('\n'); + } + if (realError) + Logger.notifyUserWithoutBugreport(stringBuffer.toString()); + else + Logger.notifyUserAboutWarningWithoutBugreport(stringBuffer + .toString()); } ; @@ -90,17 +106,25 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler { return null; } - private boolean checkErrorMarkers(final IFile resource) { + private boolean checkErrorMarkers(final IFile resource, List<String> errors) { + boolean result = false; IProject project = resource.getProject(); try { IMarker[] markers = project.findMarkers( "org.eclipse.core.resources.problemmarker", true, IResource.DEPTH_INFINITE); - return markers.length == 0; - } catch (CoreException e1) { + for (IMarker iMarker : markers) { + errors.add(iMarker.getResource().getName() + + ": " + + iMarker + .getAttribute(IMarker.MESSAGE, "unknown Error")); + result = result + || (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR; + } + } catch (CoreException e1) { } - return false; + return result; } private IEventBRoot getRootElement() { 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 41ba4f1f7cf648711e488fb4ce5753993982ecc5..c877085a3805a0b4dc296afb623a1d92db468a9d 100644 --- a/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java +++ b/de.prob.ui/src/de/prob/ui/ticket/ProBLogListener.java @@ -27,15 +27,16 @@ public final class ProBLogListener implements ILogListener { final int code = status.getCode(); if (code == Logger.BUGREPORT || code == Logger.NOBUGREPORT) { - final boolean bugreport = false; //;code == Logger.BUGREPORT; + final boolean bugreport = false; // ;code == Logger.BUGREPORT; display.asyncExec(new Runnable() { public void run() { + String title = (status.getSeverity() == IStatus.ERROR) ? "An Error occured" + : "Warning"; // Notice: ErrorTICKETDialog to provide Bugreport-Button ErrorTicketDialog.openError(display.getActiveShell(), - "Error", "An error occured.", status, bugreport); + "ProB Problem", title, status, bugreport); } - } - ); + }); } display.asyncExec(new Runnable() {