alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sat: adjust SPOT_SATSOLVER default for glucose 3.0

Browse source 
* src/misc/satsolver.cc: Add the "-model" option.
* NEWS, doc/org/satmin.org, src/bin/man/spot-x.x: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2014-02-08 21:34:35 +01:00
parent fd4a963a26
commit eb778c569a
4 changed files with 47 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -6,6 +6,10 @@ New in spot 1.2.2a (not yet released)
obtain statistics about the different iterations of the obtain statistics about the different iterations of the
SAT-based minimization. For an example, see SAT-based minimization. For an example, see
http://spot.lip6.fr/userdoc/satmin.html http://spot.lip6.fr/userdoc/satmin.html
- The default value for the SPOT_SATSOLVER environment
variable has been changed to "glucose -verb=0 -model %I >%O".
This assumes that glucose 3.0 is installed. For older
versions of glucose, remove the "-model" option.
* Bug fixes: * Bug fixes:

59
doc/org/satmin.org
View file

@ -35,14 +35,15 @@ Let us first state a few facts about this minimization procedure.
* How change the SAT solver used * How change the SAT solver used
The environment variable =SPOT_SATSOLVER= can be used to change the The environment variable =SPOT_SATSOLVER= can be used to change the
SAT solver used by Spot. The default is "=glucose %I >%O=", therefore SAT solver used by Spot. The default is "=glucose -verb=0 -model %I
if you have installed [[https://www.lri.fr/~simon/?page=glucose][=glucose=]] in your =$PATH=, it should work right >%O=", therefore if you have installed [[http://www.labri.fr/perso/lsimon/glucose/][=glucose= 3.0]] in your =$PATH=,
away. Otherwise you may redefine this variable to point the correct it should work right away. Otherwise you may redefine this variable
location or to another SAT solver. The =%I= and =%O= sequences will be to point the correct location or to another SAT solver (for older
replaced by the names of temporary files containing the input for the versions of glucose, remove the =-model= option). The =%I= and =%O=
SAT solver and receiving its output. We assume that the SAT solver sequences will be replaced by the names of temporary files containing
should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]] for input and the input for the SAT solver and receiving its output. We assume that
output. the SAT solver should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]]
for input and output.
* Enabling SAT-based minimization for deterministic automata * Enabling SAT-based minimization for deterministic automata
@ -163,7 +164,7 @@ $txt
#+RESULTS: #+RESULTS:
[[file:gfaexxb3.png]] [[file:gfaexxb3.png]]
Clearly this is automaton benefit from the transition-based Clearly this is automaton benefits from the transition-based
acceptance. If we want a traditional Büchi automaton, with acceptance. If we want a traditional Büchi automaton, with
state-based acceptance, we only need to add the =-B= option. The state-based acceptance, we only need to add the =-B= option. The
result will of course be slightly bigger. result will of course be slightly bigger.
@ -300,7 +301,7 @@ resulting 11-state DRA is converted into a 9-state DTBA by
that the formula was a recurrence. that the formula was a recurrence.
As far as SAT-based minimization goes, =dstar2tgba= will take the same As far as SAT-based minimization goes, =dstar2tgba= will take the same
options as =ltl2tgba=, so we for instance check that the smallest DTBA options as =ltl2tgba=. For instance we can see that the smallest DTBA
has 6 states: has 6 states:
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
@ -399,8 +400,8 @@ The following options can be used to fine-tune this procedure:
to belong to the same acceptance sets. to belong to the same acceptance sets.
- =-x !wdba-minimize= :: disable WDBA minimization. - =-x !wdba-minimize= :: disable WDBA minimization.
When options =-B= and =-x sat-minimize= both used, =-x state-based= and When options =-B= and =-x sat-minimize= are both used, =-x
=-x sat-acc=1= are implied. state-based= and =-x sat-acc=1= are implied.
* Logging statistics * Logging statistics
@ -420,14 +421,12 @@ cat stats.csv
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example : input(states=11) output(states=5, acc-sets=2, det=1)
input(states=11) output(states=5, acc-sets=2, det=1) :
: 9,8,35,64,44064,9043076,930,22,290,21
9,9,44,72,44064,9043076,917,20,292,12 : 7,7,33,56,14504,2191905,224,4,106,4
8,7,31,56,22272,4203158,417,7,231,9 : 6,6,28,48,10512,1358243,137,0,44,1
6,6,28,48,10512,1369289,137,1,76,2 : 5,,,,7200,782342,78,1,26,2
5,,,,7200,785942,77,1,25,1
#+end_example
The generated CSV file use the following columns: The generated CSV file use the following columns:
- the n passed to the SAT-based minimization algorithm - the n passed to the SAT-based minimization algorithm
@ -447,11 +446,15 @@ Times are measured with the times() function, and expressed
in ticks (usually: 1/100 of seconds). in ticks (usually: 1/100 of seconds).
In the above example, you can see that also the input DRA had 11 In the above example, you can see that also the input DRA had 11
states, the minimization function received a 10-state DBA (one state states. In the first line of the =stats.csv= file, you can see the
was probably simplified using simulation-based simplifications) and minimization function searching for a 9 state DTBA or obtaining a
started looking for an equivalent 9-state DTBA which it found. Then 8-state solution. (If the minimization function searched for a
looking for a 8-state DTBA, it found a solution with only 7 states, 9-state DTBA, it means it received a 10-state complete DTBA, so the
etc. No solution where found when looking for a 5-state DTBA, so the simplification performed before the minimization procedure managed to
minimal complete DTBA has 6 states. The output of =dstar2tgba= has 5 convert the 11-state DRA into a 10-state DTBA.) Starting from the
states just because it is not complete (the =--complete= option was 8-state solution, it looked for (and found) a 7-state solution, and
not given, so the useless sink state was removed). then a 6-state solution. The search for a 5-state complete DTBA
failed. The final output is reported with 5 states, because by
default we output trim automata. If the =--complete= option had been
given, the useless sink state would have been kept and the output
automaton would have 6 states.

