Implement subJVM run of KK and SAT solving.

[GoogleCodeExporter]

In A4, the translation into CNF and the SAT solving process are running in
a separate JVM. That way, it is always possible to stop that process
without fine grain control of interruption in either KK or the SAT solver.

It should be straightforward to implement this in A4E since all the hard
work is already done in the class WorkerEngine.

Unfortunately, it means that the class that implements A4Reporter must be
Serializable.

This is not the case in A4E and there is no easy way to make that class
Serializable.

It is likely that the current architecture must be modified in order to use
the subJVM approach.

That will be an important feature in the future. I am unlikely that such
feature can be implemented before April 2009 (provided that two new
students work on the project).

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

[GoogleCodeExporter]

Here is the code of some classes modified to work with WorkerEngine. The MyTask 
file
was provided by Felix Chang and adapted for A4E.

It does not work since the Reporter class is not Serializable.

Original comment by daniel.l...@gmail.com on 3 Dec 2008 at 7:58

Attachments:

• MyTask.java
• AbstractCommand.java
• ExecutableCommand.java

[GoogleCodeExporter]

Thanks to the hard work of Felix, the change was easier than expected.
It is available in 0.2.33.

Original comment by daniel.l...@gmail.com on 6 Dec 2008 at 8:22

• Changed state: Fixed