From f3b8bf8e56ec1e97662614b8a586b7e7e66bfcb5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jul 2020 22:15:54 +0200 Subject: [PATCH] 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. --- bin/autfilt.cc | 2 +- doc/org/autcross.org | 11 ++++++- doc/org/autfilt.org | 22 ++++++++++---- doc/org/citing.org | 9 +++++- doc/org/compile.org | 18 +++++++----- doc/org/concepts.org | 20 +++++++++++-- doc/org/csv.org | 23 +++++++++------ doc/org/dstar2tgba.org | 11 +++++-- doc/org/genaut.org | 3 ++ doc/org/genltl.org | 7 +++-- doc/org/hierarchy.org | 15 +++++++--- doc/org/hoa.org | 34 ++++++---------------- doc/org/index.org | 3 ++ doc/org/install.org | 9 ++++-- doc/org/ltl2tgba.org | 64 +++++------------------------------------ doc/org/ltl2tgta.org | 3 +- doc/org/ltlcross.org | 35 +++++++++++++++++++--- doc/org/ltlfilt.org | 10 +++++-- doc/org/ltlgrind.org | 1 + doc/org/ltlsynt.org | 7 ++++- doc/org/oaut.org | 19 +++++++----- doc/org/randaut.org | 41 +++++++------------------- doc/org/randltl.org | 3 +- doc/org/satmin.org | 15 +++++++--- doc/org/tut.org | 4 +++ doc/org/tut01.org | 5 ++++ doc/org/tut02.org | 4 +++ doc/org/tut03.org | 9 ++++-- doc/org/tut04.org | 2 ++ doc/org/tut10.org | 3 ++ doc/org/tut11.org | 4 +++ doc/org/tut12.org | 6 +++- doc/org/tut20.org | 5 +++- doc/org/tut21.org | 6 +++- doc/org/tut22.org | 11 ++++--- doc/org/tut23.org | 7 +++-- doc/org/tut24.org | 5 ++++ doc/org/tut30.org | 10 +++++-- doc/org/tut31.org | 3 ++ doc/org/tut50.org | 9 ++++-- doc/org/tut51.org | 4 +-- doc/org/tut52.org | 5 +++- doc/org/tut90.org | 7 ++++- doc/org/upgrade2.org | 15 ++++++++-- python/spot/__init__.py | 2 +- 45 files changed, 317 insertions(+), 194 deletions(-) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 28fc77bc0..5cc3bda7e 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -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 }, diff --git a/doc/org/autcross.org b/doc/org/autcross.org index eec479e33..058b58619 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -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 diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index bd441d10b..4ccf09f07 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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 diff --git a/doc/org/citing.org b/doc/org/citing.org index bcd322024..0704eb886 100644 --- a/doc/org/citing.org +++ b/doc/org/citing.org @@ -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 diff --git a/doc/org/compile.org b/doc/org/compile.org index e526916e9..8f5eb918f 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -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 diff --git a/doc/org/concepts.org b/doc/org/concepts.org index a9358a242..520da136e 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -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 diff --git a/doc/org/csv.org b/doc/org/csv.org index bfb6fb689..33830f563 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -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 diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index dcd538931..00fae5f20 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -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 diff --git a/doc/org/genaut.org b/doc/org/genaut.org index fef290134..2acc22ecb 100644 --- a/doc/org/genaut.org +++ b/doc/org/genaut.org @@ -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 diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 55d836cdb..14a0b416b 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -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 diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index f0df4c157..3b079c4b4 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -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 diff --git a/doc/org/hoa.org b/doc/org/hoa.org index fcee71c10..a404eae34 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -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=[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=, taillabel="#3"] - 2 -> 2 [label=, 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 diff --git a/doc/org/index.org b/doc/org/index.org index 540ca8eb2..d402b02a4 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -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 diff --git a/doc/org/install.org b/doc/org/install.org index cb485ae58..9cbd35655 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -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 diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 5a332f5a9..c2b911049 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -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=⓿>] - 0 -> 0 [label=] - 1 [label="1"] - 1 -> 0 [label=] - 1 -> 1 [label=] -} -#+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
⓿❶>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 0 -> 2 [label=] - 0 -> 3 [label=] - 1 [label=<1>] - 1 -> 0 [label=] - 1 -> 1 [label=] - 1 -> 2 [label=] - 1 -> 3 [label=] - 2 [label=<2
❶>] - 2 -> 0 [label=] - 2 -> 1 [label=] - 2 -> 2 [label=] - 2 -> 3 [label=] - 3 [label=<3
⓿>] - 3 -> 0 [label=] - 3 -> 1 [label=] - 3 -> 2 [label=] - 3 -> 3 [label=] -} -#+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 diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index 2387c20bf..f85e0fe1b 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -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 diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 491423b85..07f273902 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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 diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index e574334ba..c27853ffa 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -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 diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index 152ea210e..424fb2f59 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -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 diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index d1385ca77..8ca35d9b8 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -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 diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 603b4516c..810cf074b 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 diff --git a/doc/org/randaut.org b/doc/org/randaut.org index ae9e1d359..ec4cd44b8 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -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=] - 0 -> 2 [label=] - 1 [label="1", peripheries=2] - 1 -> 1 [label=] - 1 -> 0 [label=] - 2 [label="2", peripheries=2] - 2 -> 0 [label=] - 2 -> 2 [label=] - 2 -> 1 [label=] -} -#+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 diff --git a/doc/org/randltl.org b/doc/org/randltl.org index d37dd7876..989f56987 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -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 diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 51b8fd9d8..89c17317a 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -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 diff --git a/doc/org/tut.org b/doc/org/tut.org index 4224f2ce2..187e18144 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -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 diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 523bc4b19..91154944c 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -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 diff --git a/doc/org/tut02.org b/doc/org/tut02.org index fd4c5ceb3..0aaddb59a 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -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 diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 1311a0a61..b48366a82 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -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 diff --git a/doc/org/tut04.org b/doc/org/tut04.org index 9dc199138..02317358e 100644 --- a/doc/org/tut04.org +++ b/doc/org/tut04.org @@ -132,3 +132,5 @@ int main() #+RESULTS: : Equivalent + +# LocalWords: utf html args ltlfilt SRC eq lnot otimes ng iostream diff --git a/doc/org/tut10.org b/doc/org/tut10.org index ecfec2330..85cf5b73d 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -215,3 +215,6 @@ translate(formula, *args, dict= {})".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 diff --git a/doc/org/tut22.org b/doc/org/tut22.org index d6db5156a..2c14eebcb 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -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 diff --git a/doc/org/tut23.org b/doc/org/tut23.org index abfad8823..edf868223 100644 --- a/doc/org/tut23.org +++ b/doc/org/tut23.org @@ -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 diff --git a/doc/org/tut24.org b/doc/org/tut24.org index 4a3b1eaab..efbdaa5f0 100644 --- a/doc/org/tut24.org +++ b/doc/org/tut24.org @@ -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 diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 5e3bf6e5d..819b147b7 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -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 diff --git a/doc/org/tut31.org b/doc/org/tut31.org index 966e8770f..eaf39a788 100644 --- a/doc/org/tut31.org +++ b/doc/org/tut31.org @@ -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 diff --git a/doc/org/tut50.org b/doc/org/tut50.org index 41ee4f7e9..789e3e26a 100644 --- a/doc/org/tut50.org +++ b/doc/org/tut50.org @@ -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= -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 diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 3ad26467c..c9fbf3d11 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -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 diff --git a/doc/org/tut52.org b/doc/org/tut52.org index f75865f3f..d68254ceb 100644 --- a/doc/org/tut52.org +++ b/doc/org/tut52.org @@ -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 <> #+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 diff --git a/doc/org/tut90.org b/doc/org/tut90.org index 963385b3a..18536e94f 100644 --- a/doc/org/tut90.org +++ b/doc/org/tut90.org @@ -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 diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 5cb85df12..2406af991 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -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 diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 0be5d0ac5..a3f0c3b57 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -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'.