search

SpriMoon / alloy4eclipse

Automatically exported from code.google.com/p/alloy4eclipse
0 stars 0 forks source link

A4Solution ans is null when answer is unsat #84

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
We are now delegating the CNF generation and the resolution to a subprocess.

There is no real serialization mechanism to move an A4Solution object from
the subJVM to the main JVM.

When the answer is SAT, the subJVM creates an XML file that is then read by
the main thread.

But we have no way to create an A4Solution when the answer if unsat.

The current code is broken in the sense that we have a null A4Solution
object lying around when the answer is unsat.

We need to find an elegant way to solve that issue.

Original issue reported on code.google.com by daniel.l...@gmail.com on 4 Feb 2009 at 8:24

GoogleCodeExporter commented 9 years ago 
It would be nice to check if it is really the case in current code.

Original comment by daniel.l...@gmail.com on 18 May 2011 at 7:59

GoogleCodeExporter commented 9 years ago 
We need to check in A4 source done how this case is handled.

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