19
src/bin/man/spot-x.x
View file

@ -24,15 +24,16 @@ user time for solving the SAT problem, system time for solving the SAT
problem. problem.
.TP .TP
\fBSPOT_SATSOLVER\fR \fBSPOT_SATSOLVER\fR If set, this variable should indicate how to call
If set, this variable should indicate how to call a SAT\-solver. This a SAT\-solver. This is used by the sat\-minimize option described
is used by the sat\-minimize option described above. The default above. The default value is \f(CW"glucose -verb=0 -model %I >%O"\fR,
value is \f(CW"glucose -verb=0 %I >%O"\fR. The escape sequences it is correct for glucose version 3.0 (for older versions, remove the
\f(CW%I\fR and \f(CW%O\fR respectively denote the names of the input \fCW(-model\fR option). The escape sequences \f(CW%I\fR and
and output files. These temporary files are created in the directory \f(CW%O\fR respectively denote the names of the input and output
specified by \fBSPOT_TMPDIR\fR or \fBTMPDIR\fR (see below). The files. These temporary files are created in the directory specified
SAT-solver should follow the convention of the SAT Competition for its by \fBSPOT_TMPDIR\fR or \fBTMPDIR\fR (see below). The SAT-solver
input and output format. should follow the convention of the SAT Competition for its input and
output format.
.TP .TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR

4
src/misc/satsolver.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -40,7 +40,7 @@ namespace spot
satsolver = getenv("SPOT_SATSOLVER"); satsolver = getenv("SPOT_SATSOLVER");
if (!satsolver) if (!satsolver)
{ {
satsolver = "glucose -verb=0 %I >%O"; satsolver = "glucose -verb=0 -model %I >%O";
return; return;
} }
prime(satsolver); prime(satsolver);