Process are not properly killed by Eclipse cancel action

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Take a specification that requires a lot of time for generating the CNF
2. Clic on progress ... on the bottom right corner
3. Hit the cancel button "Running Alloy Command ..."

What is the expected output? What do you see instead?
The process should be canceled. Instead of that, the process continue, and
could run forever.
I checked on A4, it works fine.

Note that there is a difference between A4 and A4E on process management:
A4 relaunch a new JVM per process while we are using Eclipse process
management for that.

Original issue reported on code.google.com by daniel.l...@gmail.com on 8 Apr 2008 at 2:14

[GoogleCodeExporter]

Model from Irina Rychkova that shows the problem (just try to run one of the 
check
commands):

module SIG/inciGAS

//*****************************************************************

sig Description{}

sig Addres{}

//==== Model Abstract ===============

//==============================

sig Incident{

 info: one Description,

 siteInfo: one GEOInfo, //from DB 

 t1,t2,t3,t4: one Int //t1-call time; t2 - technician on site time; t3 - site secured
time; t3 - call to FB time.

 }{(t1<t2)and(t2<t3)and(t2<t4)and(t1<t4)}

sig GEOInfo{

 a: one Int // Address,

 }

sig ServiceGas_w{

locationList: set GEOInfo,

incidentList: set Incident

}

//=====================================

//==== LA_ServiceIncidentGas_w (declarative) ================

//=====================================

pred LA_ServiceIncidentGas_w[incidentList_pre, incidentList_post: set Incident,
locationList_prepost: set GEOInfo,

                      in_info: one Int, in_call, in_address, in_secured: one Int,

                      out_incident: one Incident, out_emergency: one Int] {

//Pre:

      (in_call >0 ) => //witness call

//Post:

      (one newInc: Incident | //inc created

      (newInc in incidentList_post)and !(newInc in incidentList_pre)and

      (newInc.t1 =  in_call) and

      (one loc: GEOInfo | (loc in locationList_prepost) and (loc.a = in_address) and
(newInc.siteInfo = loc)) and

      (newInc.t3 =  in_secured) and

      (((newInc.t3 - newInc.t1 <= 4) and (out_emergency=0)) or

       ((newInc.t4 = newInc.t1 +4) and (out_emergency=1))) and

      (out_incident = newInc)

)

}

run LA_ServiceIncidentGas_w for 5

sig IncidentDB { // to be able to have quantifiers over them

db : set Incident

}

sig GeoDB {

db : set GEOInfo

}

assert LA{

      some incidentList_pre: IncidentDB , locationList_prepost: GeoDB,

        in_info: Int, in_call, in_address, in_secured: Int , incidentList_post:
IncidentDB, out_incident: Incident, out_emergency: Int |

                  LA_ServiceIncidentGas_w[incidentList_pre.db, incidentList_post.db,
locationList_prepost.db,

                   in_info, in_call, in_address, in_secured, out_incident, out_emergency]

      }

assert LA1{

      all incidentList_pre: IncidentDB , locationList_prepost: GeoDB |

      some  in_info: Int, in_call, in_address, in_secured: Int , incidentList_post:
IncidentDB, out_incident: Incident, out_emergency: Int |

                  LA_ServiceIncidentGas_w[incidentList_pre.db, incidentList_post.db,
locationList_prepost.db,

                   in_info, in_call, in_address, in_secured, out_incident, out_emergency]

      }

check LA

check LA1

Original comment by daniel.l...@gmail.com on 8 Apr 2008 at 4:27

[GoogleCodeExporter]

I currently got the very same problem with my simple model.

SAT4J has a simple method called ISolver.expireTimeout() that stops the solver 
properly.

It would be nice if A4 or KK could allow Java code to programmatically 
terminate a
SAT solver.

The current solution in A4 is to create a new JVM per solver and to kill the 
JVM to
terminate the solver.

This is maybe the best solution to kill JNI solvers.

Using a pure Java platform, using ISolver.expireTimeout should work 
out-of-the-box.

Original comment by daniel.l...@gmail.com on 1 Dec 2008 at 8:12

[GoogleCodeExporter]

After discuting the issue with Felix Chang, there is support for sub-jvm CNF
generation and SAT solving in A4 WorkerEngine class.

I will take a look at it ASAP.

Original comment by daniel.l...@gmail.com on 2 Dec 2008 at 11:12

[GoogleCodeExporter]

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

[GoogleCodeExporter]

A4E is now using the subJVM approach of A4.
Available in  release 0.2.33.

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

• Changed state: Fixed