I've tried the farmer model with plugin 0.1.7 and eclipse 3.2.1:
module farmer
open util/ordering[State] as Ord
abstract sig Object {eats: set Object}
one sig Farmer, Fox, Chicken, Grain extends Object {}
fact eating { eats = Fox->Chicken + Chicken->Grain}
sig State {
near: set Object,
far: set Object
}
fact initialState {
let s0 = first[] |
s0.near = Object && no s0.far
}
pred crossRiver (from, from', to, to': set Object) {
// either the farmer takes no items
(from' = from - Farmer &&
to' = to - to.eats + Farmer ) ||
// or the Farmer takes one item
some item: from - Farmer {
from' = from - Farmer - item
to' = to - to.eats + Farmer + item
}
}
fact stateTransition {
all s: State, s': next[s] {
Farmer in s.near => crossRiver[s.near, s'.near, s.far, s'.far] else
crossRiver[s.far, s'.far, s.near, s'.near]
}
}
pred solvePuzzle() {
last[].far = Object
}
run solvePuzzle for 8 State expect 1
I run the command and everything is ok. Ask to see the model and the
xml file is shown. When I click on the graph tab the graph window goes
gray and nothing is shown.
Is there anything I should setup?
Cheers,
Paulo Matos
It works fine for me under Linux.
I guess you are using A4E under windows?
It looks like there is an issue (and a potential fix) with the current
plugin with Win32:
http://code.google.com/p/alloy4eclipse/issues/detail?id=20
Daniel
On Sep 19, 5:38 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
> Hi Paulo,
>
> It works fine for me under Linux.
>
> I guess you are using A4E under windows?
>
No, Linux... not working for me. Any thing I need to install? (apart
from graphviz?)
That's a bad news. I works fine for me both on my linux box and my mac
os iBook.
I use Eclipse 3.3 europa, not 3.2. But it should not be the problem.
Are you using Gnome or KDE?
On Sep 19, 8:02 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
> On 19 sep, 19:26, Paulo Matos <pocma...@gmail.com> wrote:
>
> > On Sep 19, 5:38 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > > Hi Paulo,
>
> > > It works fine for me under Linux.
>
> > > I guess you are using A4E under windows?
>
> > No, Linux... not working for me. Any thing I need to install? (apart
> > from graphviz?)
>
> That's a bad news. I works fine for me both on my linux box and my mac
> os iBook.
>
> I use Eclipse 3.3 europa, not 3.2. But it should not be the problem.
>
> Are you using Gnome or KDE?
>
None, I'm using XFCE4 in both my office and home PCs. I just arrived
at the home, tried the same example and get the exact same problem.
Gray window, no graph. Snapshot here:
http://users.ecs.soton.ac.uk/pocm06r/a4e_problem.png
Any ideas on this?
The dot binary should be available in the /tmp/aloy4tmp-??????????
directory of your computer.
(this is an ugly hack used in Alloy4 too). We haven't found yet how to
properly use platform dependent binaries with eclipse plugins yet.
Can you check that this directory exists?
If it does not exists, can you display the os.name and os.arch values
given by System.getProperty("os.name")?
On Sep 20, 9:36 am, DanArBer <daniel.lebe...@gmail.com> wrote:
> Paolo,
>
> The dot binary should be available in the /tmp/aloy4tmp-??????????
> directory of your computer.
> (this is an ugly hack used in Alloy4 too). We haven't found yet how to
> properly use platform dependent binaries with eclipse plugins yet.
>
> Can you check that this directory exists?
>
2 directories alloy4tmp-???? exist. No binaries inside.
> If it does not exists, can you display the os.name and os.arch values
> given by System.getProperty("os.name")?
package main;
public class SysProps {
/**
* @param args
*/
public static void main(String[] args) {
System.out.println(System.getProperty("os.name"));
System.out.println(System.getProperty("os.arch"));
}
}
returns:
Linux
amd64
Paulo, is visualization working using Alloy4 usual GUI?
Felix, would it be possible to have amd64 binaries for Linux?
Daniel
On Sep 20, 10:11 am, DanArBer <daniel.lebe...@gmail.com> wrote:
> ok, we got it, finally : there is no precompiled binaries for amd64 :)
>
> Paulo, is visualization working using Alloy4 usual GUI?
>
Yes! :)
Release 0.1.8 is on the update site.
I should solve your problem, and allow code completion of alloy
keywords.
Let us know if it works for you.
Daniel
On Sep 20, 11:06 am, DanArBer <daniel.lebe...@gmail.com> wrote:
> Paulo,
>
> Release 0.1.8 is on the update site.
>
> I should solve your problem, and allow code completion of alloy
> keywords.
>
Hum :(
Now I can't even edit an alloy file. Instead of the editor I get:
Unable to create this part due to an internal error. Reason for the
failure: Can't find bundle for base name messages, locale en_US
java.util.MissingResourceException: Can't find bundle for base name
messages, locale en_US
at
java.util.ResourceBundle.throwMissingResourceException(ResourceBundle.java:
1508)
at java.util.ResourceBundle.getBundleImpl(ResourceBundle.java:1262)
at java.util.ResourceBundle.getBundle(ResourceBundle.java:717)
at
fr.univartois.cril.alloyplugin.editor.ALSEditor.createActions(ALSEditor.java:
59)
at
org.eclipse.ui.texteditor.AbstractTextEditor.createPartControl(AbstractTextEditor.java:
2682)
at
org.eclipse.ui.texteditor.StatusTextEditor.createPartControl(StatusTextEditor.java:
53)
at
org.eclipse.ui.texteditor.AbstractDecoratedTextEditor.createPartControl(AbstractDecoratedTextEditor.java:
367)
at
org.eclipse.ui.internal.EditorReference.createPartHelper(EditorReference.java:
596)
at
org.eclipse.ui.internal.EditorReference.createPart(EditorReference.java:
372)
at
org.eclipse.ui.internal.WorkbenchPartReference.getPart(WorkbenchPartReference.java:
566)
at org.eclipse.ui.internal.PartPane.setVisible(PartPane.java:290)
at
org.eclipse.ui.internal.presentations.PresentablePart.setVisible(PresentablePart.java:
140)
at
org.eclipse.ui.internal.presentations.util.PresentablePartFolder.select(PresentablePartFolder.java:
268)
at
org.eclipse.ui.internal.presentations.util.LeftToRightTabOrder.select(LeftToRightTabOrder.java:
65)
at
org.eclipse.ui.internal.presentations.util.TabbedStackPresentation.selectPart(TabbedStackPresentation.java:
394)
at
org.eclipse.ui.internal.PartStack.refreshPresentationSelection(PartStack.java:
1144)
at org.eclipse.ui.internal.PartStack.setSelection(PartStack.java:
1097)
at org.eclipse.ui.internal.PartStack.showPart(PartStack.java:1311)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:455)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:102)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:441)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:111)
at
org.eclipse.ui.internal.EditorSashContainer.addEditor(EditorSashContainer.java:
60)
at
org.eclipse.ui.internal.EditorAreaHelper.addToLayout(EditorAreaHelper.java:
217)
at
org.eclipse.ui.internal.EditorAreaHelper.addEditor(EditorAreaHelper.java:
207)
at
org.eclipse.ui.internal.EditorManager.createEditorTab(EditorManager.java:
820)
at
org.eclipse.ui.internal.EditorManager.openEditorFromDescriptor(EditorManager.java:
719)
at
org.eclipse.ui.internal.EditorManager.openEditor(EditorManager.java:
680)
at
org.eclipse.ui.internal.WorkbenchPage.busyOpenEditorBatched(WorkbenchPage.java:
2593)
at
org.eclipse.ui.internal.WorkbenchPage.busyOpenEditor(WorkbenchPage.java:
2528)
at org.eclipse.ui.internal.WorkbenchPage.access$10(WorkbenchPage.java:
2520)
at org.eclipse.ui.internal.WorkbenchPage$9.run(WorkbenchPage.java:
2505)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:
67)
at
org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:
2500)
at
org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:
2485)
at org.eclipse.ui.ide.IDE.openEditor(IDE.java:388)
at org.eclipse.ui.ide.IDE.openEditor(IDE.java:350)
at
org.eclipse.jdt.internal.ui.javaeditor.EditorUtility.openInEditor(EditorUtility.java:
275)
at
org.eclipse.jdt.internal.ui.javaeditor.EditorUtility.openInEditor(EditorUtility.java:
139)
at
org.eclipse.jdt.internal.ui.actions.OpenActionUtil.open(OpenActionUtil.java:
49)
at org.eclipse.jdt.ui.actions.OpenAction.run(OpenAction.java:190)
at org.eclipse.jdt.ui.actions.OpenAction.run(OpenAction.java:174)
at
org.eclipse.jdt.ui.actions.SelectionDispatchAction.dispatchRun(SelectionDispatchAction.java:
267)
at
org.eclipse.jdt.ui.actions.SelectionDispatchAction.run(SelectionDispatchAction.java:
243)
at
org.eclipse.jdt.internal.ui.packageview.PackageExplorerActionGroup.handleOpen(PackageExplorerActionGroup.java:
306)
at org.eclipse.jdt.internal.ui.packageview.PackageExplorerPart
$4.open(PackageExplorerPart.java:653)
at org.eclipse.jface.viewers.StructuredViewer
$2.run(StructuredViewer.java:817)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:37)
at org.eclipse.core.runtime.Platform.run(Platform.java:852)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:44)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:149)
at
org.eclipse.jface.viewers.StructuredViewer.fireOpen(StructuredViewer.java:
815)
at
org.eclipse.jface.viewers.StructuredViewer.handleOpen(StructuredViewer.java:
1069)
at org.eclipse.jface.viewers.StructuredViewer
$6.handleOpen(StructuredViewer.java:1168)
at
org.eclipse.jface.util.OpenStrategy.fireOpenEvent(OpenStrategy.java:
249)
at org.eclipse.jface.util.OpenStrategy.access$2(OpenStrategy.java:
243)
at org.eclipse.jface.util.OpenStrategy
$1.handleEvent(OpenStrategy.java:283)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:66)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1085)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:
3154)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:2830)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:
1914)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:1878)
at
org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:
419)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:
149)
at org.eclipse.ui.internal.ide.IDEApplication.run(IDEApplication.java:
95)
at org.eclipse.core.internal.runtime.PlatformActivator
$1.run(PlatformActivator.java:78)
at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:
92)
at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:
68)
at
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:
400)
at
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:
177)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.eclipse.core.launcher.Main.invokeFramework(Main.java:336)
at org.eclipse.core.launcher.Main.basicRun(Main.java:280)
at org.eclipse.core.launcher.Main.run(Main.java:977)
at org.eclipse.core.launcher.Main.main(Main.java:952)
Release 0.1.9 solves the problem.
I forgot to include the message.properties file in the plugin jar :(
Daniel
On Sep 20, 11:32 am, DanArBer <daniel.lebe...@gmail.com> wrote:
> My mistake.
>
> Release 0.1.9 solves the problem.
>
Well Daniel, really sorry for keep bugging you. Now, I came home for
lunch so hopefully it already works in office but at home it still
doesn't work. Going back to previous questions, system properties are:
Linux
i386
and I have the following binaries inside the alloy4tmp-??? folder:
berkmin* dotbin* libminisat.so* libzchaff_basic.so* minisat1*
Shouldn't it be just 'dot' instead of 'dotbin'?
On Sep 20, 12:47 pm, Paulo Matos <pocma...@gmail.com> wrote:
> On Sep 20, 11:32 am, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > My mistake.
>
> > Release 0.1.9 solves the problem.
>
> Well Daniel, really sorry for keep bugging you. Now, I came home for
> lunch so hopefully it already works in office but at home it still
> doesn't work. Going back to previous questions, system properties are:
> Linux
> i386
>
> and I have the following binaries inside the alloy4tmp-??? folder:
> berkmin* dotbin* libminisat.so* libzchaff_basic.so* minisat1*
>
> Shouldn't it be just 'dot' instead of 'dotbin'?
>
Well, everything looks fine there.
Did you try to resize the graph window to see if it is a refresh
problem as for Nicolas's problem on Win32?
Unfortunately nothing shows up here and it is not a refresh problem.
Is there any way to get debugging messages over the console?
If you get the source code of the plugin from SVN,
http://code.google.com/p/alloy4eclipse/source
(just grab the two projects fr.univartois.cril.alloyplugin/ and
fr.univartois.cril.alloyplugin.launch/).
then using Run as ... Eclipse application on
fr.univartois.cril.alloyplugin
will launch a new Eclipse with the plugin installed and many debug
messages on the console.
Daniel
On Sep 20, 2:28 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
> On Sep 20, 2:55 pm, Paulo Matos <pocma...@gmail.com> wrote:
>
>
>
> > On Sep 20, 12:41 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > > On Sep 20, 12:47 pm, Paulo Matos <pocma...@gmail.com> wrote:
>
> > > > On Sep 20, 11:32 am, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > > > > My mistake.
>
> > > > > Release 0.1.9 solves the problem.
>
> > > > Well Daniel, really sorry for keep bugging you. Now, I came home for
> > > > lunch so hopefully it already works in office but at home it still
> > > > doesn't work. Going back to previous questions, system properties are:
> > > > Linux
> > > > i386
>
> > > > and I have the following binaries inside the alloy4tmp-??? folder:
> > > > berkmin* dotbin* libminisat.so* libzchaff_basic.so* minisat1*
>
> > > > Shouldn't it be just 'dot' instead of 'dotbin'?
>
> > > Well, everything looks fine there.
>
> > > Did you try to resize the graph window to see if it is a refresh
> > > problem as for Nicolas's problem on Win32?
>
> > Unfortunately nothing shows up here and it is not a refresh problem.
> > Is there any way to get debugging messages over the console?
>
> If you get the source code of the plugin from SVN,http://code.google.com/p/alloy4eclipse/source
>
> (just grab the two projects fr.univartois.cril.alloyplugin/ and
> fr.univartois.cril.alloyplugin.launch/).
>
> then using Run as ... Eclipse application on
> fr.univartois.cril.alloyplugin
> will launch a new Eclipse with the plugin installed and many debug
> messages on the console.
>
Thank you, I'll try that later on and I'll let you know.
> Daniel
On Sep 20, 2:28 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
> On Sep 20, 2:55 pm, Paulo Matos <pocma...@gmail.com> wrote:
>
>
>
> > On Sep 20, 12:41 pm, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > > On Sep 20, 12:47 pm, Paulo Matos <pocma...@gmail.com> wrote:
>
> > > > On Sep 20, 11:32 am, DanArBer <daniel.lebe...@gmail.com> wrote:
>
> > > > > My mistake.
>
> > > > > Release 0.1.9 solves the problem.
>
> > > > Well Daniel, really sorry for keep bugging you. Now, I came home for
> > > > lunch so hopefully it already works in office but at home it still
> > > > doesn't work. Going back to previous questions, system properties are:
> > > > Linux
> > > > i386
>
> > > > and I have the following binaries inside the alloy4tmp-??? folder:
> > > > berkmin* dotbin* libminisat.so* libzchaff_basic.so* minisat1*
>
> > > > Shouldn't it be just 'dot' instead of 'dotbin'?
>
> > > Well, everything looks fine there.
>
> > > Did you try to resize the graph window to see if it is a refresh
> > > problem as for Nicolas's problem on Win32?
>
> > Unfortunately nothing shows up here and it is not a refresh problem.
> > Is there any way to get debugging messages over the console?
>
> If you get the source code of the plugin from SVN,http://code.google.com/p/alloy4eclipse/source
>
> (just grab the two projects fr.univartois.cril.alloyplugin/ and
> fr.univartois.cril.alloyplugin.launch/).
>
> then using Run as ... Eclipse application on
> fr.univartois.cril.alloyplugin
> will launch a new Eclipse with the plugin installed and many debug
> messages on the console.
>
Hello Daniel, I tried to run the source, but a couple of lines show as
errors. I'm definitely missing something. Probably the libraries
related to plugins development. For example, this line is underlined:
import org.eclipse.ui.plugin.AbstractUIPlugin;
What's the best way to get these libraries?
Cheers,
Paulo Matos
> Daniel
Be sure to clean your project after checkout. It happens from time to
time that compilations problems appear after checking out.
I won't read my emails in the next few days. I hope someone else in
the list will answer your questions if you run into other problems.
Daniel
On Sep 21, 10:01 am, DanArBer <daniel.lebe...@gmail.com> wrote:
> You need to have the Plugin Development Environment (PDE) installed.
>
> Be sure to clean your project after checkout. It happens from time to
> time that compilations problems appear after checking out.
>
> I won't read my emails in the next few days. I hope someone else in
> the list will answer your questions if you run into other problems.
>
OK, I will, anyway, I can't seem to find the PDE update site. Do you
know it?
Release 0.1.20 is on the update site.
There is a fix for Win32 users from Nicolas Rouquette inside.
Are you using a linux64 version of Eclipse or a linux32 one?
A4E is reported to work fine on a Ubuntu 64 with a linux32 Eclipse.
--Daniel
Nicolas Rouquette and Felix Chang found a bug in the current codebase.
Release 0.1.11 is on the update site.
It is likely that the new release fixes your problem.
Could you check, please?
--Daniel
Yes, now everything is working great with 0.1.12 on my two linux
boxes, be it 32 or 64 bit.
Thanks,
Paulo Matos
> --Daniel