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

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.
parent 0342161b
Pipeline #20621 passed with stage
in 118 minutes and 53 seconds
......@@ -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
# -*- 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 4.8 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 &amp; !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 &amp; b>]
0 -> 1 [label=<!a &amp; !b>]
0 -> 2 [label=<!a &amp; b>]
0 -> 3 [label=<a &amp; !b>]
1 [label=<1>]
1 -> 0 [label=<a &amp; b>]
1 -> 1 [label=<!a &amp; !b>]
1 -> 2 [label=<!a &amp; b>]
1 -> 3 [label=<a &amp; !b>]
2 [label=<2<br/><font color="#F17CB0">❶</font>>]
2 -> 0 [label=<a &amp; b>]
2 -> 1 [label=<!a &amp; !b>]
2 -> 2 [label=<!a &amp; b>]
2 -> 3 [label=<a &amp; !b>]
3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
3 -> 0 [label=<a &amp; b>]
3 -> 1 [label=<!a &amp; !b>]
3 -> 2 [label=<!a &amp; b>]
3 -> 3 [label=<a &amp; !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
# -*- 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