diff --git a/build.gradle b/build.gradle
index f18a8db85b7f7441e9cdcf1e06c6746a8eaf86a0..2b8fbd8a64a364922cd43b8eb13fa7755ec14d2e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -2,7 +2,7 @@
import org.apache.tools.ant.taskdefs.condition.Os
project.ext{
-
+
targetRepositories = ["http://download.eclipse.org/releases/indigo/",
"http://rodin-b-sharp.sourceforge.net/updates",
"http://rodin-b-sharp.sourceforge.net/core-updates"
@@ -18,7 +18,7 @@ apply from: 'tycho_build.gradle'
task bMotionStudioHelpCustumBuild(type: Exec){
-
+
commandLine 'ant', '-f','de.bmotionstudio.help/customBuild.xml'
}
@@ -36,7 +36,7 @@ project(':de.prob.core') {
}
- def parser_version = '2.4.28-SNAPSHOT'
+ def parser_version = '2.4.33-SNAPSHOT'
dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
@@ -49,7 +49,7 @@ project(':de.prob.core') {
compile group: "de.prob", name: "theorymapping", version: parser_version , changing: true
compile 'commons-lang:commons-lang:2.6'
}
-
+
}
project(':de.prob.ui') {
@@ -75,11 +75,11 @@ def download(address,target) {
task downloadCli << {
def dir = workspacePath+'de.prob.core/prob/'
delete file(dir)
- new File(dir).mkdirs()
-
+ new File(dir).mkdirs()
+
['leopard64':'macos','linux32':'linux','linux64':'linux64','win32':'windows'].each {
def n = it.getKey()
-
+
def targetdir = dir+it.getValue()
def targetzip = dir+"probcli_${n}.zip"
def url = "http://nightly.cobra.cs.uni-duesseldorf.de/cli/probcli_${n}.zip"
@@ -101,20 +101,20 @@ task downloadCli << {
into targetdir
}
delete file(targetzip)
-
+
}
task downloadCli2 ( type: Exec ) {
-
+
def dir = workspacePath+'de.prob.core/prob/'
delete file(dir)
- new File(dir).mkdirs()
-
+ new File(dir).mkdirs()
+
['leopard64':'macos','linux32':'linux','linux64':'linux64','win32':'windows'].each {
def n = it.getKey()
-
+
def targetdir = dir+it.getValue()
def targetzip = dir+"probcli_${n}.zip"
def url = "http://nightly.cobra.cs.uni-duesseldorf.de/cli/probcli_${n}.zip"
@@ -136,17 +136,17 @@ task downloadCli2 ( type: Exec ) {
into targetdir
}
delete file(targetzip)
-
+
['leopard64':'macos','linux32':'linux','linux64':'linux64'].each {
-
+
def n = it.getKey()
targetdir = dir+it.getValue()
download( "http://nightly.cobra.cs.uni-duesseldorf.de/cspm/cspm-"+n, targetdir+"/cspm" )
}
- commandLine 'chmod', 'a+x', dir+'linux'+'/cspm', dir+'linux64'+'/cspm', dir+'macos'+'/cspm'
- //commandLine 'chmod', 'a+x', dir+'*'+'/cspm'
-
+ commandLine 'chmod', 'a+x', dir+'linux'+'/cspm', dir+'linux64'+'/cspm', dir+'macos'+'/cspm'
+ //commandLine 'chmod', 'a+x', dir+'*'+'/cspm'
+
download( "http://nightly.cobra.cs.uni-duesseldorf.de/cspm/cspm-windows", dir+"windows"+"/cspm.exe" )
}
@@ -166,4 +166,3 @@ task collectArtifacts(type:Copy) {
from workspacePath + "index.html"
into workspacePath + 'updatesite'
}
-
diff --git a/de.bmotionstudio.rodin/src/de/bmotionstudio/rodin/StartEventBVisualizationHandler.java b/de.bmotionstudio.rodin/src/de/bmotionstudio/rodin/StartEventBVisualizationHandler.java
index 7d0799c38ad624891800d6b6cf41c0e6b64877d7..73fdccadfa2dac75a95554de9becd38b45f02744 100644
--- a/de.bmotionstudio.rodin/src/de/bmotionstudio/rodin/StartEventBVisualizationHandler.java
+++ b/de.bmotionstudio.rodin/src/de/bmotionstudio/rodin/StartEventBVisualizationHandler.java
@@ -1,40 +1,40 @@
-/**
- * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
- * Heinrich Heine Universitaet Duesseldorf
- * This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
- * */
-
-package de.bmotionstudio.rodin;
-
-import org.eclipse.core.commands.IHandler;
-import org.eclipse.core.resources.IFile;
-import org.eclipse.core.resources.IResource;
-import org.eclipse.core.resources.IWorkspace;
-import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.core.runtime.IPath;
-import org.eclipse.core.runtime.Path;
-import org.eclipse.jface.viewers.IStructuredSelection;
-
-import de.bmotionstudio.gef.editor.handler.StartVisualizationFileHandler;
-
-/**
- * @author Lukas Ladenberger
- *
- */
-public class StartEventBVisualizationHandler extends
- StartVisualizationFileHandler implements IHandler {
-
- @Override
- protected IFile getBmsFileFromSelection(IStructuredSelection ssel) {
- if (ssel.getFirstElement() instanceof BMotionStudioRodinFile) {
- IResource resource = ((BMotionStudioRodinFile) ssel
- .getFirstElement()).getResource();
- IWorkspace workspace = ResourcesPlugin.getWorkspace();
- IPath location = Path.fromOSString(resource.getFullPath()
- .toOSString());
- return workspace.getRoot().getFileForLocation(location);
- }
- return null;
- }
-
-}
+/**
+ * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
+ * Heinrich Heine Universitaet Duesseldorf
+ * This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
+ * */
+
+package de.bmotionstudio.rodin;
+
+import org.eclipse.core.commands.IHandler;
+import org.eclipse.core.resources.IFile;
+import org.eclipse.core.resources.IResource;
+import org.eclipse.core.resources.IWorkspace;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.core.runtime.IPath;
+import org.eclipse.core.runtime.Path;
+import org.eclipse.jface.viewers.IStructuredSelection;
+
+import de.bmotionstudio.gef.editor.handler.StartVisualizationFileHandler;
+
+/**
+ * @author Lukas Ladenberger
+ *
+ */
+public class StartEventBVisualizationHandler extends
+ StartVisualizationFileHandler implements IHandler {
+
+ @Override
+ protected IFile getBmsFileFromSelection(IStructuredSelection ssel) {
+ if (ssel.getFirstElement() instanceof BMotionStudioRodinFile) {
+ IResource resource = ((BMotionStudioRodinFile) ssel
+ .getFirstElement()).getResource();
+ IWorkspace workspace = ResourcesPlugin.getWorkspace();
+ IPath location = Path.fromOSString(resource.getFullPath()
+ .toOSString());
+ return workspace.getRoot().getFile(location);
+ }
+ return null;
+ }
+
+}
diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index 6037143e852ed9a2db70bc105172263b8d4bde55..2d8492b577e13616723ba613cfad88688ed06063 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -4,20 +4,20 @@
<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.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.26-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.35-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jfmi-1.0.2-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jna-3.4.0.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.4.26-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.26-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.4.35-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.35-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.7.jar"/>
</classpath>
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 448ac968741ca08c110cd38087eb0df2906061d5..aaeb82bff53ac70e5c9bffdc9983531454dc95b1 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -2,10 +2,10 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Animator Core
Bundle-SymbolicName: de.prob.core;singleton:=true
-Bundle-Version: 9.4.1.qualifier
+Bundle-Version: 9.4.3.qualifier
Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
org.rodinp.core;bundle-version="[1.7.0,1.8.0)",
- org.eventb.theory.core;bundle-version="[2.0.0,3.0.0)";resolution:=optional,
+ org.eventb.theory.core;bundle-version="[3.0.0,3.1.0)";resolution:=optional,
org.eventb.core.ast;bundle-version="[3.0.0,3.2.0)",
org.eclipse.core.resources;bundle-version="[3.5.0,4.0.0)",
org.eventb.core.seqprover;bundle-version="[3.0.0,3.2.0)",
@@ -122,28 +122,19 @@ Bundle-Activator: de.prob.core.internal.Activator
Eclipse-BuddyPolicy: registered
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ClassPath: .,
- lib/dependencies/unicode-2.4.26-SNAPSHOT.jar,
- lib/dependencies/theorymapping-2.4.26-SNAPSHOT.jar,
- lib/dependencies/prologlib-2.4.26-SNAPSHOT.jar,
- lib/dependencies/parserbase-2.4.26-SNAPSHOT.jar,
- lib/dependencies/ltlparser-2.4.26-SNAPSHOT.jar,
- lib/dependencies/cliparser-2.4.26-SNAPSHOT.jar,
- lib/dependencies/bparser-2.4.26-SNAPSHOT.jar,
- lib/dependencies/answerparser-2.4.26-SNAPSHOT.jar,
- lib/dependencies/unicode-2.4.22-SNAPSHOT.jar,
- lib/dependencies/theorymapping-2.4.22-SNAPSHOT.jar,
- lib/dependencies/prologlib-2.4.22-SNAPSHOT.jar,
- lib/dependencies/parserbase-2.4.22-SNAPSHOT.jar,
- lib/dependencies/ltlparser-2.4.22-SNAPSHOT.jar,
- lib/dependencies/cliparser-2.4.22-SNAPSHOT.jar,
- lib/dependencies/bparser-2.4.22-SNAPSHOT.jar,
- lib/dependencies/answerparser-2.4.22-SNAPSHOT.jar,
- lib/dependencies/jgrapht-0.8.3.jar,
+ lib/dependencies/unicode-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/theorymapping-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/prologlib-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/parserbase-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/ltlparser-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/cliparser-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/bparser-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/answerparser-2.4.35-SNAPSHOT.jar,
+ lib/dependencies/xstream-1.4.7.jar,
lib/dependencies/commons-codec-1.6.jar,
lib/dependencies/commons-lang-2.6.jar,
lib/dependencies/jsr305-1.3.9.jar,
lib/dependencies/xmlpull-1.1.3.1.jar,
lib/dependencies/xpp3_min-1.1.4c.jar,
- lib/dependencies/xstream-1.4.3.jar,
lib/dependencies/jfmi-1.0.2-SNAPSHOT.jar,
lib/dependencies/jna-3.4.0.jar
diff --git a/de.prob.core/build.gradle b/de.prob.core/build.gradle
index 60dd16f13dc3acdbf16941f1423292a2600a4663..364ac58838c3736c60c6224ea0722075d9d82f0a 100644
--- a/de.prob.core/build.gradle
+++ b/de.prob.core/build.gradle
@@ -1,6 +1,6 @@
apply plugin: 'java'
-def parser_version = '2.4.18-SNAPSHOT'
+def parser_version = '2.4.35-SNAPSHOT'
dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
@@ -13,7 +13,7 @@ dependencies {
compile group: "de.prob", name: "theorymapping", version: parser_version , changing: true
compile 'commons-lang:commons-lang:2.6'
compile 'commons-codec:commons-codec:1.6'
- compile 'com.thoughtworks.xstream:xstream:1.4.3'
+ compile 'com.thoughtworks.xstream:xstream:1.4.7'
compile group: 'net.java.dev.jna', name: 'jna', version: '3.4.0'
compile group: 'edu.berkeley.eecs.ptolemy', name: 'jfmi', version: '1.0.2-SNAPSHOT'
-}
\ No newline at end of file
+}
diff --git a/de.prob.core/build.properties b/de.prob.core/build.properties
index 99230d528427c77989fe9534724cf6533e521d2e..04b12c31027b62018da3c6e00c1c118328e8de94 100644
--- a/de.prob.core/build.properties
+++ b/de.prob.core/build.properties
@@ -8,7 +8,6 @@ bin.includes = META-INF/,\
lib/dependencies/commons-codec-1.6.jar,\
lib/dependencies/xmlpull-1.1.3.1.jar,\
lib/dependencies/xpp3_min-1.1.4c.jar,\
- lib/dependencies/xstream-1.4.3.jar,\
lib/dependencies/jfmi-1.0.2-SNAPSHOT.jar,\
lib/dependencies/jna-3.4.0.jar
diff --git a/de.prob.core/prob_target.target b/de.prob.core/prob_target.target
index 1d4ccde825dd2d9e8fc8956b8f5dc20e67ff458a..9b6eee4fa416c5d277c5cfb08020b490a9e6e069 100644
--- a/de.prob.core/prob_target.target
+++ b/de.prob.core/prob_target.target
@@ -1,21 +1,22 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<?pde version="3.8"?><target name="prob_target" sequenceNumber="32">
+<?pde version="3.8"?><target name="prob_target" sequenceNumber="39">
<locations>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
-<unit id="org.eclipse.gef" version="0.0.0"/>
-<repository location="http://download.eclipse.org/tools/gef/updates/releases"/>
+<unit id="org.eventb.ide.feature.group" version="3.1.0.201412171041-e1a03f3"/>
+<unit id="fr.systerel.editor.feature.group" version="0.8.0.201412171041-e1a03f3"/>
+<unit id="org.rodinp.feature.group" version="1.7.0.201412171041-e1a03f3"/>
+<unit id="org.rodinp.platform.feature.group" version="3.1.0.201412171041-e1a03f3"/>
+<unit id="org.rodinp.platform.sources.feature.group" version="3.1.0.201412171041-e1a03f3"/>
+<unit id="org.rodinp.platform.tests.feature.group" version="3.1.0.201412171041-e1a03f3"/>
+<repository location="http://www.stups.uni-duesseldorf.de/ProB/buildlibs/rodin/"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
+<unit id="org.eventb.theory.feature.feature.group" version="3.0.0"/>
<repository location="http://rodin-b-sharp.sourceforge.net/updates/"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
-<unit id="org.eventb.ide.feature.group" version="3.0.1.201406111447-5326174"/>
-<unit id="fr.systerel.editor.feature.group" version="0.7.0.201406111447-5326174"/>
-<unit id="org.rodinp.feature.group" version="1.7.0.201406111447-5326174"/>
-<unit id="org.rodinp.platform.feature.group" version="3.0.0.201406111447-5326174"/>
-<unit id="org.rodinp.platform.tests.feature.group" version="3.0.0.201406111447-5326174"/>
-<unit id="org.rodinp.platform.sources.feature.group" version="3.0.0.201406111447-5326174"/>
-<repository location="http://www.stups.uni-duesseldorf.de/ProB/buildlibs/rodin/"/>
+<unit id="org.eclipse.gef.sdk.feature.group" version="3.9.101.201408150207"/>
+<repository location="http://download.eclipse.org/releases/luna"/>
</location>
</locations>
</target>
diff --git a/de.prob.core/src/de/prob/core/Animator.java b/de.prob.core/src/de/prob/core/Animator.java
index e78a5611b36a4821ca7e01fd01fdc0075bfba21c..b147a8df738c304b71ccb83b5ed0a944bffa8a74 100644
--- a/de.prob.core/src/de/prob/core/Animator.java
+++ b/de.prob.core/src/de/prob/core/Animator.java
@@ -39,6 +39,7 @@ import de.prob.exceptions.ProBException;
public final class Animator {
private static Animator animator = new Animator();
+ private static Animator auxanimator = null;
/**
*
@@ -66,6 +67,14 @@ public final class Animator {
return animator;
}
+ public final static Animator getAuxAnimator() {
+ if (auxanimator == null) {
+ auxanimator = new Animator();
+ }
+ return auxanimator;
+ }
+
+
/**
* Terminates the current animation (forcefully!) and restarts the ProB
* core. After calling this method, all information from the current
diff --git a/de.prob.core/src/de/prob/core/command/ConstructTraceCommand.java b/de.prob.core/src/de/prob/core/command/ConstructTraceCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..a12b0d913e8e0e1a8c92c6bddd407527defa97e5
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/ConstructTraceCommand.java
@@ -0,0 +1,196 @@
+/**
+ * (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.command;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
+
+import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
+import de.be4.classicalb.core.parser.exceptions.BException;
+import de.prob.core.Animator;
+import de.prob.core.domainobjects.Operation;
+import de.prob.core.domainobjects.State;
+import de.prob.core.domainobjects.StateError;
+import de.prob.core.domainobjects.Variable;
+import de.prob.core.domainobjects.eval.PredicateEvalElement;
+import de.prob.core.internal.Activator;
+import de.prob.exceptions.ProBException;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.CompoundPrologTerm;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+/**
+ * Command to execute an event that has not been enumerated by ProB.
+ *
+ * @author Jens Bendisposto
+ *
+ */
+public final class ConstructTraceCommand implements IComposableCommand {
+
+ private static final String RESULT_VARIABLE_STATES = "States";
+ private static final String RESULT_VARIABLE_OPS = "Ops";
+ private static final String RESULT_VARIABLE_ERRORS = "Errors";
+
+ private final List<PredicateEvalElement> evalElement;
+ private final List<String> name;
+ private final List<String> errors = new ArrayList<String>();
+ private List<Integer> executionNumber = new ArrayList<Integer>();
+
+ public ConstructTraceCommand(final List<String> name,
+ final List<String> predicates, Integer executionNumber) {
+ this.name = name;
+ this.evalElement = new ArrayList<PredicateEvalElement>();
+ for (String string : predicates) {
+ try {
+ evalElement.add(PredicateEvalElement.create(string));
+ } catch (BException e) {
+ throw new IllegalArgumentException(
+ "Formula must be a predicate: " + string);
+ }
+ }
+ if (name.size() != evalElement.size()) {
+ throw new IllegalArgumentException(
+ "Must provide the same number of names and predicates.");
+ }
+ int size = this.name.size();
+ for (int i = 0; i < size; ++i) {
+ this.executionNumber.add(executionNumber);
+ }
+ }
+
+ public ConstructTraceCommand(final List<String> name,
+ final List<String> predicate) {
+ this(name, predicate, 1);
+ }
+
+ public ConstructTraceCommand(final List<String> name,
+ final List<String> predicate, final List<Integer> executionNumber) {
+ this(name, predicate);
+ this.executionNumber = executionNumber;
+ if (name.size() != executionNumber.size()) {
+ throw new IllegalArgumentException(
+ "Must provide the same number of names and execution numbers.");
+ }
+ }
+
+ /**
+ * This method is called when the command is prepared for sending. The
+ * method is called by the Animator class, most likely it is not interesting
+ * for other classes.
+ *
+ * @throws ProBException
+ *
+ * @see de.prob.animator.command.AbstractCommand#writeCommand(de.prob.prolog.output.IPrologTermOutput)
+ */
+ @Override
+ public void writeCommand(final IPrologTermOutput pto) {
+ pto.openTerm("prob_construct_trace");
+ pto.openList();
+ for (String n : name) {
+ pto.printAtom(n);
+ }
+ pto.closeList();
+ final ASTProlog prolog = new ASTProlog(pto, null);
+ pto.openList();
+ for (PredicateEvalElement cb : evalElement) {
+ cb.getPrologAst().apply(prolog);
+ }
+ pto.closeList();
+ pto.openList();
+ for (Integer n : executionNumber) {
+ pto.printNumber(n);
+ }
+ pto.closeList();
+ pto.printVariable(RESULT_VARIABLE_STATES);
+ pto.printVariable(RESULT_VARIABLE_OPS);
+ pto.printVariable(RESULT_VARIABLE_ERRORS);
+ pto.closeTerm();
+ }
+
+ public boolean hasErrors() {
+ return !errors.isEmpty();
+ }
+
+ public List<String> getErrors() {
+ return errors;
+ }
+
+ @Override
+ public void processResult(
+ final ISimplifiedROMap<String, PrologTerm> bindings)
+ throws CommandException {
+ // errors
+ ListPrologTerm list = (ListPrologTerm) bindings
+ .get(RESULT_VARIABLE_ERRORS);
+ for (PrologTerm prologTerm : list) {
+ errors.add(prologTerm.toString());
+ }
+
+ // Change history in Animator ...
+ // need to reconstruct operations and states
+ final Animator animator = Animator.getAnimator();
+
+ ListPrologTerm operations = (ListPrologTerm) bindings
+ .get(RESULT_VARIABLE_OPS);
+ ListPrologTerm states = (ListPrologTerm) bindings
+ .get(RESULT_VARIABLE_STATES);
+
+ for (int i = 0; i < operations.size(); i++) {
+ PrologTerm operationPrologTerm = operations.get(i);
+ Operation op = Operation.fromPrologTerm(operationPrologTerm);
+
+ // state(NewStateId,StateValues,Initialised,InvKO,MaxOpsReached,Timeout,OpTimeout,StateErrors,UnsatProps,OperationsForState)
+ CompoundPrologTerm statePrologTerm = (CompoundPrologTerm) states
+ .get(i);
+
+ ListPrologTerm stateValuesPrologTerm = (ListPrologTerm) statePrologTerm
+ .getArgument(2);
+ List<Variable> stateValues = new LinkedList<Variable>();
+ for (PrologTerm prologTerm : stateValuesPrologTerm) {
+ stateValues.add(new Variable((CompoundPrologTerm) prologTerm));
+ }
+
+ ListPrologTerm stateErrorsPrologTerm = (ListPrologTerm) statePrologTerm
+ .getArgument(8);
+ Collection<StateError> stateErrors = new LinkedList<StateError>();
+ for (PrologTerm prologTerm : stateErrorsPrologTerm) {
+ stateErrors
+ .add(new StateError((CompoundPrologTerm) prologTerm));
+ }
+
+ Set<String> opTimeouts = new HashSet<String>(
+ PrologTerm.atomicStrings((ListPrologTerm) statePrologTerm
+ .getArgument(7)));
+
+ ArrayList<Operation> enabledOperations = new ArrayList<Operation>();
+
+ for (PrologTerm enop : (ListPrologTerm) statePrologTerm
+ .getArgument(10)) {
+ final CompoundPrologTerm cpt = (CompoundPrologTerm) enop;
+ enabledOperations.add(Operation.fromPrologTerm(cpt));
+ }
+
+ State s = new State(statePrologTerm.getArgument(1).toString(),
+ statePrologTerm.getArgument(2).toString().equals("true"),
+ statePrologTerm.getArgument(3).toString().equals("true"),
+ statePrologTerm.getArgument(5).toString().equals("true"),
+ statePrologTerm.getArgument(4).toString().equals("true"),
+ stateValues, enabledOperations, stateErrors, opTimeouts);
+
+ Activator.computedState(s);
+ animator.getHistory().add(s, op);
+ animator.announceCurrentStateChanged(s, op);
+ }
+
+ }
+}
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 30af5f46ecbb2d1e8f9edb2ba904a18f628d5d9a..98f0b1e5a27112cbd10cc5a02acf5c297e31823c 100644
--- a/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ExploreStateCommand.java
@@ -6,10 +6,16 @@
package de.prob.core.command;
-import java.util.*;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
import de.prob.core.Animator;
-import de.prob.core.domainobjects.*;
+import de.prob.core.domainobjects.Operation;
+import de.prob.core.domainobjects.State;
+import de.prob.core.domainobjects.StateError;
+import de.prob.core.domainobjects.Variable;
import de.prob.core.internal.Activator;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
@@ -80,10 +86,8 @@ public final class ExploreStateCommand implements IComposableCommand {
// only show error message on SETUP_CONSTANTS and
// PARTIALLY_SETUP_CONSTANTS
- if (enabledOperations.size() == 1
- && enabledOperations.get(0).getName().toLowerCase()
- .contains("constants") && unsatPropertiesExist) {
- Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties:\n\n"
+ if (unsatPropertiesExist) {
+ Logger.notifyUserWithoutBugreport("ProB could not find valid constants wich satisfy the properties.\n"
+ unsatPropsCommand.getUnsatPropertiesDescription());
} else if (!initialised && enabledOperations.isEmpty()
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 4c6990ac9afe0e480e24aa903e20273b343107c3..4c45e0f2ae892af17a5740468fe492d9a6511de1 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
@@ -51,10 +51,11 @@ public class CounterExample {
.asList(modelCheckingResult.getInitPathOps()));
ceSize = modelCheckingResult.getCounterexample().size();
+ final String[] atomicFormulaNames = createAtomicNames(modelCheckingResult);
+
final List<ArrayList<Boolean>> predicateValues = createStates(modelCheckingResult
- .getCounterexample());
+ .getCounterexample(), atomicFormulaNames);
- final String[] atomicFormulaNames = createAtomicNames(modelCheckingResult);
propositionRoot = createExample(modelCheckingResult.getStructure(),
atomicFormulaNames, predicateValues);
propositionRoot.setVisible(true);
@@ -73,10 +74,17 @@ public class CounterExample {
return res;
}
- private List<ArrayList<Boolean>> createStates(final ListPrologTerm example) {
+ private List<ArrayList<Boolean>> createStates(final ListPrologTerm example, String[] atomicFormulaNames) {
List<ArrayList<Boolean>> predicateValues = new ArrayList<ArrayList<Boolean>>();
- for (int i = 0; i < example.size(); i++) {
+ // A bug fix from 31.10.2014: changed the termination condition from
+ // 'i < example.size()' to 'i < atomicFormulaNames.length'. The statement
+ // predicateValues.get(i).add(value == 0 ? false : true) in the inner for-loop (lines 98-105)
+ // crashed once the reported counter-example 'example' had less atoms as atomic propositions,
+ // e.g. for 'G ({x/=1} & {y<=10})' with 'example = [atom(0,[0,1],none)]' an IndexOutOfBounds-Exception
+ // had been thrown. Note that the bug-fix has been not thoroughly tested and there may be other issues
+ // that may occur.
+ for (int i = 0; i < atomicFormulaNames.length; i++) {
predicateValues.add(new ArrayList<Boolean>());
}
@@ -92,12 +100,15 @@ public class CounterExample {
for (int i = 0; i < values.size(); i++) {
int value = ((IntegerPrologTerm) values.get(i)).getValue()
.intValue();
- predicateValues.get(i).add(value == 0 ? false : true);
+ // 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);
+ predicateValues.get(i).add(value == 0 ? false : true);
}
final Operation operation = NONE.equals(operationTerm) ? null
: Operation.fromPrologTerm(operationTerm);
- final CounterExampleState ceState = new CounterExampleState(index,
+ final CounterExampleState ceState = new CounterExampleState(index,
stateId, operation);
states.add(ceState);
index++;
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 cede1459aa58b4d634ddc9deec9f54ded5ac49cb..15d6ace44a758cc4e5b5867a332973747c4fb370 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -407,7 +407,7 @@ public class Theories {
private static void processDefinitions(FormulaFactory ff,
ITypeEnvironment te, IPrologTermOutput prologOutput,
ISCDirectOperatorDefinition[] directOperatorDefinitions)
- throws RodinDBException {
+ throws CoreException {
for (ISCDirectOperatorDefinition def : directOperatorDefinitions) {
Formula<?> scFormula = def.getSCFormula(ff, te);
diff --git a/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF b/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF
index 55ff7ade5f04b2d9eef77e6f8556b4c32bf394a6..8e09a35b7045ed04604c7a0de391377fcae6714f 100644
--- a/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF
+++ b/de.prob.eventb.disprover.core/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ 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: 1.3.2.qualifier
+Bundle-Version: 2.0.5.qualifier
Bundle-Vendor: Heinrich-Heine University Dusseldorf
Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
de.prob.core;bundle-version="[9.4.0,9.5.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 1c7f3f8c8ecf5220c35770faf0e2d09d5a775647..6eaa13155176cc519eb31b21f24953b437741af0 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
@@ -1,17 +1,31 @@
package de.prob.eventb.disprover.core;
-import java.util.*;
+import java.util.HashSet;
+import java.util.Set;
import org.eclipse.core.runtime.Status;
-import org.eventb.core.*;
+import org.eventb.core.IEventBProject;
+import org.eventb.core.IPOSequent;
import org.eventb.core.ast.Predicate;
-import org.eventb.core.seqprover.*;
+import org.eventb.core.seqprover.IConfidence;
+import org.eventb.core.seqprover.IProofMonitor;
+import org.eventb.core.seqprover.IProofRule;
import org.eventb.core.seqprover.IProofRule.IAntecedent;
-import org.rodinp.core.*;
+import org.eventb.core.seqprover.IProverSequent;
+import org.eventb.core.seqprover.IReasoner;
+import org.eventb.core.seqprover.IReasonerInput;
+import org.eventb.core.seqprover.IReasonerInputReader;
+import org.eventb.core.seqprover.IReasonerInputWriter;
+import org.eventb.core.seqprover.IReasonerOutput;
+import org.eventb.core.seqprover.ProverFactory;
+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.*;
+import de.prob.core.Animator;
+import de.prob.core.PrologException;
import de.prob.eventb.disprover.core.internal.DisproverCommand;
import de.prob.eventb.disprover.core.internal.ICounterExample;
import de.prob.eventb.disprover.core.translation.DisproverContextCreator;
@@ -107,13 +121,14 @@ public class DisproverReasoner implements IReasoner {
IEventBProject evbProject = (IEventBProject) project
.getAdapter(IEventBProject.class);
ICounterExample counterExample = DisproverCommand.disprove(
- Animator.getAnimator(), evbProject, allHypotheses,
+ Animator.getAuxAnimator(), evbProject, allHypotheses,
selectedHypotheses, goal, timeoutFactor, context, pm);
// Logger.info("Disprover: Result: " + counterExample.toString());
return counterExample;
}
+ @SuppressWarnings("unused")
private String predicateToProlog(Predicate pred) {
PrologTermStringOutput pto = new PrologTermStringOutput();
TranslationVisitor v = new TranslationVisitor();
@@ -132,8 +147,15 @@ public class DisproverReasoner implements IReasoner {
Predicate goal = sequent.goal();
+ // currently, we assume that all existing hypotheses have been used
+ // TODO: make ProB figure out which ones were actually used
+ Set<Predicate> usedHyps = new HashSet<Predicate>();
+ for (Predicate predicate : sequent.hypIterable()) {
+ usedHyps.add(predicate);
+ }
+
IAntecedent ante = ProverFactory.makeAntecedent(goal);
-
+
if (counterExample == null) {
return ProverFactory.reasonerFailure(this, input,
"ProB: Error occurred.");
@@ -148,7 +170,7 @@ public class DisproverReasoner implements IReasoner {
if (!counterExample.counterExampleFound() && counterExample.isProof()) {
System.out.println(sequent.toString() + ": Proof.");
return ProverFactory.makeProofRule(this, input, sequent.goal(),
- null, IConfidence.DISCHARGED_MAX,
+ usedHyps, IConfidence.DISCHARGED_MAX,
"ProB (no enumeration / all cases checked)");
}
@@ -176,8 +198,8 @@ public class DisproverReasoner implements IReasoner {
}
System.out.println(sequent.toString() + ": Counter-Example found.");
- return ProverFactory.makeProofRule(this, input, null, null,
- IConfidence.PENDING, counterExample.toString(), ante);
+ return ProverFactory.makeProofRule(this, input, sequent.goal(),
+ usedHyps, IConfidence.PENDING, counterExample.toString(), ante);
}
@Override
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
index f2d5d87b2e85eb5be776b3ce573fa8b818cb0a50..8596f053818fcf67b9bc9360990fa697f13d31b8 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
@@ -12,15 +12,23 @@ import org.osgi.service.prefs.Preferences;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
-import de.prob.core.*;
-import de.prob.core.command.*;
+import de.prob.core.Animator;
+import de.prob.core.ProBCommandJob;
+import de.prob.core.command.ClearMachineCommand;
+import de.prob.core.command.CommandException;
+import de.prob.core.command.ComposedCommand;
+import de.prob.core.command.IComposableCommand;
+import de.prob.core.command.SetPreferenceCommand;
+import de.prob.core.command.SetPreferencesCommand;
+import de.prob.core.command.StartAnimationCommand;
import de.prob.eventb.disprover.core.DisproverReasoner;
import de.prob.eventb.disprover.core.command.DisproverLoadCommand;
import de.prob.eventb.translator.internal.TranslationVisitor;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.*;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
/**
* The DisproverCommand takes two sets of ASTs (one for the machine and a list
@@ -109,8 +117,7 @@ public class DisproverCommand implements IComposableCommand {
public void writeCommand(final IPrologTermOutput pto) {
pto.openTerm("cbc_disprove");
- Predicate pred = goal;
- translatePredicate(pto, pred);
+ translatePredicate(pto, goal);
pto.openList();
for (Predicate p : this.allHypotheses) {
translatePredicate(pto, p);
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
index 00a0ed486fb1d86e1da41d85e1599329de85318d..69ec7ed4a45beab25c77f2e88dc18517e79004c9 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverIdentifier.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.List;
import org.eventb.core.ast.Expression;
-import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.Type;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -28,13 +27,10 @@ public class DisproverIdentifier {
private final String name;
private final Type type;
- private final FormulaFactory ff;
private final boolean givenSet;
- public DisproverIdentifier(String name, Type type, boolean givenSet,
- FormulaFactory ff) {
+ public DisproverIdentifier(String name, Type type, boolean givenSet) {
this.givenSet = givenSet;
- this.ff = ff;
this.name = name;
this.type = type;
}
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
index dceaec2b769aff5c1e4da9d0bacca51d47ff313f..12d68b9627987a665522e08558d083d861c64185 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/translation/DisproverContextCreator.java
@@ -1,12 +1,26 @@
package de.prob.eventb.disprover.core.translation;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
-import org.eventb.core.ast.*;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.ITypeEnvironment.IIterator;
+import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IProverSequent;
-import de.be4.classicalb.core.parser.node.*;
+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.AEventBContextParseUnit;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.ASetsContextClause;
+import de.be4.classicalb.core.parser.node.PContextClause;
+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.prob.eventb.disprover.core.internal.DisproverIdentifier;
import de.prob.eventb.translator.internal.TranslationVisitor;
@@ -43,7 +57,7 @@ public class DisproverContextCreator {
DisproverIdentifier id = new DisproverIdentifier(
typeIterator.getName(), typeIterator.getType(),
- typeIterator.isGivenSet(), ff);
+ typeIterator.isGivenSet());
// sets are added to the context, vars to the model
if (id.isGivenSet()) {
diff --git a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
index 01f62e3ae5639352456797082f2693b6a3c58ff1..3f936494719280c931789b2777a4d5b7bcda1628 100644
--- a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
+++ b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
@@ -2,18 +2,19 @@ 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.0.3.qualifier
+Bundle-Version: 2.0.5.qualifier
Bundle-Vendor: Heinrich-Heine University Dusseldorf
Require-Bundle: org.eclipse.core.runtime,
- org.eventb.ui;bundle-version="[3.0.0,3.1.0)",
- de.prob.eventb.disprover.core;bundle-version="[1.3.2,2.0.0)",
+ org.eventb.ui;bundle-version="[3.0.0,3.2.0)",
+ de.prob.eventb.disprover.core;bundle-version="[2.0.0,2.1.0)",
org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
de.prob.core,
org.eventb.core.ast;bundle-version="[3.0.0,3.2.0)",
org.eventb.core.seqprover;bundle-version="[3.0.0,3.2.0)",
org.eclipse.osgi,
org.rodinp.core;bundle-version="[1.7.0,1.8.0)",
- org.eventb.core;bundle-version="[3.0.0,3.2.0)"
+ org.eventb.core;bundle-version="[3.0.0,3.2.0)",
+ de.prob.ui;bundle-version="7.4.0"
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy
Bundle-Localization: plugin
diff --git a/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif b/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif
new file mode 100644
index 0000000000000000000000000000000000000000..c6867d469651f80e12a2021e619563e3f2a39b64
Binary files /dev/null and b/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif differ
diff --git a/de.prob.eventb.disprover.ui/plugin.xml b/de.prob.eventb.disprover.ui/plugin.xml
index 7518659c1c1a9942bcb13f5034489f98f82c05c7..9d24e750d23e001f5df639f2575b21f6dc5cef3e 100644
--- a/de.prob.eventb.disprover.ui/plugin.xml
+++ b/de.prob.eventb.disprover.ui/plugin.xml
@@ -72,5 +72,32 @@
name="ProB (Dis-)Prover">
</page>
</extension>
+ <extension
+ point="org.eclipse.ui.commands">
+ <command
+ id="de.prob.eventb.disprover.ui.exportpos"
+ name="Export Proof Obligations for ProB">
+ </command>
+ </extension>
+ <extension
+ point="org.eclipse.ui.handlers">
+ <handler
+ class="de.prob.eventb.disprover.ui.export.ExportPOsHandler"
+ commandId="de.prob.eventb.disprover.ui.exportpos">
+ </handler>
+ </extension>
+ <extension
+ point="org.eclipse.ui.menus">
+ <menuContribution
+ allPopups="false"
+ locationURI="popup:more_commands">
+ <command
+ commandId="de.prob.eventb.disprover.ui.exportpos"
+ icon="icons/prob_mini_logo.gif"
+ label="Export POs for ProB"
+ style="push">
+ </command>
+ </menuContribution>
+ </extension>
</plugin>
diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..01176ac53f0bff8a88529d0643a6b30a091afb95
--- /dev/null
+++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
@@ -0,0 +1,236 @@
+package de.prob.eventb.disprover.ui.export;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.util.Date;
+
+import org.eclipse.core.commands.AbstractHandler;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+import org.eclipse.core.commands.IHandler;
+import org.eclipse.core.runtime.Platform;
+import org.eclipse.core.runtime.preferences.InstanceScope;
+import org.eclipse.jface.dialogs.MessageDialog;
+import org.eclipse.jface.viewers.ISelection;
+import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.widgets.FileDialog;
+import org.eclipse.swt.widgets.Shell;
+import org.eclipse.ui.handlers.HandlerUtil;
+import org.eventb.core.EventBPlugin;
+import org.eventb.core.IContextRoot;
+import org.eventb.core.IEventBRoot;
+import org.eventb.core.IMachineRoot;
+import org.eventb.core.IPORoot;
+import org.eventb.core.IPOSequent;
+import org.eventb.core.IPSRoot;
+import org.eventb.core.IPSStatus;
+import org.eventb.core.ast.Predicate;
+import org.eventb.core.pm.IProofAttempt;
+import org.eventb.core.pm.IProofComponent;
+import org.eventb.core.pm.IProofManager;
+import org.eventb.core.seqprover.IConfidence;
+import org.eventb.core.seqprover.IProofTree;
+import org.eventb.core.seqprover.IProverSequent;
+import org.osgi.service.prefs.BackingStoreException;
+import org.osgi.service.prefs.Preferences;
+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.eventb.disprover.core.translation.DisproverContextCreator;
+import de.prob.eventb.translator.internal.TranslationVisitor;
+import de.prob.logging.Logger;
+import de.prob.prolog.output.PrologTermOutput;
+
+public class ExportPOsHandler extends AbstractHandler implements IHandler {
+
+ @Override
+ public Object execute(final ExecutionEvent event) throws ExecutionException {
+ final IEventBRoot root = getSelectedEventBRoot(event);
+ if (root != null) {
+ final Preferences prefs = Platform.getPreferencesService()
+ .getRootNode().node(InstanceScope.SCOPE)
+ .node("prob_export_preferences");
+ final Shell shell = HandlerUtil.getActiveShell(event);
+ final String fileName = askForExportFile(prefs, shell, root);
+ if (fileName != null) {
+ exportPOs(fileName, root);
+ }
+ }
+ return null;
+ }
+
+ private IEventBRoot getSelectedEventBRoot(final ExecutionEvent event) {
+ final ISelection fSelection = HandlerUtil.getCurrentSelection(event);
+ IEventBRoot root = null;
+ if (fSelection instanceof IStructuredSelection) {
+ final IStructuredSelection ssel = (IStructuredSelection) fSelection;
+ if (ssel.size() == 1
+ && ssel.getFirstElement() instanceof IEventBRoot) {
+ root = (IEventBRoot) ssel.getFirstElement();
+ }
+ }
+ return root;
+ }
+
+ private String askForExportFile(final Preferences prefs, final Shell shell,
+ final IEventBRoot root) {
+ final String path = prefs.get("dir", System.getProperty("user.home"));
+
+ final FileDialog dialog = new FileDialog(shell, SWT.SAVE);
+ dialog.setFilterExtensions(new String[] { "*.pl" });
+
+ dialog.setFilterPath(path);
+ final String subext = (root instanceof IMachineRoot) ? "_mch" : "_ctx";
+ dialog.setFileName(root.getComponentName() + subext + ".pl");
+ String result = dialog.open();
+ if (result != null) {
+ final String newPath = dialog.getFilterPath();
+ if (!path.equals(newPath)) {
+ prefs.put("dir", newPath);
+ try {
+ prefs.flush();
+ } catch (BackingStoreException e) {
+ // Ignore, if preferences are not stored correctly we simply
+ // ignore it (annoying, but not critical)
+ }
+ }
+ if (!result.endsWith(".pl")) {
+ result += ".pl";
+ }
+ }
+ return result;
+ }
+
+ public static void exportPOs(final String filename, final IEventBRoot root) {
+ final boolean isSafeToWrite = isSafeToWrite(filename);
+
+ if (isSafeToWrite) {
+ PrintWriter fw = null;
+ try {
+ fw = new PrintWriter(filename);
+ if (root instanceof IContextRoot) {
+ IContextRoot croot = (IContextRoot) root;
+ IPORoot poRoot = croot.getSCContextRoot().getPORoot();
+ IPSRoot psRoot = croot.getSCContextRoot().getPSRoot();
+ exportPOs(fw, poRoot, psRoot);
+ } else if (root instanceof IMachineRoot) {
+ IMachineRoot croot = (IMachineRoot) root;
+ IPORoot poRoot = croot.getSCMachineRoot().getPORoot();
+ IPSRoot psRoot = croot.getSCMachineRoot().getPSRoot();
+ exportPOs(fw, poRoot, psRoot);
+ } else {
+ throw new IllegalArgumentException(
+ "Not a Context or Machine root.");
+ }
+ fw.append('\n');
+
+ } catch (IllegalArgumentException e) {
+ Logger.notifyUser(e.getMessage());
+ } catch (IOException e) {
+ Logger.notifyUser("Unable to create file '" + filename + "'");
+ } catch (RodinDBException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ } finally {
+ if (fw != null) {
+ fw.close();
+ }
+ }
+ }
+ }
+
+ private static void exportPOs(PrintWriter fw, IPORoot poRoot, IPSRoot psRoot)
+ throws RodinDBException {
+ PrologTermOutput pto = new PrologTermOutput(fw, false);
+ ASTProlog modelAst = new ASTProlog(pto, null);
+ TranslationVisitor tVisitor = new TranslationVisitor();
+
+ Date date = new Date();
+ pto.openTerm("generated");
+ pto.printNumber(date.getTime());
+ pto.printAtom(date.toString());
+ pto.closeTerm();
+ pto.fullstop();
+
+ pto.openTerm("project_name");
+ pto.printAtom(poRoot.getRodinProject().getElementName());
+ pto.closeTerm();
+ pto.fullstop();
+
+ pto.openTerm("machine_name");
+ pto.printAtom(poRoot.getElementName());
+ pto.closeTerm();
+ pto.fullstop();
+
+ IPOSequent[] sequents = poRoot.getSequents();
+ for (IPOSequent ipoSequent : sequents) {
+ IProverSequent proverSequent = toProverSequent(ipoSequent);
+ AEventBContextParseUnit disproverContext = DisproverContextCreator
+ .createDisproverContext(proverSequent);
+
+ // disprover_po(Name,Context,Goal,Hyps,SelectedHyps)
+ pto.openTerm("disprover_po");
+
+ pto.printAtom(ipoSequent.getElementName());
+
+ disproverContext.apply(modelAst);
+
+ proverSequent.goal().accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+
+ pto.openList();
+ for (Predicate hyp : proverSequent.hypIterable()) {
+ hyp.accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+ }
+ pto.closeList();
+
+ pto.openList();
+ for (Predicate hyp : proverSequent.selectedHypIterable()) {
+ hyp.accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+ }
+ pto.closeList();
+
+ // The result: true = proven in rodin, unknown else
+ IPSStatus status = psRoot.getStatus(ipoSequent.getElementName());
+ if (status.getConfidence() == IConfidence.DISCHARGED_MAX) {
+ pto.printAtom("true");
+ } else {
+ pto.printAtom("unknown");
+ }
+
+ pto.closeTerm();
+ pto.fullstop();
+ }
+ }
+
+ public static IProverSequent toProverSequent(IPOSequent sequent)
+ throws RodinDBException {
+ IPORoot poRoot = (IPORoot) sequent.getRoot();
+ IProofManager pm = EventBPlugin.getProofManager();
+ IProofComponent pc = pm.getProofComponent(poRoot);
+ IProofAttempt pa = pc.createProofAttempt(sequent.getElementName(),
+ "ProB PO Export", null);
+
+ IProofTree proofTree = pa.getProofTree();
+
+ IProverSequent proverSequent = proofTree.getSequent();
+ pa.dispose();
+
+ return proverSequent;
+ }
+
+ private static boolean isSafeToWrite(final String filename) {
+ if (new File(filename).exists()) {
+ final MessageDialog dialog = new MessageDialog(null, "File exists",
+ null, "The file exists. Do you want to overwrite it?",
+ MessageDialog.QUESTION, new String[] { "Yes", "No" }, 0);
+ return dialog.open() == 0;
+ } else
+ return true;
+ }
+}
diff --git a/de.prob.plugin/META-INF/MANIFEST.MF b/de.prob.plugin/META-INF/MANIFEST.MF
index 57d4aa60176c7850a354a2f2de3db563ed6e402f..0e6729300d3e168ca78c55c5ef9a151b9883d0fd 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.3.0.qualifier
+Bundle-Version: 2.3.2.qualifier
Fragment-Host: de.prob.ui;bundle-version="[7.4.0,7.5.0)"
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-Vendor: HHU Düsseldorf STUPS Group
diff --git a/de.prob.symbolic/META-INF/MANIFEST.MF b/de.prob.symbolic/META-INF/MANIFEST.MF
index 52e10653dc0de613fe409cd198ca0a1d16e8ad36..718636bd34bb20e63d61c454bb1fdee61a46fe30 100644
--- a/de.prob.symbolic/META-INF/MANIFEST.MF
+++ b/de.prob.symbolic/META-INF/MANIFEST.MF
@@ -2,11 +2,11 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Symbolic Evaluation Support
Bundle-SymbolicName: de.prob.symbolic;singleton:=true
-Bundle-Version: 1.0.0.qualifier
+Bundle-Version: 7.4.2.qualifier
Bundle-Activator: de.prob.symbolic.Activator
Require-Bundle: org.eclipse.core.runtime,
de.prob.core;bundle-version="[9.4.0,9.5.0)",
- org.eventb.ui;bundle-version="[3.0.0,3.1.0)",
+ org.eventb.ui;bundle-version="[3.0.0,3.2.0)",
de.prob.ui;bundle-version="[7.4.0,7.5.0)",
org.rodinp.core;bundle-version="[1.7.0,1.8.0)",
org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
diff --git a/de.prob.ui/META-INF/MANIFEST.MF b/de.prob.ui/META-INF/MANIFEST.MF
index 9560d2533dc204f2eedfa3b23fd178923b35b896..a4bdc20fdd9b5502c53ad00bc577bd83b2b6cf8e 100644
--- a/de.prob.ui/META-INF/MANIFEST.MF
+++ b/de.prob.ui/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Ui Plug-in
Bundle-SymbolicName: de.prob.ui;singleton:=true
-Bundle-Version: 7.4.0.qualifier
+Bundle-Version: 7.4.2.qualifier
Require-Bundle: org.eclipse.ui;bundle-version="[3.5.0,4.0.0)",
org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
org.eclipse.core.resources;bundle-version="[3.5.0,4.0.0)",
diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml
index 6bf2e1f287fe32c93a44f4924fcb7d4f3c4a6dfc..d7fbd3701c61ff4f570797202ad465b683d9ce93 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -1041,22 +1041,6 @@
<separator
name="de.prob.ui.separator2"
visible="true">
- <visibleWhen>
- <with
- variable="selection">
- <iterate
- operator="or">
- <or>
- <instanceof
- value="org.eventb.core.IMachineRoot">
- </instanceof>
- <instanceof
- value="org.eventb.core.IContextRoot">
- </instanceof>
- </or>
- </iterate>
- </with>
- </visibleWhen>
</separator>
<command
commandId="de.prob.ui.starteventbanimation"
@@ -1135,22 +1119,6 @@
<separator
name="de.prob.ui.separator1"
visible="true">
- <visibleWhen>
- <with
- variable="selection">
- <iterate
- operator="or">
- <or>
- <instanceof
- value="org.eventb.core.IMachineRoot">
- </instanceof>
- <instanceof
- value="org.eventb.core.IContextRoot">
- </instanceof>
- </or>
- </iterate>
- </with>
- </visibleWhen>
</separator>
</menuContribution>
<menuContribution
diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingJob.java b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingJob.java
index b4ec10349fd06183643c4b6eacfcc128c3688600..85b1420774409b4506cf1304b7f18e75a56093ab 100644
--- a/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingJob.java
+++ b/de.prob.ui/src/de/prob/ui/ltl/LtlCheckingJob.java
@@ -70,7 +70,7 @@ public final class LtlCheckingJob extends Job {
}
private Result doSomeModelchecking() throws ProBException {
- return LtlCheckingCommand.modelCheck(animator, formula, 500, option);
+ return LtlCheckingCommand.modelCheck(animator, formula, -1, option); // this used to be 500 instead of -1, but currently the Java side does not seem to cope with the LTL model checker returning; -1 means no maximum value
}
private boolean setSymmetry() {
diff --git a/de.prob.units/META-INF/MANIFEST.MF b/de.prob.units/META-INF/MANIFEST.MF
index fb821994124ddcbc1a64b988a414de1ce6920dc7..2d668cb186eb3384c26803c31f1a5789da4ffe57 100644
--- a/de.prob.units/META-INF/MANIFEST.MF
+++ b/de.prob.units/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: ProB Physical Units Support
Bundle-SymbolicName: de.prob.units;singleton:=true
-Bundle-Version: 1.0.0.qualifier
+Bundle-Version: 7.4.2.qualifier
Bundle-Activator: de.prob.units.Activator
Require-Bundle: org.eclipse.core.runtime,
org.eclipse.core.commands,
@@ -10,7 +10,7 @@ Require-Bundle: org.eclipse.core.runtime,
org.eclipse.jface,
org.rodinp.core;bundle-version="[1.7.0,1.8.0)",
de.prob.core;bundle-version="[9.4.0,9.5.0)",
- org.eventb.ui;bundle-version="[3.0.0,3.1.0)",
+ org.eventb.ui;bundle-version="[3.0.0,3.2.0)",
de.prob.ui;bundle-version="[7.4.0,7.5.0)",
org.eventb.core;bundle-version="[3.0.0,3.2.0)",
org.eclipse.ui.workbench
diff --git a/de.prob2.disprover.feature/feature.xml b/de.prob2.disprover.feature/feature.xml
index ef18a17292e2114b3dfef21becf966ad6f25ee1c..f31df8800fb762d5e60da20f1510b744ed9f5835 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 - EXPERIMENTAL (Dis)Prover"
- version="3.0.5.qualifier"
+ version="3.0.8.qualifier"
provider-name="HHU Düsseldorf STUPS Group">
<description url="http://www.stups.uni-duesseldorf.de/ProB">
@@ -232,14 +232,15 @@ litigation.
<requires>
<import plugin="org.eclipse.core.runtime" version="3.5.0" match="compatible"/>
<import plugin="de.prob.core" version="9.4.0" match="equivalent"/>
- <import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/>
- <import plugin="org.rodinp.core" version="1.7.0" match="equivalent"/>
- <import plugin="org.eventb.ui" version="3.0.0" match="equivalent"/>
- <import plugin="de.prob.eventb.disprover.core" version="1.3.2" match="compatible"/>
- <import plugin="org.eclipse.osgi"/>
<import plugin="org.eventb.core.seqprover" version="3.0.0"/>
<import plugin="org.eventb.core" version="3.0.0"/>
+ <import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/>
<import plugin="org.eventb.core.ast" version="3.0.0"/>
+ <import plugin="org.rodinp.core" version="1.7.0" match="equivalent"/>
+ <import plugin="org.eventb.ui" version="3.0.0"/>
+ <import plugin="org.eclipse.osgi"/>
+ <import plugin="de.prob.ui" version="7.4.0" match="greaterOrEqual"/>
+ <import plugin="de.prob.eventb.disprover.core" version="2.0.0" match="equivalent"/>
</requires>
<plugin
diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml
index 51c720033b4933c43d42c49dab5db93d26350e98..4f63793dcdc2c14a4d0028d7b0cabd6212f6da49 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.0.5.qualifier"
+ version="3.0.8.qualifier"
provider-name="HHU Düsseldorf STUPS Group">
<description url="http://www.stups.uni-duesseldorf.de/ProB">
@@ -226,23 +226,23 @@ litigation.
<requires>
<import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.ui.ide" version="3.5.0" match="compatible"/>
- <import plugin="org.eclipse.ui.views" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.runtime" version="3.5.0" match="compatible"/>
- <import plugin="org.eclipse.core.databinding" version="1.2.0" match="compatible"/>
- <import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/>
- <import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.7.0" match="compatible"/>
<import plugin="de.prob.core" version="9.4.0" match="equivalent"/>
- <import plugin="org.eclipse.help" version="3.5.100" match="greaterOrEqual"/>
+ <import plugin="org.eventb.core" version="3.0.0"/>
<import plugin="org.eclipse.core.resources" version="3.5.0" match="compatible"/>
<import plugin="org.rodinp.core" version="1.7.0" match="equivalent"/>
+ <import plugin="org.eventb.core.ast" version="3.0.0"/>
+ <import plugin="org.eventb.core.seqprover" version="3.0.0"/>
<import plugin="de.prob.ui" version="7.4.0" match="equivalent"/>
<import plugin="org.eclipse.core.expressions" version="3.4.101" match="compatible"/>
+ <import plugin="org.eclipse.ui.views" version="3.5.0" match="compatible"/>
+ <import plugin="org.eclipse.core.databinding" version="1.2.0" match="compatible"/>
+ <import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/>
+ <import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/>
+ <import plugin="org.eclipse.help" version="3.5.100" match="greaterOrEqual"/>
<import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/>
<import plugin="de.bmotionstudio.gef.editor" version="5.5.0" match="equivalent"/>
- <import plugin="org.eventb.core" version="3.0.0"/>
- <import plugin="org.eventb.core.ast" version="3.0.0"/>
- <import plugin="org.eventb.core.seqprover" version="3.0.0"/>
</requires>
<plugin
diff --git a/de.prob2.symbolic.feature/feature.xml b/de.prob2.symbolic.feature/feature.xml
index bfdeac8810ab27faeb15a9d47025172a29e69b97..e02e10ac1402d008b6b0c0922d43c5980a6c8ea4 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.0.5.qualifier"
+ version="3.0.8.qualifier"
provider-name="HHU Düsseldorf STUPS Group">
<description url="http://www.stups.uni-duesseldorf.de/ProB">
@@ -232,11 +232,11 @@ litigation.
<requires>
<import plugin="org.eclipse.core.runtime"/>
<import plugin="de.prob.core" version="9.4.0" match="equivalent"/>
- <import plugin="org.eventb.ui" version="3.0.0" match="equivalent"/>
<import plugin="de.prob.ui" version="7.4.0" match="equivalent"/>
<import plugin="org.rodinp.core" version="1.7.0" match="equivalent"/>
<import plugin="org.eclipse.ui" version="3.5.0" match="compatible"/>
<import plugin="org.eventb.core" version="3.0.0"/>
+ <import plugin="org.eventb.ui" version="3.0.0"/>
</requires>
<plugin
diff --git a/de.prob2.units.feature/feature.xml b/de.prob2.units.feature/feature.xml
index 4d04c511664d82b17498f794615778b121103fec..5a1514b4ba4c0bd6be0c7ebd9b5becb1b2a63dbb 100644
--- a/de.prob2.units.feature/feature.xml
+++ b/de.prob2.units.feature/feature.xml
@@ -2,7 +2,7 @@
<feature
id="de.prob2.units.feature"
label="ProB for Rodin3 - Physical Units Support"
- version="3.0.5.qualifier"
+ version="3.0.8.qualifier"
provider-name="HHU Düsseldorf STUPS Group">
<description url="http://www.stups.uni-duesseldorf.de/ProB">
@@ -230,10 +230,10 @@ litigation.
<import plugin="org.eclipse.jface"/>
<import plugin="org.rodinp.core" version="1.7.0" match="equivalent"/>
<import plugin="de.prob.core" version="9.4.0" match="equivalent"/>
- <import plugin="org.eventb.ui" version="3.0.0" match="equivalent"/>
<import plugin="de.prob.ui" version="7.4.0" match="equivalent"/>
- <import plugin="org.eclipse.ui.workbench"/>
<import plugin="org.eventb.core" version="3.0.0"/>
+ <import plugin="org.eclipse.ui.workbench"/>
+ <import plugin="org.eventb.ui" version="3.0.0"/>
</requires>
<plugin