Commit 21e2d9bb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: a few additional links

* doc/org/index.org: Add links to the hierarchy and sat-minimization.
* doc/org/satmin.org: Show how to use glucose.
parent 8f9d165c
...@@ -18,11 +18,12 @@ checking. It has the following notable features: ...@@ -18,11 +18,12 @@ checking. It has the following notable features:
- Several algorithms for formula manipulation including: simplifying - Several algorithms for formula manipulation including: simplifying
formulas, testing implication or equivalence, testing formulas, testing implication or equivalence, testing
stutter-invariance, removing some operators by rewriting, translation stutter-invariance, removing some operators by rewriting, translation
to automata... to automata, testing membership to the [[file:hierarchy.org][temporal hierarchy of Manna & Pnueli]]...
- Several algorithms for automata manipulation including: product, - Several algorithms for automata manipulation including: product,
emptiness checks, simulation-based reductions, minimization of emptiness checks, simulation-based reductions, minimization of
weak-DBA, removal of useless SCCs, acceptance-condition weak-DBA, removal of useless SCCs, acceptance-condition
transformations, determinization, etc. transformations, determinization, [[file:satmin.org][SAT-based minimization of
deterministic automata]], etc.
- In addition to the C++ interface, most of its algorithms are usable - In addition to the C++ interface, most of its algorithms are usable
via [[file:tools.org][command-line tools]], and via [[file:tut.org][Python bindings]]. via [[file:tools.org][command-line tools]], and via [[file:tut.org][Python bindings]].
- One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but - One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but
......
...@@ -28,9 +28,10 @@ Let us first state a few facts about this minimization procedure. ...@@ -28,9 +28,10 @@ Let us first state a few facts about this minimization procedure.
3) These two procedures can optionally constrain their output to 3) These two procedures can optionally constrain their output to
use state-based acceptance. (They simply restrict all the outgoing use state-based acceptance. (They simply restrict all the outgoing
transitions of a state to belong to the same acceptance sets.) transitions of a state to belong to the same acceptance sets.)
4) Spot distributes a SAT solver, PicoSAT call_version()[:results raw]. This solver was chosen for its performances, simplicity of integration and licence compatible with Spot's one. 4) Spot is built using PicoSAT call_version()[:results raw].
However, it is still possible to use an external SAT solver (as described This solver was chosen for its performances, simplicity of
below). integration and license compatibility. However, it is
still possible to use an external SAT solver (as described below).
5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton. 5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton.
If they fail to determinize the property, they will simply output a If they fail to determinize the property, they will simply output a
nondeterministic automaton, if they managed to obtain a nondeterministic automaton, if they managed to obtain a
...@@ -49,12 +50,20 @@ Let us first state a few facts about this minimization procedure. ...@@ -49,12 +50,20 @@ Let us first state a few facts about this minimization procedure.
* How to change the SAT solver used * How to change the SAT solver used
By default Spot uses PicoSAT call_version()[:results raw]), this SAT-solver
is built into the Spot library, so that no temporary files are used to
store the problem.
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. By default it uses the one distributed with (PicoSAT SAT solver used by Spot. This variable should describe a shell command
call_version()[:results raw]). to run the SAT-solver on an input file called =%I= so that a model satisfying
Here is the expected format of =SPOT_SATSOLVER= : "=<SAT_SOLVER> [options] %I >%O=". The =%I= and =%O= sequences will be replaced by the names of temporary files containing the input for the SAT solver and receiving its output. the formula will be written in =%O=. For instance to use [[http://www.labri.fr/perso/lsimon/glucose/][Glucose 3.0]], instead
If you have installed the corresponding binary in your =$PATH=, it should work right away. Otherwise you may redefine this variable to point the correct location of the SAT solver. of the builtin version of PicoSAT, define
We assume that the SAT solver should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]] for input and output. #+BEGIN_SRC sh
export SPOT_SATSOLVER='glucose -verb=0 -model %I >%O'
#+END_SRC
We assume the SAT solver follows the input/output conventions of the
[[http://www.satcompetition.org/][SAT competition]]
* Enabling SAT-based minimization in =ltl2tgba= or =dstar2tgba= * Enabling SAT-based minimization in =ltl2tgba= or =dstar2tgba=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment