Question about executing checks in Eclipse Alloy

[yirco]

Hi,

Alloy in Eclipse is a great idea. Better user experience.

I have this question if I may. I ran the Alloy example from:
http://alloy.mit.edu/alloy4/tutorial4/currentmodel-FS-1.html

using the traditional Alloy Analyzer 4.1.10 and the Eclipse Alloy
plugin

When I change this:

// File system has one root
assert oneRoot { one d: Dir | no d.parent }

to this (one -> no)

// File system has one root
assert oneRoot { no d: Dir | no d.parent }

The traditional Analyzer shows a counterexample but the Eclipse Alloy
does not. It writes in the console:
============ Command Check oneRoot for 5: ============
============ Total time: 0 (ms) ===========
============ Answer ============

Am I doing anything incorrectly?

Thank you.

[DanArBer]

hi,

Could you tell us which version of the plugin you are using, on which
operating system?

It looks like you are getting into a bug causes by running A4 in a
subprocess within Eclipse.
That should be fixed in the latest versions of the plugin.

Daniel

[yirco]

Hello Daniel,

I used the update site:
http://alloy4eclipse.googlecode.com/svn/trunk/updatesite/

In About Eclipse it says:
Alloy Plug-in 0.2.36

Plug-in details:
Alloy Launch Plug-in 4.2.0
Alloy Plug-in 0.2.35
Help Plug-in 1.0.1
pluginName 0.0.10

Jirka

[DanArBer]

Jirka,

Could you go to the A4E preference page and try to check the first
box:
Execute Alloy tasks Locally ...

and see if it works better?

Which SAT solver are you using?

Daniel

[yirco]

I tried it both checked and unchecked: Execute Alloy tasks locally ...
I use the standard defaults, i.e. SAT4J and tried others with the same
results.

When I check an assert or run a predicate it creates a new xml file
the the folder output. When I click the xml file, the Eclipse gets
stuck - not responding. I need to end the Eclipse process. I run it on
Windows.

[Pascal A]

hi

I'm a new A4E user and I meet the same problem
did you solve this issue ?

best regards

PA