Next solution does not work any longer

[GoogleCodeExporter]

With the change to subJVM process for the grounding and SAT solving steps,
it appears that the next() method that we used to call on an A4Solution
does no longer work :(

Original issue reported on code.google.com by daniel.l...@gmail.com on 8 Dec 2008 at 7:59

[GoogleCodeExporter]

Hi:  Similar tricks to A4 would have to be done to make solution enumeration 
work.

In A4, we created 2 special tasks SimpleTask1 and SimpleTask2
for doing solution solving and doing solution enumeration in subJVM.

In A4E, solution solving in subJVM works, but solution enumeration in subJVM 
doesn't
work.
That's because the current A4E way is that once a solution is solved
by the subJVM, then the solution is written to XML and then read-back from XML.
But the read-back instance is not associated with a live SAT solver.
(The live SAT solver is still alive in the subJVM, but it's out of reach from 
parent JVM)
Live SAT solver is needed to perform solution enumeration.

Please take a look at A4's SimpleTask2 and we can then discuss later
on how to apply the same approach to A4E.

Sincerely
Felix Chang
Alloy4 Lead Developer

Original comment by felix2...@gmail.com on 8 Dec 2008 at 9:20

[GoogleCodeExporter]

Felix,

Thanks for pointing me to the right direction.
I will take a look at it this week and let you know if I have some problems to 
adapt
it to A4E.

Daniel

Original comment by daniel.l...@gmail.com on 8 Dec 2008 at 9:33

[GoogleCodeExporter]

That feature need to be implemented if possible for release 0.3.0.
Please check SimpleTask2 class in A4.

Original comment by daniel.l...@gmail.com on 19 May 2011 at 8:53

[GoogleCodeExporter]

We should have time this year to fix that issue.

Original comment by daniel.l...@gmail.com on 17 Apr 2012 at 6:46