|
|
|
SearchNavigationUser login |
Performance
|
||||
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte
into their corresponding primitive numerical value (so that they can be compared) is expensive.
You can speed up a bit by saying "some j1: seq/Int",
since you seem to be trying to find a sequence index corresponding to something...
and seq/Int is exactly the set of legal sequence indices.
(And it automatically excludes negative values so you don't even need "j1 >= 0")
Also, try going to Options menu, then change SAT solver to "MiniSat".
Executing "Run test for 4 int, 7 seq"
Solver=minisat(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
8936 vars. 234 primary vars. 19989 clauses. 118342ms.
No instance found. Predicate may be inconsistent. 31ms.
Look at the time reported, I realize that the time to convert
the constraints to CNF is still very large compared to the time to search for the solution. Do you think it is normal?
Is there any way (general/specific) to arrange the constraints to speed up the conversion to CNF?
pred t_rec1 [n: State, j: seq/Int, is: iSeq, ss: sSeq] {
some j1: seq/Int | j1 < j &&
{some n1: State | n1 = ss.seqStates[j1] &&
{some t: iSeq | t = extract[is, j1, j-1] &&
{some j2: seq/Int | j2 != j1 &&
j2 < #inds[is.seqInputs] && ss.seqStates[j2] = n1 &&
{some j3: seq/Int | j3 > j2 &&
j3 < #inds[is.seqInputs] &&
ss.seqStates[j3] = n && extract[is, j2, j3-1] = t &&
subSeq[getDS[n1], t, 0] && d_rec[n, j3, is, ss]}}}}
}
Note that the cost of reducing a model into a true/false answer
has to be paid somewhere.
If we use a sloppier Alloy->Kodkod->CNF translation,
then we end up with a bigger CNF that will take longer
for the SAT solver to crunch down.
If we use very aggressive circuit simplification as we do now,
we sometimes spend a lot of time converting to CNF,
but the final CNF is trivial.
So the cost has to be paid somewhere.
(By the way, are you using the "seq" keyword and/or the util/sequniv module?
I forgot to ask you. The "seq/Int" is defined to be the set of indices
used by the util/sequniv module (which is automatically imported by the "seq" keyword.
But if you're using util/sequence or other sequence module, then seq/Int
will *not* match it, and you will end up with a seemingly correct but in fact incorrect model)
Thanks for your help.
I'd like to share some experience:
Although I limited the scope to seq 7 (4 int),
and the FSM model is kept very small,
Alloy took me more than 81 hrs for CNF translation,
then only 47 ms to solve.
The code causing such the situation is identified as below.
Of course, the formulas are a bit complicated.
Executing "Run test for 4 int, 7 seq"
Solver=minisat(jni) Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
13522 vars. 234 primary vars. 24425 clauses. 293626062ms.
No instance found. Predicate may be inconsistent. 47ms.
// Node n is t_recognized in sequence is along ss
// Again, recursive calls are not allowed in Alloy 4
// Here implement only two levels of it
pred t_rec2 [n: State, j: seq/Int, is: iSeq, ss: sSeq] {
some j1: seq/Int | j1 < j &} &}}}}
}
pred t_rec1 [n: State, j: seq/Int, is: iSeq, ss: sSeq] {
// see above
}
Thanks,
takes place in Java (and is subject to extremely severe garbage collection
penalty if you don't have enough memory).
On the other hand, CNF solving is done in C/C++, and does not use
garbage collection.
81 hours of translation definitely points to excessive swapping and/or
excessive garbage collection I believe.
Try running it on a machine with more physical ram,
and then go to Options menu and increase the amount of memory you give.
(And you may need to use 64-bit Windows rather than 32-bit Windows
to give more memory to your Java virtual environment)