Closed GoogleCodeExporter closed 9 years ago
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
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
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
Original comment by daniel.l...@gmail.com
on 3 Dec 2008 at 7:59
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
Original issue reported on code.google.com by
daniel.l...@gmail.com
on 8 Apr 2008 at 2:14