From 21e2d9bb32198f9c9b71432125dd9f9475f0d538 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Jan 2017 09:00:26 +0100 Subject: [PATCH] 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. --- doc/org/index.org | 5 +++-- doc/org/satmin.org | 25 +++++++++++++++++-------- 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/doc/org/index.org b/doc/org/index.org index 53eb4fc59..ece19e67d 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -18,11 +18,12 @@ checking. It has the following notable features: - Several algorithms for formula manipulation including: simplifying formulas, testing implication or equivalence, testing 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, emptiness checks, simulation-based reductions, minimization of 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 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 diff --git a/doc/org/satmin.org b/doc/org/satmin.org index f1a7b73fa..73b9a415a 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -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 use state-based acceptance. (They simply restrict all the outgoing 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. - However, it is still possible to use an external SAT solver (as described - below). +4) Spot is built using PicoSAT call_version()[:results raw]. + This solver was chosen for its performances, simplicity of + 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. If they fail to determinize the property, they will simply output a nondeterministic automaton, if they managed to obtain a @@ -49,12 +50,20 @@ Let us first state a few facts about this minimization procedure. * 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 -SAT solver used by Spot. By default it uses the one distributed with (PicoSAT -call_version()[:results raw]). -Here is the expected format of =SPOT_SATSOLVER= : "= [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. -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. -We assume that the SAT solver should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]] for input and output. +SAT solver used by Spot. This variable should describe a shell command +to run the SAT-solver on an input file called =%I= so that a model satisfying +the formula will be written in =%O=. For instance to use [[http://www.labri.fr/perso/lsimon/glucose/][Glucose 3.0]], instead +of the builtin version of PicoSAT, define +#+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=