org: run a spell checker on the documentation
* doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org, doc/org/tut52.org, doc/org/tut90.org, doc/org/upgrade2.org: Run ispell-buffer on all these. * bin/autfilt.cc, python/spot/__init__.py: Fix typos in help texts noticed while spell-checking the org files.
This commit is contained in:
Alexandre Duret-Lutz
parent
0fbc83e9c2
commit
f3b8bf8e56
45 changed files with 317 additions and 194 deletions
|
|
@ -185,7 +185,7 @@ static const argp_option options[] =
|
|||
"match automata with a number of declared, but unused atomic "
|
||||
"propositions in RANGE", 0 },
|
||||
{ "acceptance-is", OPT_ACCEPTANCE_IS, "NAME|FORMULA", 0,
|
||||
"match automata with given accetance condition", 0 },
|
||||
"match automata with given acceptance condition", 0 },
|
||||
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
|
||||
"keep automata that are isomorphic to the automaton in FILENAME", 0 },
|
||||
{ "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
|
||||
|
|
|
|||
|
|
@ -491,4 +491,13 @@ rm -f autcross.csv
|
|||
# LocalWords: bQiY IubpMs dfmYfX NXLr zSwXhW bDOq og mUp QVurtU ap
|
||||
# LocalWords: ok complementation Ai Aj gRqrd ubUpHb JxFi oQGbj SQT
|
||||
# LocalWords: kWt Eo Xsc WXgCB vLwKMQ tI SXF qqlE KXplk ZFTCz PNY
|
||||
# LocalWords: hUAK IjnFhD cWys ZqjdQh
|
||||
# LocalWords: hUAK IjnFhD cWys ZqjdQh args ltlcross CSV SRC sed HB
|
||||
# LocalWords: LBTT's LBTT lOYLT WGO UIX wx abng Eq WdZ CvfJ tYq dpa
|
||||
# LocalWords: YvkfS ahOMS HdynHB PcREk XcblC tgba csv YPfmR bT DpL
|
||||
# LocalWords: gpYcBB mxsGU fPCaeC hgYD xM YU Qu hwVVVD MLmVq edfVVE
|
||||
# LocalWords: ATTR acc scc nondetstates noweb EOF ttpQt elszrt isDr
|
||||
# LocalWords: rFJYtN BwKL KHA BSYDwC DjL hw PASD ltldo genltl Gp fP
|
||||
# LocalWords: VyvQVJ fVtUyh cNgs MWSMMU oVyBs XF XFp Tgzsu aOBmny
|
||||
# LocalWords: Sg al iPt iZ aA xyBCkm Ju FyS HU Xy rVG veUbt Rceyvf
|
||||
# LocalWords: YXtcP imCn LwA xF aUm xdVyk UpeRPV kI yARu IDzrh
|
||||
# LocalWords: parallelization xargs findutils moreutils
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: =autfilt=
|
||||
#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting ω-automata.
|
||||
#+DESCRIPTION: Spot command-line tool for filtering, transforming, and converting ω-automata.
|
||||
#+INCLUDE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
#+PROPERTY: header-args:sh :results verbatim :exports both
|
||||
|
|
@ -9,10 +9,10 @@ The =autfilt= tool can filter, transform, and convert a stream of automata.
|
|||
|
||||
The tool operates a loop over 5 phases:
|
||||
- input one automaton
|
||||
- optionally preprocess the automaton
|
||||
- optionally pre-process the automaton
|
||||
- optionally filter the automaton (i.e., decide whether to ignore the
|
||||
automaton or continue with it)
|
||||
- optionally postprocess the automaton (to simply it or change its acceptance)
|
||||
- optionally post-process the automaton (to simply it or change its acceptance)
|
||||
- output the automaton
|
||||
|
||||
The simplest way to use the tool is simply to use it for input and
|
||||
|
|
@ -211,7 +211,7 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|||
in RANGE
|
||||
--accept-word=WORD keep automata that accept WORD
|
||||
--acceptance-is=NAME|FORMULA
|
||||
match automata with given accetance condition
|
||||
match automata with given acceptance condition
|
||||
--ap=RANGE match automata with a number of (declared) atomic
|
||||
propositions in RANGE
|
||||
--are-isomorphic=FILENAME keep automata that are isomorphic to the
|
||||
|
|
@ -248,6 +248,8 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|||
--is-weak keep only weak automata
|
||||
--nondet-states=RANGE keep automata whose number of nondeterministic
|
||||
states is in RANGE
|
||||
-N, --nth=RANGE assuming input automata are numbered from 1, keep
|
||||
only those in RANGE
|
||||
--rej-sccs=RANGE, --rejecting-sccs=RANGE
|
||||
keep automata whose number of non-trivial
|
||||
rejecting SCCs is in RANGE
|
||||
|
|
@ -809,7 +811,7 @@ randltl -n -1 a b | ltlfilt --simplify --remove-wm |
|
|||
:header-args:sh: :results verbatim :exports code
|
||||
:END:
|
||||
|
||||
We know from a previous exemple that formula =a U b U c= accepts the
|
||||
We know from a previous example that formula =a U b U c= accepts the
|
||||
word =b; cycle{c}=. We can actually highlight the corresponding
|
||||
run in the automaton:
|
||||
|
||||
|
|
@ -868,3 +870,13 @@ ltl2tgba 'F((b R a) W Gb)' |
|
|||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f example.hoa aut-ex1.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args pre LBTT's dstar lbtt SRC EOF DOTEXTRA
|
||||
# LocalWords: rankdir invis init fi randaut acc SCCs det tgba sed
|
||||
# LocalWords: CSV iw dges tates sccs ap SCC nondet rej triv ba Dax
|
||||
# LocalWords: cobuchi coBuchi superset sbacc determinized al ATVA
|
||||
# LocalWords: Safra Redziejowski cnf scc aN subautomaton destut dnf
|
||||
# LocalWords: dualize APs rabin gra streett gsa instut NUM incr aut
|
||||
# LocalWords: langmap preproc PicoSAT SATsolver SATSOLVER svg txt
|
||||
# LocalWords: randltl ltlfilt uniq Fb XF ltldo wm Gb GFa FG hlword
|
||||
# LocalWords: hlnondet
|
||||
|
|
|
|||
|
|
@ -19,7 +19,6 @@ use the following reference:
|
|||
of the library, [[file:tools.org][the tools]], the Python bindings), and provides many
|
||||
references detailing more specific aspects.
|
||||
|
||||
|
||||
* Other, more specific, references
|
||||
|
||||
Alternatively, you may also like to reference these papers to
|
||||
|
|
@ -91,3 +90,11 @@ be more specific about a particular aspect of Spot.
|
|||
|
||||
For a while, this used to be the only paper presenting Spot as a
|
||||
model-checking library.
|
||||
|
||||
# LocalWords: utf html Alexandre Duret Lutz Lewkowicz Amaury Xu pdf
|
||||
# LocalWords: Fauchille Thibaud Michaud Etienne Proc ATVA LNCS TGBA
|
||||
# LocalWords: ltlfilt randltl ltlcross tgba Eddine Fabrice Kordon
|
||||
# LocalWords: Petri ToPNoC tgta Souheib Baarir LPAR Tomáš Babiak
|
||||
# LocalWords: František Blahoudek Joachim Křetínský Müller Strejček
|
||||
# LocalWords: CAV Maximilien Colange ltlsynt Christel Baier
|
||||
# LocalWords: Poitrenaud Volendam
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ greetings and the Spot version:
|
|||
|
||||
|
||||
To successfully compile this example program, we need a C++ compiler,
|
||||
obvisously. On this page, we are going to assume that you use =g++=
|
||||
obviously. On this page, we are going to assume that you use =g++=
|
||||
(version 7 or later), but other compilers like =clang++= share the
|
||||
same user interface. To successfully build the =hello= program, we
|
||||
might need to tell the compiler several things:
|
||||
|
|
@ -55,7 +55,7 @@ might need to tell the compiler several things:
|
|||
|
||||
In the likely case linking was made against the shared library
|
||||
=libspot.so=, the dynamic loader will have to locate =libspot.so=
|
||||
everytime the =hello= program is started, so this too might require
|
||||
every time the =hello= program is started, so this too might require
|
||||
some fiddling, for instance using the environment variable
|
||||
=LD_LIBRARY_PATH= if the library has not been installed in a standard
|
||||
location.
|
||||
|
|
@ -146,7 +146,7 @@ it every time you want to run a binary that depends on Spot.
|
|||
|
||||
* Case 4: You compiled Spot yourself, but did not install it
|
||||
|
||||
We do not recommand this, but it is possible to compile programs
|
||||
We do not recommend this, but it is possible to compile programs
|
||||
that uses an uninstalled version of Spot.
|
||||
|
||||
So you would just compile Spot in some directory (let's call it
|
||||
|
|
@ -178,7 +178,7 @@ There are at least two traps with this scenario:
|
|||
archive/ (some file with a =*.la= extension) that is an abstraction
|
||||
for a library (be it static, shared, or both), and its dependencies
|
||||
or options. During =make install=, these /Libtool archives/ are
|
||||
transformed into actuall shared or static libraries, installed and
|
||||
transformed into actual shared or static libraries, installed and
|
||||
configured properly. But since in this scenario =make install= is
|
||||
not run, you have to deal with the /Libtool archives/ directly.
|
||||
|
||||
|
|
@ -205,7 +205,7 @@ the desired result. See the [[http://www.gnu.org/software/libtool/manual/][GNU
|
|||
* Other libraries
|
||||
|
||||
If your program has to handle BDDs directly (for instance if you are
|
||||
[[file:tut22.org][creating an automaton]] explicitely), or if your system does not support
|
||||
[[file:tut22.org][creating an automaton]] explicitly), or if your system does not support
|
||||
one library requiring another, you will need to link with the =bddx=
|
||||
library. This should be as simple as adding =-lbddx= after =-lspot=
|
||||
in the first three cases.
|
||||
|
|
@ -234,8 +234,8 @@ will turn on assertions, and debugging options, while
|
|||
#+END_SRC
|
||||
will disable assertions and enable more optimizations.
|
||||
|
||||
If you are writing programs against Spot, we recommand to compile Spot
|
||||
with =--enable-devel= while your are developping your programs (the
|
||||
If you are writing programs against Spot, we recommend to compile Spot
|
||||
with =--enable-devel= while your are developing your programs (the
|
||||
assertions in Spot can be useful to diagnose problems in your program,
|
||||
or in Spot), and then use =--disable-devel= once you are confident and
|
||||
desire speed.
|
||||
|
|
@ -245,3 +245,7 @@ will default to =--disable-devel=.
|
|||
|
||||
Development versions (i.e., versions ending with a letter) default to
|
||||
=--enable-devel=.
|
||||
|
||||
# LocalWords: utf html args SRC nThis preprocessor libspot lspot LD
|
||||
# LocalWords: dev subdirectory sudo ldconfig ld usr Libtool libtool
|
||||
# LocalWords: portably gdb BDDs bddx lbddx libbddx Wextra Og devel
|
||||
|
|
|
|||
|
|
@ -496,7 +496,7 @@ formula. Everything here is case-sensitive.
|
|||
|
||||
#+BEGIN_SRC python :results verbatim raw :exports results
|
||||
import spot
|
||||
# org-mode recognize | as a table delemiter even in ~|~ or =|= but the
|
||||
# org-mode recognizes | as a table delimiter even in ~|~ or =|= but the
|
||||
# documented workaround to use \vert{} does not work in ~\vert{}~ or =\vert{}=.
|
||||
# So until we have a better solution, let's leave the =...= mode to display
|
||||
# \vert{} characters.
|
||||
|
|
@ -567,7 +567,7 @@ edge will have the same effect as forking the automaton to evaluate
|
|||
the rest of the word simultaneously from each universal destination.
|
||||
A run of an alternating automaton can therefore be pictured as a tree.
|
||||
The tree is accepting if all its branches satisfy the acceptance condition.
|
||||
(See the [[http://adl.github.io/hoaf/][Hanoi Omega-Automa format]] for more precise semantics.)
|
||||
(See the [[http://adl.github.io/hoaf/][Hanoi Omega-Automata format]] for more precise semantics.)
|
||||
|
||||
For instance the following alternating co-Büchi ω-automaton was
|
||||
generated by [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba 1.1.3=]] for the LTL formula =GF(a <-> Xb)=.
|
||||
|
|
@ -1033,7 +1033,7 @@ layers.
|
|||
built upon the =libspot= or =libspotgen= libraries
|
||||
- =libspotltsmin= is a library that helps interfacing Spot with
|
||||
dynamic libraries that [[http://fmt.cs.utwente.nl/tools/ltsmin/][LTSmin]] uses to represent state-spaces. It
|
||||
currently supports libraries generated from promela models using
|
||||
currently supports libraries generated from Promela models using
|
||||
SpinS or a patched version of DiVinE, but you have to install
|
||||
those third-party tools first. See [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/ltsmin/README][=tests/ltsmin/README=]]
|
||||
for details.
|
||||
|
|
@ -1163,3 +1163,17 @@ set right before the automaton is output. The notable exception is
|
|||
=product-states=, which is a property present in automata returned by
|
||||
=spot::product()= function in case it is necessary to know the origins
|
||||
of each state.
|
||||
|
||||
# LocalWords: utf html args ap ltl boolean automata ap BDD bdd BDDs
|
||||
# LocalWords: boolean acyclic subformulas Reif buchi BuDDy BDDs ap
|
||||
# LocalWords: ldots Minterms minterms Automata automata boolean bdd
|
||||
# LocalWords: minterms Automata automata buchi Büchi iff SRC ltl GF
|
||||
# LocalWords: tgba svg txt mathit Xb automata te hoa EOF autfilt ba
|
||||
# LocalWords: arg bdd Büchi iff buchi SRC ltl tgba GFa GFb autfilt
|
||||
# LocalWords: gba svg txt automata acc GF tba implem SRC Streett fi
|
||||
# LocalWords: dstar FGb twa ltlfilt neverclaim GFp tmp init od Bd
|
||||
# LocalWords: LBTT's lbtt LBT DRA Safra Sig ltldo FGp tl pdf psl
|
||||
# LocalWords: libbddx libspot libddx libspotgen libspotltsmin SpinS
|
||||
# LocalWords: LTSmin DiVinE ltsmin IPython Jupyter SCC SCCs trival
|
||||
# LocalWords: flagname newval degen dnf streett degeneralize const
|
||||
# LocalWords: aiger
|
||||
|
|
|
|||
|
|
@ -197,15 +197,15 @@ randltl -n 2 a b | ltlfilt --remove-wm |
|
|||
cat results.csv
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc"
|
||||
: "(1)","ltl2tgba -s %f >%N","ok",0,0.0247303,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,3994,1
|
||||
: "(1)","ltl3ba -f %s >%N","ok",0,0.00314673,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,3994,1
|
||||
: "(0)","ltl2tgba -s %f >%N","ok",0,0.0246916,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1
|
||||
: "(0)","ltl3ba -f %s >%N","ok",0,0.00343519,1,0,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1
|
||||
: "(!(G((F(b)) | (F(!((b) | (G(b))))))))","ltl2tgba -s %f >%N","ok",0,0.0233752,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1
|
||||
: "(!(G((F(b)) | (F(!((b) | (G(b))))))))","ltl3ba -f %s >%N","ok",0,0.00316933,1,0,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1
|
||||
: "(G((F(b)) | (F(!((b) | (G(b)))))))","ltl2tgba -s %f >%N","ok",0,0.0238983,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4083,1
|
||||
: "(G((F(b)) | (F(!((b) | (G(b)))))))","ltl3ba -f %s >%N","ok",0,0.00315896,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4083,1
|
||||
: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nondet_states","nondet_aut","complete_aut","product_states","product_transitions","product_scc"
|
||||
: "0","ltl2tgba -s %f >%N","ok",0,0.0447891,1,1,0,1,1,0,0,0,1,0,1
|
||||
: "0","ltl3ba -f %s >%N","ok",0,0.010318,1,0,0,1,1,0,0,0,1,0,1
|
||||
: "1","ltl2tgba -s %f >%N","ok",0,0.0448043,1,1,1,1,1,0,0,1,200,4199,1
|
||||
: "1","ltl3ba -f %s >%N","ok",0,0.0101865,1,1,1,1,1,0,0,1,200,4199,1
|
||||
: "!(F(!(b)))","ltl2tgba -s %f >%N","ok",0,0.0432052,1,1,1,1,1,0,0,0,200,2059,1
|
||||
: "!(F(!(b)))","ltl3ba -f %s >%N","ok",0,0.0103946,1,1,1,1,1,0,0,0,200,2059,1
|
||||
: "F(!(b))","ltl2tgba -s %f >%N","ok",0,0.043252,2,3,4,1,2,0,0,1,400,8264,2
|
||||
: "F(!(b))","ltl3ba -f %s >%N","ok",0,0.009877,2,3,4,1,2,0,0,1,400,8264,2
|
||||
|
||||
If we run =ltlfilt= on the first column, it will process the =formula=
|
||||
header as if it was an LTL formula.
|
||||
|
|
@ -285,3 +285,8 @@ cat result.csv
|
|||
: "!((F(p0)) -> ((!(p1)) U (p0)))","ltl2tgba","ok",0,0.0243147,3,5,10,1,3,2,1,0,0,0,0,1,0,0,0,0,598,10398,4,"HOA: v1 name: ""Fp0 & (p1 R !p0)"" States: 3 Start: 1 AP: 2 ""p1"" ""p0"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic stutter-invariant weak --BODY-- State: 0 {0} [t] 0 State: 1 [!0&!1] 1 [0&!1] 2 State: 2 [1] 0 [!1] 2 --END--"
|
||||
: "G((p0) -> (G(!(p1))))","ltl2tgba","ok",0,0.0201896,2,3,5,1,2,0,0,2,0,0,0,0,1,0,0,0,400,5025,2,"HOA: v1 name: ""G(!p0 | G!p1)"" States: 2 Start: 1 AP: 2 ""p0"" ""p1"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored deterministic stutter-invariant weak --BODY-- State: 0 {0} [!1] 0 State: 1 {0} [0&!1] 0 [!0] 1 --END--"
|
||||
: "!(G((p0) -> (G(!(p1)))))","ltl2tgba","ok",0,0.0194598,3,6,12,1,3,2,1,0,0,0,0,1,0,0,0,1,600,12354,3,"HOA: v1 name: ""F(p0 & Fp1)"" States: 3 Start: 1 AP: 2 ""p0"" ""p1"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete deterministic stutter-invariant terminal --BODY-- State: 0 [!1] 0 [1] 2 State: 1 [0&!1] 0 [!0] 1 [0&1] 2 State: 2 {0} [t] 2 --END--"
|
||||
|
||||
# LocalWords: utf CSV html args genltl randltl ltlfilt SRC gf csv
|
||||
# LocalWords: GFp tgba dstar autfilt randaut Fp Xa ltlcross abc GFa
|
||||
# LocalWords: GFb GFc GFd GFe wm ba acc scc nondet aut ok Fb Gb dac
|
||||
# LocalWords: Buchi nonacc
|
||||
|
|
|
|||
|
|
@ -183,7 +183,7 @@ The =dstar2tgba= tool implements a 4-step process:
|
|||
|
||||
1. read the automaton
|
||||
2. convert it into TGBA
|
||||
3. postprocess the resulting TGBA (simplifying the automaton, a degeneralizing it into a BA or Monitor if requested)
|
||||
3. post-process the resulting TGBA (simplifying the automaton, degeneralizing it into a BA or Monitor if requested)
|
||||
4. output the resulting automaton
|
||||
|
||||
BTW, the above scenario is also exactly what you get with [[file:autfilt.org][=autfilt=]] if
|
||||
|
|
@ -298,7 +298,7 @@ For instance here is a complex command that will
|
|||
- print it
|
||||
- then convert the formula into =ltl2dstar='s input format, process
|
||||
it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA
|
||||
transltor), and process the result with =dstar2tgba= to build a
|
||||
translator), and process the result with =dstar2tgba= to build a
|
||||
Büchi automaton (=-B=), favoring determinism if we can (=-D=),
|
||||
and finally displaying some statistics about this conversion.
|
||||
|
||||
|
|
@ -433,3 +433,10 @@ Sometimes, as in the [[#streett_to_tgba_example][example for =GFa & GFb=]] the o
|
|||
conversion happens to be deterministic. This is pure luck: Spot does
|
||||
not implement any algorithm to preserve the determinism of Streett
|
||||
automata.
|
||||
|
||||
# LocalWords: utf dstar tgba html args LBTT's dstar's Ds GFb DRA ba
|
||||
# LocalWords: fagfb ltlfilt SRC nba dsar DBA Acc Sig svg txt init
|
||||
# LocalWords: fi streett GFa gfafgb gfagfb degeneralizing sed sbacc
|
||||
# LocalWords: ouput lbtt GraphViz's SCCs hoaf neverclaim randltl wm
|
||||
# LocalWords: Sst sst det Fc Gc GFc Xc XXFc XFc Gb SCC CNF buchi et
|
||||
# LocalWords: Krishnan al vis Löding's cdot
|
||||
|
|
|
|||
|
|
@ -60,3 +60,6 @@ genaut --ks-nca=..5 --stats='%F=%L has %s states'
|
|||
: ks-nca=3 has 7 states
|
||||
: ks-nca=4 has 9 states
|
||||
: ks-nca=5 has 11 states
|
||||
|
||||
# LocalWords: utf genaut html args scalable SRC sed nca dsa nba svg
|
||||
# LocalWords: kscobuchi txt
|
||||
|
|
|
|||
|
|
@ -339,9 +339,9 @@ sb-patterns=27,p0 | (p1 U p0)
|
|||
#+end_example
|
||||
|
||||
Note that ~--sb-patterns=2 --sb-patterns=4 --sb-patterns=21..22~ also
|
||||
have their complement formula listed as ~--sb-patterns=3
|
||||
have their complement formulas listed as ~--sb-patterns=3
|
||||
--sb-patterns=8 --sb-patterns=23..24~. So if you build the set of
|
||||
formula output by =genltl --sb-patterns= plus its negation, it will
|
||||
formulas output by =genltl --sb-patterns= plus their negations, it will
|
||||
contain only 46 formulas, not 54.
|
||||
|
||||
#+BEGIN_SRC sh
|
||||
|
|
@ -356,3 +356,6 @@ genltl --sb --pos --neg | ltlfilt --uniq --count
|
|||
# LocalWords: ccj Xp XXp Xq XXq rv GFp lbt utf SETUPFILE html dac
|
||||
# LocalWords: Dwyer et al FMSP Etessami Holzmann sb Somenzi Bloem
|
||||
# LocalWords: CAV LaTeX Fq Fp pNN Gp XFp XF XGp FGp XG ltlfilt uniq
|
||||
# LocalWords: args fxg GFa GFan GFz xn gxf hkrss liberouter Holeček
|
||||
# LocalWords: kr DBA nlogn quasilinear kv Xb XXb XXXb FGa GFb beem
|
||||
# LocalWords: Pelánek sejk GFai GFbn FGb FGbn Sikert al's tv uu pos
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ supported by Spot). The combination of these allowed operators only
|
|||
makes it possible to express constraints on finite prefixes.
|
||||
|
||||
/Obligations/ can be thought of as Boolean combinations of /safety/
|
||||
and /guarentee/ properties, while /reactivity/ properties are Boolean
|
||||
and /guarantee/ properties, while /reactivity/ properties are Boolean
|
||||
combinations of /recurrence/ and /persistence/ properties. The
|
||||
negation of a /safety/ property is a /guarantee/ property (and
|
||||
vice-versa), and the same duality hold for /persistence/ and
|
||||
|
|
@ -182,7 +182,7 @@ The order given above actually starts with the easier checks first and
|
|||
keep the most complex tests at the end of the pipeline so they are
|
||||
applied to fewer formulas. Testing whether a formula is an LTL
|
||||
formula is very cheap, testing if a formula is an obligation is harder
|
||||
(it may involves a translation to automata and a poweset
|
||||
(it may involves a translation to automata and a powerset
|
||||
construction), and testing whether a formula is a recurrence is the
|
||||
most costly procedure (it involves a translation as well, plus
|
||||
conversion to deterministic Rabin automata, and an attempt to convert
|
||||
|
|
@ -518,7 +518,7 @@ language larger than that of the property.
|
|||
automata.
|
||||
|
||||
For the subclass of /obligation/ properties, using =-D= is a sure way
|
||||
to obain a deterministic automaton (and even a minimal one), but for
|
||||
to obtain a deterministic automaton (and even a minimal one), but for
|
||||
the /recurrence/ properties that are not /obligations/ the translator
|
||||
does not make /too much/ effort to produce deterministic automata,
|
||||
even with =-D= (this might change in the future).
|
||||
|
|
@ -666,7 +666,7 @@ The translator is aware of that, so when it detects that the input
|
|||
formula is a syntactic-persistence, it simplifies its translation
|
||||
slightly to ensure that the output will use at most one acceptance
|
||||
set. (It is possible to define a persistence properties using an LTL
|
||||
formula that is not a syntactic-persistance, in that case this
|
||||
formula that is not a syntactic-persistence, in that case this
|
||||
optimization is simply not applied.)
|
||||
|
||||
If the input is a weak property that is not syntactically weak, the
|
||||
|
|
@ -723,3 +723,10 @@ $txt
|
|||
[[file:hier-persistence-7.svg]]
|
||||
|
||||
That is indeed, a weak non-deterministic automaton.
|
||||
|
||||
# LocalWords: utf Pnueli html args PODC SCC subexpressions mathsf
|
||||
# LocalWords: SRC ltlfilt vw GOPRT randltl genltl ltlgrind Dwyers
|
||||
# LocalWords: et al FMSP dac uniq XFp psl Fb GF Gb FX GFb GXa wc tl
|
||||
# LocalWords: powerset pdf FGb Xa Xb FXa GFa Löding IPL Dax ATVA
|
||||
# LocalWords: tgba Löding's nondet hier oblig svg txt SCCs dstar
|
||||
# LocalWords: XFb ltldo streett DBA FGa varphi
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
#+PROPERTY: header-args:sh :results verbatim :exports both
|
||||
|
||||
|
||||
The [[http://adl.github.io/hoaf/][Hanoi Omega-Automa format]] is a textual representation of
|
||||
The [[http://adl.github.io/hoaf/][Hanoi Omega-Automata format]] is a textual representation of
|
||||
ω-automata labeled by Boolean formulas over a set of atomic
|
||||
propositions, and using an arbitrary acceptance condition. The
|
||||
typical acceptances conditions like Büchi, generalized-Büchi,
|
||||
|
|
@ -680,7 +680,7 @@ The above table is for version 1 of the format. When version 1.1 is
|
|||
selected (using =-H1.1=), some negated properties may be output. In
|
||||
particular, =stutter-sensitive= is replaced by =!stutter-invariant=.
|
||||
The logic of not cluttering the output with all of =!terminal=,
|
||||
=!weak=, and =!inhenrently-weak= is similar to the positive versions:
|
||||
=!weak=, and =!inherently-weak= is similar to the positive versions:
|
||||
=!inherently-weak= implies =!weak= which in turn implies =!terminal=,
|
||||
so only one of those is emitted unless =-Hv= is used.
|
||||
|
||||
|
|
@ -998,30 +998,6 @@ EOF
|
|||
autfilt decorate.hoa -d'.#'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: decorate
|
||||
#+begin_example
|
||||
digraph "" {
|
||||
rankdir=LR
|
||||
label=<t<br/>[all]>
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
node [style="filled", fillcolor="#ffffa0"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[fontsize=12] fontsize=12 stylesheet="spot.css" edge[arrowhead=vee, arrowsize=.7, fontsize=12]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 1
|
||||
0 [label=<0>]
|
||||
0 -> 0 [label=<1>, taillabel="#1", style=bold, color="#FF4DA0"]
|
||||
1 [label=<1>, style="bold,filled", color="#1F78B4"]
|
||||
1 -> 2 [label=<1>, taillabel="#2", style=bold, color="#FF7F00"]
|
||||
2 [label=<2>, style="bold,filled", color="#6A3D9A"]
|
||||
2 -> 0 [label=<b>, taillabel="#3"]
|
||||
2 -> 2 [label=<a & !b>, taillabel="#4"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file decorate.svg :var txt=decorate :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -1172,3 +1148,9 @@ State: 2 {0}
|
|||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f stvstracc.hoa sba.hoa stvstrlab.hoa decorate.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: html args Büchi accsets BDD SRC stvstracc EOF sed sba
|
||||
# LocalWords: acc Buchi Hm tgba GFa Fb encodings parametered ary Hk
|
||||
# LocalWords: bitsets randaut stvstrlab aut Hv hw bigwedge mathsf
|
||||
# LocalWords: genltl gf GFp Fp parser's rankdir br labelloc ffffa
|
||||
# LocalWords: fillcolor fontname svg txt Xa
|
||||
|
|
|
|||
|
|
@ -77,3 +77,6 @@ in any question (in English) or bug report without subscribing.
|
|||
|
||||
Our [[file:citing.org][citing page]] has a list of papers you could cite if you need to
|
||||
reference Spot in an academic publication.
|
||||
|
||||
# LocalWords: utf psl acc LBTT DSTAR Pnueli DBA SCCs ltlcross GPL
|
||||
# LocalWords: autcross LASTRELEASE LASTDATE Doxygen Jupyter IPython
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ Once the repository is set up, you can simply install Spot with:
|
|||
sudo dnf install spot python3-spot spot-devel spot-doc
|
||||
#+END_SRC
|
||||
or a subset of those packages. The package =spot= contains the
|
||||
command-line tools, =python3-spot= contains the Python bindinges,
|
||||
command-line tools, =python3-spot= contains the Python bindings,
|
||||
=spot-devel= contains the C++ header files, and =spot-doc= the
|
||||
documentation that you can also find online. Those packages depends
|
||||
on =libspot= that contains the shared libraries.
|
||||
|
|
@ -138,7 +138,7 @@ on =libspot= that contains the shared libraries.
|
|||
|
||||
The =master= branch of the git repository contains the code for the
|
||||
latest released version, possibly with a few yet-to-be-released
|
||||
bugfixes. The =next= branch is the main development branch, and contains
|
||||
bug fixes. The =next= branch is the main development branch, and contains
|
||||
the (working) code that should be part of the next major release.
|
||||
|
||||
To clone the git repository, use
|
||||
|
|
@ -151,3 +151,8 @@ This should put you on the =next= branch by default. From there, read
|
|||
the [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/HACKING][HACKING]] file that should be at the top of your cloned repository:
|
||||
it lists all the tools you should install before attempting to compile
|
||||
the source tree.
|
||||
|
||||
# LocalWords: utf html LASTRELEASE LASTTARBALL LASTNEWS dev sudo
|
||||
# LocalWords: libpython usr SRC README amd wget libspot GPG CFD pdf
|
||||
# LocalWords: FECF ipython libbddx libspotltsmin dnf config repo
|
||||
# LocalWords: lrde devel
|
||||
|
|
|
|||
|
|
@ -82,25 +82,6 @@ output by default)
|
|||
#+BEGIN_SRC sh :exports none
|
||||
ltl2tgba "Fa & GFb" -d
|
||||
#+END_SRC
|
||||
#+RESULTS: dotex
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 1
|
||||
0 [label="0"]
|
||||
0 -> 0 [label=<b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 -> 0 [label=<!b>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<a>]
|
||||
1 -> 1 [label=<!a>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file dotex.svg :var txt=dotex :exports results
|
||||
$txt
|
||||
|
|
@ -249,40 +230,6 @@ as above, for comparison.
|
|||
ltl2tgba -S 'GFa & GFb' -d
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: dotex2gba
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label=<0<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
||||
0 -> 0 [label=<a & b>]
|
||||
0 -> 1 [label=<!a & !b>]
|
||||
0 -> 2 [label=<!a & b>]
|
||||
0 -> 3 [label=<a & !b>]
|
||||
1 [label=<1>]
|
||||
1 -> 0 [label=<a & b>]
|
||||
1 -> 1 [label=<!a & !b>]
|
||||
1 -> 2 [label=<!a & b>]
|
||||
1 -> 3 [label=<a & !b>]
|
||||
2 [label=<2<br/><font color="#F17CB0">❶</font>>]
|
||||
2 -> 0 [label=<a & b>]
|
||||
2 -> 1 [label=<!a & !b>]
|
||||
2 -> 2 [label=<!a & b>]
|
||||
2 -> 3 [label=<a & !b>]
|
||||
3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 -> 0 [label=<a & b>]
|
||||
3 -> 1 [label=<!a & !b>]
|
||||
3 -> 2 [label=<!a & b>]
|
||||
3 -> 3 [label=<a & !b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -1060,7 +1007,7 @@ genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"'
|
|||
|
||||
Note that because no formula have been passed as argument to
|
||||
=ltl2tgba=, it defaulted to reading them from standard input. Such a
|
||||
behaviour can be requested explicitly with =-F -= if needed (e.g., to
|
||||
behavior can be requested explicitly with =-F -= if needed (e.g., to
|
||||
read from standard input in addition to processing other formula
|
||||
supplied with =-f=).
|
||||
|
||||
|
|
@ -1152,7 +1099,7 @@ page showing how to build them in Python and C++]].
|
|||
|
||||
Because Monitors accept every recognized run (in other words, they
|
||||
only reject words that are not recognized), it makes little sense to
|
||||
use option =-C= to request /complete/ monitors. If uou combine =-C=
|
||||
use option =-C= to request /complete/ monitors. If you combine =-C=
|
||||
with =-M=, the result will output as a Büchi automaton if (and only
|
||||
if) a sink state had to be added. For instance, here is the
|
||||
"complete" version of the previous monitor.
|
||||
|
|
@ -1178,5 +1125,8 @@ $txt
|
|||
# LocalWords: GraphViz's LBTT's neverclaim SPOT's init goto fi Gb
|
||||
# LocalWords: controled Gc gagbgc disjunction pre rewritings SCC Xa
|
||||
# LocalWords: WDBA determinize degeneralization satisfiability SCCs
|
||||
# LocalWords: genltl nondeterministic eval setenv concat getenv
|
||||
# LocalWords: setq
|
||||
# LocalWords: genltl nondeterministic eval setenv concat getenv DG
|
||||
# LocalWords: setq html args acc Buchi rankdir fontname Lato svg br
|
||||
# LocalWords: fillcolor ffffa vee arrowsize gba hoaf processings dp
|
||||
# LocalWords: ambig FGa fga fbgc fbgcfga determinized nosplit xltl
|
||||
# LocalWords: det scc simul FGb xdet P'min p'min p'max CSV iw
|
||||
|
|
|
|||
|
|
@ -112,4 +112,5 @@ Other Models of Concurrency (ToPNoC VI), LNCS 7400, p. 94--112, 2012.
|
|||
# LocalWords: Geldenhuys tgba SRC init invis nb Acc augb sed png fn
|
||||
# LocalWords: cmdline Tpng txt Büchi livelock gba gta GFa GFb TGTAs
|
||||
# LocalWords: gfagfb topnoc Eddine SALEM's ToPNoC LNCS eval setenv
|
||||
# LocalWords: concat getenv setq
|
||||
# LocalWords: concat getenv setq utf html args svg TGBAs Alexandre
|
||||
# LocalWords: Duret Lutz Fabrice Kordon Petri
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ Although =ltlcross= performs similar sanity checks as LBTT, it does
|
|||
not implement any of the interactive features of LBTT. In our almost
|
||||
10-year usage of LBTT, we never had to use its interactive features to
|
||||
understand bugs in our translation. Therefore =ltlcross= will report
|
||||
problems, maybe with a conterexample, but you will be on your own to
|
||||
problems, maybe with a counterexample, but you will be on your own to
|
||||
investigate and fix them (the =--grind= option may help you reduce the
|
||||
problem to a shorter formula).
|
||||
|
||||
|
|
@ -659,7 +659,7 @@ showing two automata for =a U b=, the first automaton is deterministic
|
|||
a nondeterministic state (state A2 has two possible successors for the
|
||||
assignment $ab$) and is therefore not deterministic.
|
||||
|
||||
If option =--aumbiguous= was passed to =ltlcross=, the column
|
||||
If option =--ambiguous= was passed to =ltlcross=, the column
|
||||
=ambiguous_aut= holds a Boolean indicating whether the automaton is
|
||||
ambiguous, i.e., if there exists a word that can be accepted by at
|
||||
least two different runs. (This information is not yet available for
|
||||
|
|
@ -1420,7 +1420,7 @@ No problem detected.
|
|||
into a =Makefile= that calls =ltlcross= for each of them.
|
||||
|
||||
For instance here is how to build a makefile called =ltlcross.mk=
|
||||
testing ltl2tgbaand ltl3ba against all formulas produced by
|
||||
testing =ltl2tgba= and =ltl3ba= against all formulas produced by
|
||||
=genltl --eh=, and gathering statistics from all runs in =all.csv=.
|
||||
|
||||
#+NAME: ltlcross.mk
|
||||
|
|
@ -1470,4 +1470,31 @@ rm -f results.csv results.json ltlcross.csv bogus-grind bogus ltlcross.mk
|
|||
# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO
|
||||
# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic
|
||||
# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq
|
||||
# LocalWords: setenv concat getenv
|
||||
# LocalWords: setenv concat getenv utf html args SCCs nonaccepting
|
||||
# LocalWords: dstar's lcr hvzgTC iYh nzjV rqfB OUNHEn qzVvdx eUfHTG
|
||||
# LocalWords: infixed LBT's dstar parsers MWei nba streett mv dst
|
||||
# LocalWords: Rabinizer MWRei rabinizer dra tela COMMANDFMT delag
|
||||
# LocalWords: da dgra dpa ldba untrusted ne UWmAOs UALknk JlcYb Yqa
|
||||
# LocalWords: vcaV jwQ eDh rE kjYd yDowOn zxU yf Dj NcC xUjPQ fD yl
|
||||
# LocalWords: OCI kdqA ZsPBds IxFTSb hRJ OAV yTDisN CUj lF xWC fx
|
||||
# LocalWords: aHi ATTR nondet aut ok degeneralized lor nonacc noweb
|
||||
# LocalWords: EOF genltl gizrt os LiBWmP ztzWmc DCyLpz MeEivW oXCj
|
||||
# LocalWords: APddNG un njT YNmfBO bGzWb rlrmnz KobkRW DFKnk IIcXH
|
||||
# LocalWords: sYE ypOBqt rJtfR qK stderr dt str SRC datatable chr
|
||||
# LocalWords: ok num acc scc nondet aut attr dcast SRC dt sep str
|
||||
# LocalWords: chr ok num acc scc nondet aut selfref attr chr tgba
|
||||
# LocalWords: dt SRC ltlcross svg ggplot aes abline colour hjust ba
|
||||
# LocalWords: randltl eval lbtt ltlgrind OTHERFILENAME Fb modella
|
||||
# LocalWords: lcr Nc CDjvYF LVv Sl EmhjSb GzR mwR gEcuQH UoNQx Qn
|
||||
# LocalWords: IDRd VDFaS bkvvTT wMAQUJ qoYoWz ILwXXp avS MYCa vJss
|
||||
# LocalWords: ItCKaM TG leC UXhs KwJJli kbRvp dups otaRtY bRLcyO GH
|
||||
# LocalWords: DMJCE gHu gKcHMk UPD HUKX Dpno xyO fx vxmn wgw sd vt
|
||||
# LocalWords: eA qHT qrbNOJ ceD Vz upQ EStxbg nUoj DgrW ohXyzM Vd
|
||||
# LocalWords: bozRHC wYkQs TCxOYi uWKDhZ OkfrP aEdRAF vy Kv lcfpVl
|
||||
# LocalWords: Hig Fc AvSorS AZkvCI Hd LNy pM tygKaf YHFrm GL iyV WD
|
||||
# LocalWords: riOaKL RHWB iVlf Xli Ez Gy BLLY nQYO efo bF fFzkpv MQ
|
||||
# LocalWords: FGa ltzvEc dqnX wmIXr yJesT HHyVWR scKnIH Wloux Rin
|
||||
# LocalWords: SCCs bh PHg LvvYEm bcUDEs Pw REy parallelization src
|
||||
# LocalWords: parallelize xargs findutils ltlfilt pnn formules mk
|
||||
# LocalWords: moreutils's Makefile makefile fread externalptr Gp XF
|
||||
# LocalWords: XFp XGp FGp GFp
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: =ltlfilt=
|
||||
#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting LTL formulas.
|
||||
#+DESCRIPTION: Spot command-line tool for filtering, transforming, and converting LTL formulas.
|
||||
#+INCLUDE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
#+PROPERTY: header-args:sh :results verbatim :exports both
|
||||
|
|
@ -159,7 +159,7 @@ ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c & a)' --relabel-bool=pnn
|
|||
: p0 & GFp0 & FGp1
|
||||
: p0 & p1 & GF(p0 & p1) & FG(p0 & p2)
|
||||
|
||||
In the first formula, the independent =a & !b= and =!c= subformulae
|
||||
In the first formula, the independent =a & !b= and =!c= subformulas
|
||||
were respectively renamed =p0= and =p1=. In the second formula, =a &
|
||||
!b= and =!c & a= are dependent so they could not be renamed; instead
|
||||
=a=, =!b= and =c= were renamed as =p0=, =p1= and =p2=.
|
||||
|
|
@ -595,4 +595,8 @@ rm -f ltlex.def ltlex.never scheck.ltl
|
|||
# LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck
|
||||
# LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc
|
||||
# LocalWords: pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb
|
||||
# LocalWords: XF XXa
|
||||
# LocalWords: XF XXa utf html args isop bool ap APs ltlf LTLf STR
|
||||
# LocalWords: subexpressions unabbreviate substring eFGiMRW eFGiMW
|
||||
# LocalWords: GF FG FGp hfe rdy req lup sr clk addr eq GFa XG Xc Xd
|
||||
# LocalWords: subexpression ba neverclaim ltlex init fi ltldo siPSL
|
||||
# LocalWords: subformula FXb FX CSV vw Pnueli LaTeX wc
|
||||
|
|
|
|||
|
|
@ -90,3 +90,4 @@ argument.
|
|||
|
||||
# LocalWords: ltlgrind num toc html ltlcross FILENAME SRC sed ap Gb
|
||||
# LocalWords: const multop multops unary decrement disjunction Gc
|
||||
# LocalWords: utf args
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ The output is composed of two parts:
|
|||
- the first one is a single line REALIZABLE or UNREALIZABLE;
|
||||
- the second one is an automaton describing the controller (if the input
|
||||
specification is realizable). In this example, the controller has a single
|
||||
state, with two loops labelled by =a & b & c= and =(!a | !b) & !c=.
|
||||
state, with two loops labeled by =a & b & c= and =(!a | !b) & !c=.
|
||||
|
||||
If a controller exists, then one with finite memory exists. Such controllers
|
||||
are easily represented as automata (or more specifically as I/O automata or
|
||||
|
|
@ -107,3 +107,8 @@ You can also ask =ltlsynt= to print to obtained parity game into
|
|||
[[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag
|
||||
=--print-pg=. Note that this flag deactivates the resolution of the parity
|
||||
game, which is to be deferred to one of the solvers from PGSolver.
|
||||
|
||||
# LocalWords: utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF
|
||||
# LocalWords: UNREALIZABLE unrealizable SYNTCOMP realizability Proc
|
||||
# LocalWords: syfco ltlxba Zielonka's Thibaud Michaud Maximilien
|
||||
# LocalWords: Colange PGSolver
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ Details about supported features of the HOA format can be found on a
|
|||
|
||||
The [[http://adl.github.io/hoaf/][HOA]] output should be the preferred format to use if you want to
|
||||
pass automata between different tools. Since Spot 1.99.7, it is the
|
||||
default output format, but you can explicitely request it using the
|
||||
default output format, but you can explicitly request it using the
|
||||
=-H= parameter and this allows passing additional options to the HOA
|
||||
printer.
|
||||
|
||||
|
|
@ -453,12 +453,12 @@ of the default horizontal layout), =c= requests circle states, =s=
|
|||
causes strongly-connected components to be displayed, =n= causes the
|
||||
name (see below) of the automaton to be displayed, and =a= causes the
|
||||
acceptance condition to be shown as well. Option =b= causes sets to
|
||||
be ouput as bullets (e.g., ⓿ instead of ={0}=); option =r= (for
|
||||
be output as bullets (e.g., ⓿ instead of ={0}=); option =r= (for
|
||||
rainbow) causes sets to be displayed in different colors, while option
|
||||
=R= also uses colors, but it chooses them depending on whether a set
|
||||
is used with Fin-acceptance, Inf-acceptance, or both. Option
|
||||
=C(COLOR)= can be used to color all states using =COLOR=, and the
|
||||
option =f(FONT)= is used to select a fontname: it is often necessary
|
||||
option =f(FONT)= is used to select a font name: it is often necessary
|
||||
when =b= is used to ensure the characters ⓿, ❶, etc. are all selected
|
||||
from the same font.
|
||||
|
||||
|
|
@ -623,7 +623,7 @@ Caveats:
|
|||
compute the size of each label before calling GraphViz to layout the
|
||||
graph. This is because GraphViz cannot compute the correct size of
|
||||
mathematical formulas. Unfortunately, the release of =dot2tex
|
||||
2.9.0= contains a bug where sizes are intepreted as integers instead
|
||||
2.9.0= contains a bug where sizes are interpreted as integers instead
|
||||
of floats. This can cause labels or shapes to disappear. This bug
|
||||
of =dot2tex= was fixed in 2014, but at the time of writing
|
||||
(summer 2017) no new release of =dot2tex= has been made. To work around this,
|
||||
|
|
@ -649,7 +649,7 @@ Most tools support a common set of statistics about the output
|
|||
automaton (like =%s= for the number of states, =%t= for transitions,
|
||||
=%e= for edges, etc.). Additional statistics might be available
|
||||
depending on what the tool does (for instance [[file:autfilt.org][=autfilt=]] also uses
|
||||
capitaized letters =%S=, =%T=, and =%E= to display the same statistics
|
||||
capitalized letters =%S=, =%T=, and =%E= to display the same statistics
|
||||
about the input automaton). All the available statistics are
|
||||
displayed when a tool is run with =--help=.
|
||||
|
||||
|
|
@ -760,7 +760,7 @@ genltl --or-gf=1..8 | ltl2tgba --high --stats='%f,%r,%R'
|
|||
: GF(p1 | p2 | p3 | p4 | p5 | p6 | p7 | p8),0.480063,0.48
|
||||
|
||||
Note that =%r= is implemented using the most precise clock available
|
||||
and usually has nano-second precision, while =%R= uses the =times()=
|
||||
and usually has nanosecond precision, while =%R= uses the =times()=
|
||||
system call (when available) and is usually only precise up to 1/100
|
||||
of a second. However, as a wall-clock time, =%r= will also be
|
||||
affected by the load of the machine: if a machine is overloaded, or
|
||||
|
|
@ -950,4 +950,9 @@ rm -f out-det0.hoa out-det1.hoa
|
|||
# LocalWords: labelloc rankdir subgraph lp pos invis gv png cmdline
|
||||
# LocalWords: Tpng txt Hs Hm CSV Htl LBT dstar init goto fi Tpdf XF
|
||||
# LocalWords: oaut vcsn randaut nondeterministic filename csv hoa
|
||||
# LocalWords: varphi lnot GFb FG
|
||||
# LocalWords: varphi lnot GFb FG args SRC Büchi rEctangular svg GFa
|
||||
# LocalWords: FGa od DOTEXTRA DOTDEFAULT pdf Tsvg vcsna cas EOF xyz
|
||||
# LocalWords: vcsnA Brf Lato ffffa vee arrowsize tex neato circo mv
|
||||
# LocalWords: LaTeX TikZ PSTricks formater autosize nominsize tmp
|
||||
# LocalWords: latexmk sbarx cd sudo py iw dges tates Rscript genltl
|
||||
# LocalWords: gf GFp nano ltldo tba randltl det
|
||||
|
|
|
|||
|
|
@ -65,11 +65,12 @@ $txt
|
|||
|
||||
* Acceptance condition
|
||||
|
||||
The generation of the acceptance sets abn is controlled with the following four parameters:
|
||||
The generation of the acceptance condition and acceptance sets is
|
||||
controlled with the following four parameters:
|
||||
|
||||
- =-A ACCEPTANCE= (or =--acceptance=ACCEPTANCE=) controls both the acceptance condition,
|
||||
and the number of associated acceptance sets. The =ACCEPTANCE= argument is documented
|
||||
in =--help= as follows:
|
||||
- =-A ACCEPTANCE= (or =--acceptance=ACCEPTANCE=) controls both the
|
||||
acceptance condition, and the number of associated acceptance sets.
|
||||
The =ACCEPTANCE= argument is documented in =--help= as follows:
|
||||
#+BEGIN_SRC sh :exports results
|
||||
randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p'
|
||||
#+END_SRC
|
||||
|
|
@ -99,7 +100,7 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p'
|
|||
|
||||
#+end_example
|
||||
|
||||
When a range of the form $i..j$ is used, the actual value is taken as randomly
|
||||
When a range of the form $i..j$ is used, the actual value is taken randomly
|
||||
between $i$ and $j$ (included).
|
||||
|
||||
- =-a= (or =--acc-probability=) controls the probability that any
|
||||
|
|
@ -137,30 +138,6 @@ $txt
|
|||
randaut -Q3 -e0.4 -B -a0.7 2 --dot
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: randaut5
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 1 [label=<!p0 & !p1>]
|
||||
0 -> 2 [label=<!p0 & !p1>]
|
||||
1 [label="1", peripheries=2]
|
||||
1 -> 1 [label=<!p0 & !p1>]
|
||||
1 -> 0 [label=<p0 & p1>]
|
||||
2 [label="2", peripheries=2]
|
||||
2 -> 0 [label=<p0 & p1>]
|
||||
2 -> 2 [label=<p0 & !p1>]
|
||||
2 -> 1 [label=<!p0 & !p1>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file randaut5.svg :var txt=randaut5 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -237,7 +214,7 @@ automatically implies =--ba=.
|
|||
|
||||
Automata are send to standard output by default, by you can use =-o=
|
||||
to give a filename, or even a pattern for filenames. For instance the
|
||||
following generates 20 automatas, but store them in different files
|
||||
following generates 20 automata, but store them in different files
|
||||
according to the acceptance condition. The format =%g= represent the
|
||||
formula for the acceptance condition and would not make a nice
|
||||
filename, but =%[s]g= is a short name for that acceptance condition
|
||||
|
|
@ -300,3 +277,7 @@ $txt
|
|||
|
||||
You should be able to find each of the expected type of SCCs in the above picture.
|
||||
The green rectangles mark the three SCCs that contain some accepting cycles.
|
||||
|
||||
# LocalWords: utf randaut html args SRC svg txt randltl sed Buchi
|
||||
# LocalWords: acc ba rankdir hoaf lbtt Hl wc rautaut SCCs SCC sccs
|
||||
# LocalWords: A'parity
|
||||
|
|
|
|||
|
|
@ -341,4 +341,5 @@ non-length-matching variant of the =and= operator.
|
|||
# LocalWords: Xc GFb Gc Xb Fb XFb Xa dups ltlfilt Fc XXc GX GFc XG
|
||||
# LocalWords: rewritings ltl ap GF ANDed GFa boolean EConcat eword
|
||||
# LocalWords: UConcat boolform andNLM concat Kleen eval setenv setq
|
||||
# LocalWords: getenv
|
||||
# LocalWords: getenv html args FGb nonnegative Fp FGp xargs LaTeX
|
||||
# LocalWords: FGc subformula GXb fstar
|
||||
|
|
|
|||
|
|
@ -294,7 +294,7 @@ The following options can be used to fine-tune this procedure:
|
|||
where is the difference? They both start by encoding the research of the
|
||||
=N-1= step and then:
|
||||
- =2= uses PicoSAT assumptions. It adds =sat-incr-steps= assumptions
|
||||
(each of them removing one more state) and then checks direclty the
|
||||
(each of them removing one more state) and then checks directly the
|
||||
=N-1-(sat-incr-steps)= step. If such automaton is found, the process is
|
||||
restarted. Otherwise, a binary search begins between =N-1= and
|
||||
=N-1-sat-incr-steps=. If not provided, =sat-incr-steps= default value
|
||||
|
|
@ -307,7 +307,7 @@ The following options can be used to fine-tune this procedure:
|
|||
- =-x sat-minimize=4= :: enable SAT-based minimization. It tries to reduce the
|
||||
size of the automaton one state at a time. This option implies
|
||||
=-x tba-det=.
|
||||
- =-x sat-incr-steps=N= :: set the value of =sat-incr-steps= to N. It doest not
|
||||
- =-x sat-incr-steps=N= :: set the value of =sat-incr-steps= to N. It does not
|
||||
make sense to use it without =-x sat-minimize=2= or =-x sat-minimize=3=.
|
||||
- =-x sat-acc=$m$= :: attempt to build a minimal DTGBA with $m$ acceptance sets.
|
||||
This options implies =-x sat-minimize=.
|
||||
|
|
@ -497,7 +497,7 @@ The =--sat-minimize= option takes a comma separated list of arguments
|
|||
that can be any of the following:
|
||||
|
||||
- =acc=DOUBLEQUOTEDSTRING= :: where the =DOUBLEQUOTEDSTRING= is an
|
||||
acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA syntax]], or a parametrized acceptance
|
||||
acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA syntax]], or a parameterized acceptance
|
||||
name (the different [[http://adl.github.io/hoaf/#acceptance-specifications][=acc-name:= options from HOA]]).
|
||||
- =max-states=N= :: where =N= is an upper-bound on the maximum
|
||||
number of states of the constructed automaton.
|
||||
|
|
@ -515,7 +515,7 @@ that can be any of the following:
|
|||
starting automaton. Now, where is the difference? They both start by
|
||||
encoding the research of the =N-1= step and then:
|
||||
- =1= uses PicoSAT assumptions. It adds =steps= assumptions (each of
|
||||
them removing one more state) and then checks direclty the
|
||||
them removing one more state) and then checks directly the
|
||||
=N-1-(sat-incr-steps)= step. If such automaton is found, the process is
|
||||
restarted. Otherwise, a binary search begins between =N-1= and
|
||||
=N-1-sat-incr-steps=. If not provided, =sat-incr-steps= defaults to 6.
|
||||
|
|
@ -645,3 +645,10 @@ rm -f output.hoa output2.hoa
|
|||
* Python interface
|
||||
|
||||
See the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] notebook.
|
||||
|
||||
# LocalWords: utf html args SRC tgba dstar DTBA DT PicoSAT LPAR GF
|
||||
# LocalWords: unminimized SATSOLVER det tba degeneralized gfaexxb
|
||||
# LocalWords: svg txt BD ltlfilt DRA wm nba acc arg ltldo DBA WDBA
|
||||
# LocalWords: SCC TCONG powerset incr DTGBA wdba FGa FGb autfiltsm
|
||||
# LocalWords: Buchi GFa GFb DOUBLEQUOTEDSTRING langmap SATLOG csv
|
||||
# LocalWords: src sed sys satmin ipynb
|
||||
|
|
|
|||
|
|
@ -90,3 +90,7 @@ real notebooks instead.
|
|||
- [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties.
|
||||
- [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]].
|
||||
- [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][=twagraph-internals.ipynb=]] Inner workings of the =twa_graph= class.
|
||||
|
||||
# LocalWords: utf html bdd IPython ipynb io randaut accparse acc
|
||||
# LocalWords: cond randltl genltl genaut scc testingaut ltsmin dve
|
||||
# LocalWords: DiVinE LTSmin pml twa atva inv satmin twagraph
|
||||
|
|
|
|||
|
|
@ -463,3 +463,8 @@ _formula_format(self, spec)
|
|||
formating function for strings.
|
||||
|
||||
#+end_example
|
||||
|
||||
# LocalWords: utf html args ltlfilt LBT lbt SRC GFp FGp LBT's str
|
||||
# LocalWords: parenth parsers stex iostream psl superset nullptr GF
|
||||
# LocalWords: subformulas simplifier simp sp lq CSV formatspec
|
||||
# LocalWords: LaTeX formating
|
||||
|
|
|
|||
|
|
@ -155,3 +155,7 @@ ltlfilt -ps --relabel-bool=pnn --define -f 'a U (a & b)'
|
|||
This "Boolean sub-expression" relabeling is available in Python and
|
||||
C++ via the =relabel_bse= function. The interface is identical to
|
||||
=relabel=.
|
||||
|
||||
# LocalWords: utf html args renamings SRC ltlfilt ps pnn ba prepend
|
||||
# LocalWords: tmp defs init fi ltldo newname oldname str iostream
|
||||
# LocalWords: abc Abc bool bse
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ constructors for each supported operator.
|
|||
The Boolean constants true and false are returned by =formula::tt()=
|
||||
and =formula:ff()=. Atomic propositions can be built with
|
||||
=formula::ap("name")=. Unary and binary operators use a
|
||||
straighforward syntax like =formula::F(arg)= or =formula::U(first,
|
||||
straightforward syntax like =formula::F(arg)= or =formula::U(first,
|
||||
second)=, while n-ary operators take an initializer list as argument
|
||||
as in =formula::And({arg1, arg2, arg3})=.
|
||||
|
||||
|
|
@ -48,7 +48,7 @@ Here is the list of supported operators:
|
|||
formula::G(arg, min, max); // G[min..max] arg
|
||||
formula::Closure(arg);
|
||||
formula::NegClosure(arg);
|
||||
formula::first_match(arg); // SVA's first match opetaror
|
||||
formula::first_match(arg); // SVA's first match operator
|
||||
// binary operators
|
||||
formula::Xor(left, right);
|
||||
formula::Implies(left, right);
|
||||
|
|
@ -485,3 +485,8 @@ Here is the =F= and =G= exchange:
|
|||
|
||||
Like in C++, extra arguments to =map= and =traverse= are passed as
|
||||
additional to the function given in the first argument.
|
||||
|
||||
# LocalWords: utf html args accessor Unary arg ary initializer SRC
|
||||
# LocalWords: unary SVA's tl pdf subformulas subformula memoization
|
||||
# LocalWords: iostream FGa GFb GFc fga gfb gfc kindstar kindstr DFS
|
||||
# LocalWords: enum subtrees gcount cpp GF Fb xchg fg GFa FGb countg
|
||||
|
|
|
|||
|
|
@ -132,3 +132,5 @@ int main()
|
|||
|
||||
#+RESULTS:
|
||||
: Equivalent
|
||||
|
||||
# LocalWords: utf html args ltlfilt SRC eq lnot otimes ng iostream
|
||||
|
|
|
|||
|
|
@ -215,3 +215,6 @@ translate(formula, *args, dict=<spot.impl.bdd_dict; proxy of <Swig Object of typ
|
|||
so check out the spot-x(7) man page for details.
|
||||
|
||||
#+end_example
|
||||
|
||||
# LocalWords: utf html args SRC tgba GFa GFb init fi str aut xargs
|
||||
# LocalWords: coBuchi StateBasedAcceptance SBAcc
|
||||
|
|
|
|||
|
|
@ -284,3 +284,7 @@ If your application requires monitors and you plan to build them with
|
|||
Spot, it is very likely that you will want to convert the resulting
|
||||
automata to your own data structure. See [[file:tut21.org][how to print an automaton in
|
||||
a custom format]] to learn all you need to iterate over Spot's automata.
|
||||
|
||||
# LocalWords: utf html args SRC tgba Xyellow svg txt acc det str
|
||||
# LocalWords: aut monitorable ltlfilt d'Amorim Roşu CAV Tabakov DFA
|
||||
# LocalWords: Vardi SystemC SCCs determinize powerset
|
||||
|
|
|
|||
|
|
@ -240,7 +240,7 @@ perform some LTLf model checking, you should stop at step 3. Keep the
|
|||
=alive= proposition in your property automaton, and also add it to the
|
||||
Kripke structure representing your system.
|
||||
|
||||
Alternatively, if your Kripke structure is already equiped with some
|
||||
Alternatively, if your Kripke structure is already equipped with some
|
||||
=dead= property (as introduced by default in our [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin= interface]]),
|
||||
you could replace =alive= by =!dead= by using ~ltlfilt
|
||||
--from-ltl="!dead"~ (from the command-line), a running
|
||||
|
|
@ -255,3 +255,7 @@ operator:
|
|||
- The strong next: =X[!] a= is true if =a= hold in the next step *and*
|
||||
there must be a next step. In particular =X[!]1= asserts that
|
||||
there is a successor.
|
||||
|
||||
# LocalWords: utf LTLf html args ltlf src ltlfilt Fc tgba svg txt
|
||||
# LocalWords: ap De Giacomo Vardi IJCAI Dutta Memocode acc Buchi ba
|
||||
# LocalWords: postprocess aut det str NFA DFA ltsmin iff
|
||||
|
|
|
|||
|
|
@ -213,7 +213,7 @@ can be specified if needed.
|
|||
There are actually different C++ interfaces to the automaton parser,
|
||||
depending on your use case. For instance the parser is able to read a
|
||||
stream of automata stored in the same file, so that they could be
|
||||
processed in a loop. For this, you would instanciate a
|
||||
processed in a loop. For this, you would instantiate a
|
||||
=spot::automaton_stream_parser= object and call its =parse()= method
|
||||
in a loop. Each call to this method will either return one
|
||||
=spot::parsed_aut_ptr=, or =nullptr= if there is no more automaton to
|
||||
|
|
@ -319,3 +319,6 @@ State: 1 {0}
|
|||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f tut20.never
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args SRC init od LBTT's dstar's acc Buchi fi
|
||||
# LocalWords: str lbtt aut BDDs bdd ptr nullptr
|
||||
|
|
|
|||
|
|
@ -562,7 +562,7 @@ Here is the very same example, but written in Python:
|
|||
for t in aut.out(s):
|
||||
print(" edge({} -> {})".format(t.src, t.dst))
|
||||
# bdd_print_formula() is designed to print on a std::ostream, and
|
||||
# is inconveniant to use in Python. Instead we use
|
||||
# is inconvenient to use in Python. Instead we use
|
||||
# bdd_format_formula() as this simply returns a string.
|
||||
print(" label =", spot.bdd_format_formula(bdict, t.cond))
|
||||
print(" acc sets =", t.acc)
|
||||
|
|
@ -848,3 +848,7 @@ State 16:
|
|||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f tut21.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args mathit src dst cond accsets tgba Fb Fc
|
||||
# LocalWords: acc Buchi BDDs bdd ap ithvar aut const num init bdict
|
||||
# LocalWords: varnum sep Templated
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ automata in Spot.
|
|||
// States are numbered from 0.
|
||||
aut->new_states(3);
|
||||
// The default initial state is 0, but it is always better to
|
||||
// specify it explicitely.
|
||||
// specify it explicitly.
|
||||
aut->set_init_state(0U);
|
||||
|
||||
// new_edge() takes 3 mandatory parameters: source state,
|
||||
|
|
@ -109,7 +109,7 @@ State: 2
|
|||
# States are numbered from 0.
|
||||
aut.new_states(3)
|
||||
# The default initial state is 0, but it is always better to
|
||||
# specify it explicitely.
|
||||
# specify it explicitly.
|
||||
aut.set_init_state(0)
|
||||
|
||||
# new_edge() takes 3 mandatory parameters: source state, destination state,
|
||||
|
|
@ -202,7 +202,7 @@ whenever possible".
|
|||
// States are numbered from 0.
|
||||
aut->new_states(3);
|
||||
// The default initial state is 0, but it is always better to
|
||||
// specify it explicitely.
|
||||
// specify it explicitly.
|
||||
aut->set_init_state(0U);
|
||||
|
||||
// new_edge() takes 3 mandatory parameters: source state,
|
||||
|
|
@ -267,7 +267,7 @@ State: 2
|
|||
# States are numbered from 0.
|
||||
aut.new_states(3)
|
||||
# The default initial state is 0, but it is always better to
|
||||
# specify it explicitely.
|
||||
# specify it explicitly.
|
||||
aut.set_init_state(0)
|
||||
|
||||
# new_edge() takes 3 mandatory parameters: source state, destination state,
|
||||
|
|
@ -405,3 +405,6 @@ State: 2
|
|||
[0 | 1] 1 {0 2}
|
||||
--END--
|
||||
#+end_SRC
|
||||
|
||||
# LocalWords: utf html args SRC tgba TGBAs cpp bdd aut twa ap buchi
|
||||
# LocalWords: ithvar init acc bdict BuDDy str sba setacc cond
|
||||
|
|
|
|||
|
|
@ -61,7 +61,7 @@ edges (declared with =new_edge()=) and universal edges (declared with
|
|||
// States are numbered from 0.
|
||||
aut->new_states(3);
|
||||
// The default initial state is 0, but it is always better to
|
||||
// specify it explicitely.
|
||||
// specify it explicitly.
|
||||
aut->set_init_state(0U);
|
||||
|
||||
// new_edge() takes 3 mandatory parameters: source state,
|
||||
|
|
@ -128,7 +128,7 @@ State: 2
|
|||
# States are numbered from 0.
|
||||
aut.new_states(3)
|
||||
# The default initial state is 0, but it is always better to
|
||||
# specify it explicitely.
|
||||
# specify it explicitly.
|
||||
aut.set_init_state(0);
|
||||
|
||||
# new_edge() takes 3 mandatory parameters: source state, destination state,
|
||||
|
|
@ -181,3 +181,6 @@ alternating automaton.
|
|||
Once you have built an alternating automaton, you can [[file:tut31.org][remove the
|
||||
alternation]] to obtain a non-deterministic Büchi or generalized Büchi
|
||||
automaton.
|
||||
|
||||
# LocalWords: utf html args GFa SRC txt cpp EOF aut svg bdd twa ap
|
||||
# LocalWords: ithvar init bddtrue acc Buchi bdict BuDDy str
|
||||
|
|
|
|||
|
|
@ -239,3 +239,8 @@ State 2:
|
|||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f tut24.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args noweb SRC acc Buchi EOF svg txt aut num
|
||||
# LocalWords: nonalt init const src dst cond dest aut init dst SRC
|
||||
# LocalWords: dests nonalt num src cond acc noweb bdict ui str ud
|
||||
# LocalWords: bdd
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ any acceptance to Büchi acceptance.
|
|||
We use =autfilt= with option =-B= to request Büchi acceptance and
|
||||
state-based output and =-D= to express a preference for deterministic
|
||||
output. Using option =-D/--deterministic= (or =--small=) actually
|
||||
activates the "postprocessing" routines of Spot: the acceptance will
|
||||
activates the "post-processing" routines of Spot: the acceptance will
|
||||
not only be changed to Büchi, but simplification routines (useless
|
||||
SCCs removal, simulation-based reductions, acceptance sets
|
||||
simplifications, WDBA-minimization, ...) will also be applied.
|
||||
|
|
@ -84,7 +84,7 @@ $txt
|
|||
|
||||
In the general case transforming an automaton with a complex
|
||||
acceptance condition into a Büchi automaton can make the output
|
||||
bigger. However the postprocessing routines may manage to simplify
|
||||
bigger. However the post-processing routines may manage to simplify
|
||||
the result further.
|
||||
|
||||
|
||||
|
|
@ -139,7 +139,7 @@ Help on function postprocess in module spot:
|
|||
postprocess(automaton, *args, formula=None, xargs=None)
|
||||
Post process an automaton.
|
||||
|
||||
This applies a number of simlification algorithms, depending on
|
||||
This applies a number of simplification algorithms, depending on
|
||||
the options supplied. Keep in mind that 'Deterministic' expresses
|
||||
just a preference that may not be satisfied if the input is
|
||||
not already 'Deterministic'.
|
||||
|
|
@ -234,3 +234,7 @@ State: 4
|
|||
#+BEGIN_SRC sh :results silent
|
||||
rm -f tut30.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args dstar SRC ltldo Xp XXp svg txt SCCs acc
|
||||
# LocalWords: WDBA Buchi postprocess aut str xargs TGBA coBuchi
|
||||
# LocalWords: StateBasedAcceptance SBAcc postprocessor
|
||||
|
|
|
|||
|
|
@ -174,3 +174,6 @@ State: 1
|
|||
#+BEGIN_SRC sh :results silent
|
||||
rm -f tut31.hoa
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html args SRC acc Buchi noweb EOF svg txt SCCs
|
||||
# LocalWords: TGBA tgba aut str
|
||||
|
|
|
|||
|
|
@ -214,7 +214,7 @@ syntax of C++ works exactly as if we had typed
|
|||
|
||||
In the above =example()= function, the iterators =i= and =end= are
|
||||
instances of the =internal::edge_iterator<spot::twa_graph::graph_t>=
|
||||
class, which redefines enough operators to act like an STL Foward
|
||||
class, which redefines enough operators to act like an STL Forward
|
||||
Iterator over all outgoing edges of =s=. Note that the =tmp= and =i=
|
||||
objects hold a pointer to the graph, but it does not really matter
|
||||
because the compiler will optimize this away.
|
||||
|
|
@ -444,7 +444,7 @@ the entire automaton in memory; if they prefer, they can compute it as
|
|||
it is explored.
|
||||
|
||||
Naturally =twa_graph=, even if it stores the automaton graph
|
||||
explicitly, is a subclasse of =twa=, so it also implements the
|
||||
explicitly, is a subclass of =twa=, so it also implements the
|
||||
on-the-fly interface but without computing anything.
|
||||
|
||||
** How this interface works
|
||||
|
|
@ -889,3 +889,8 @@ print it.
|
|||
: 1->1
|
||||
: 0->2
|
||||
: 2->2
|
||||
|
||||
# LocalWords: utf html args twa twagraph ipynb SRC plantuml uml svg
|
||||
# LocalWords: stl bool src dst succ distate typedef bdd ptr init
|
||||
# LocalWords: cond acc aut FGa FGb tmp inlined DFS dfs num ish todo
|
||||
# LocalWords: Subclasses otf iterable iter emplace srcit
|
||||
|
|
|
|||
|
|
@ -593,5 +593,5 @@ class, used to build on-the-fly product.
|
|||
# LocalWords: nondeterministicaly kripke succ plantuml uml png iter
|
||||
# LocalWords: bdd ptr const init bool dst cond acc pos ithvar ap ss
|
||||
# LocalWords: xodd yodd str nullptr noweb cmdline Tpng cmd circo GF
|
||||
# LocalWords: txt LTL af preallocated deallocation destructor
|
||||
# LocalWords: unicity
|
||||
# LocalWords: txt LTL af preallocated deallocation destructor svg
|
||||
# LocalWords: unicity kA src cpp tooltip
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ memory.
|
|||
|
||||
Our Kripke structure represent a model whose states consist of pairs
|
||||
of modulo-3 integers $(x,y)$. At any state the possible actions
|
||||
will be to increment any one of the two integer (nondeterministicaly).
|
||||
will be to increment any one of the two integers (nondeterministically).
|
||||
That increment is obviously done modulo 3. For instance state $(1,2)$
|
||||
has two possible successors:
|
||||
- $(2,2)$ if =x= was incremented, or
|
||||
|
|
@ -303,3 +303,6 @@ read the C++ description for details.
|
|||
#+BEGIN_SRC text :noweb yes
|
||||
<<demo-2py()>>
|
||||
#+END_SRC
|
||||
|
||||
# LocalWords: utf html kripke SRC bool bdd ithvar ap init noweb svg
|
||||
# LocalWords: GraphViz's cmd circo txt GF af py bdddict ns str
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ automata agree on the BDD variables used to represent $a$ and $b$.
|
|||
The =spot::bdd_dict= object is in charge of allocating BDD variables,
|
||||
and ensuring that multiple users reuse the same variables for similar
|
||||
purpose. When a =twa_graph= automaton is constructed, it takes a
|
||||
=bdd_dict= as argument. Everytime an atomic proposition is
|
||||
=bdd_dict= as argument. Every time an atomic proposition is
|
||||
registered through the =twa::register_ap()= method, the =bdd_dict=
|
||||
is queried.
|
||||
|
||||
|
|
@ -445,3 +445,8 @@ variables *anonymous* because their meaning is unknown the the
|
|||
|
||||
#+RESULTS:
|
||||
: [(0, 2), (0, 3), (1, 0), (1, 1), (2, 2), (2, 3), (3, 0), (3, 1)]
|
||||
|
||||
# LocalWords: utf bdd html args BDDs DAGs twa SRC aut ap bff src
|
||||
# LocalWords: unregisters unregister dest init dst str num cond GF
|
||||
# LocalWords: noweb XXa RuntimeError del v'i anonbase bddfalse isop
|
||||
# LocalWords: ithvar
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ experience of updating a couple of projects that are using Spot.
|
|||
=tgba_explicit_string= used to encode a TGBA using a graph whose
|
||||
state was named using LTL formulas, integers, or strings) are
|
||||
replaced by a =twa_graph= class in which the representation is
|
||||
more complact and efficient, but where states are necessarily
|
||||
more compact and efficient, but where states are necessarily
|
||||
numbered. Many algorithms have been rewritten on top of this
|
||||
=twa_graph= class, and this simplified them a lot.
|
||||
|
||||
|
|
@ -360,7 +360,7 @@ removed, ~8200 lines added), and brings some nice benefits:
|
|||
- LTL/PSL formulas are now represented by lightweight formula
|
||||
objects (instead of pointers to children of an abstract
|
||||
formula class) that perform reference counting automatically.
|
||||
- There is no hierachy anymore: all operators are represented by
|
||||
- There is no hierarchy anymore: all operators are represented by
|
||||
a single type of node in the syntax tree, and an enumerator is
|
||||
used to distinguish between operators.
|
||||
- Visitors have been replaced by member functions such as =map()=
|
||||
|
|
@ -665,3 +665,14 @@ for (auto i: aut->succ(s))
|
|||
| ~tgba_succ_iterator::current_acceptance_conditions()~ | ~twa_succ_iterator::acc()~ | |
|
||||
| ~tgba_succ_iterator::current_condition()~ | ~twa_succ_iterator::cond()~ | |
|
||||
| ~tgba_succ_iterator::current_state()~ | ~twa_succ_iterator::dst()~ | |
|
||||
|
||||
# LocalWords: utf html cpp BuDDy ptr TGBA tgba twa tgba renamings
|
||||
# LocalWords: reimplemented cpp SRC bdd bddx BuDDy bvec bvecx fdd
|
||||
# LocalWords: fddx dstarparse eltlparse iface kripke adhoc ltlast
|
||||
# LocalWords: kripkeparse ltlenv ltlparse ltlvisit config sabaalgos
|
||||
# LocalWords: neverparse saba taalgos tgbaalgos dualize tgbaparse
|
||||
# LocalWords: libbdd libbddx lspot lbddx lbdd namespace ptr xargs
|
||||
# LocalWords: typedefs sed aut taa tgta acc buchi myalgorithm succ
|
||||
# LocalWords: iter num dst cond BDDs arg dstar dtgba dupexp bfs dfs
|
||||
# LocalWords: instantiator hoaf lbtt tl simplifier boolean psl str
|
||||
# LocalWords: lbt sclatex utg utf neverclaim scc
|
||||
|
|
|
|||
|
|
@ -780,7 +780,7 @@ _add_formula('are_equivalent', 'equivalent_to')
|
|||
def postprocess(automaton, *args, formula=None, xargs=None):
|
||||
"""Post process an automaton.
|
||||
|
||||
This applies a number of simlification algorithms, depending on
|
||||
This applies a number of simplification algorithms, depending on
|
||||
the options supplied. Keep in mind that 'Deterministic' expresses
|
||||
just a preference that may not be satisfied if the input is
|
||||
not already 'Deterministic'.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue