alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/org/concepts.org (T-based vs. S-based acceptance): Adjust example.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2022-09-09 16:41:44 +02:00
parent bdac53511a
commit d9248e2e97
1 changed files with 6 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

25
doc/org/concepts.org
View file

@ -381,13 +381,14 @@ When /transition-based acceptance/ is used, acceptance sets are now
sets of /edges/ (or set of /transitions/ if you prefer), and runs are sets of /edges/ (or set of /transitions/ if you prefer), and runs are
accepting if the edges they visit satisfy the acceptance condition. accepting if the edges they visit satisfy the acceptance condition.
Here is an example of Transition-based Generalized Büchi Automaton Here is an example of Transition-based Büchi Automaton
(TGBA). (TBA).
#+NAME: tgba-example1 #+NAME: tgba-example1
#+BEGIN_SRC sh #+BEGIN_SRC sh
ltl2tgba 'GF(a & X(a U b))' -d ltl2tgba 'GF(a & X(a U b))' -d
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file concept-tgba1.svg :var txt=tgba-example1 :exports results #+BEGIN_SRC dot :file concept-tgba1.svg :var txt=tgba-example1 :exports results
$txt $txt
#+END_SRC #+END_SRC
@ -399,27 +400,13 @@ This automaton accept all ω-words that infinitely often match the
pattern $a^+;b$ (that is: a positive number of letters where $a$ is pattern $a^+;b$ (that is: a positive number of letters where $a$ is
true are followed by one letter where $b$ is true). true are followed by one letter where $b$ is true).
Using transition-based acceptance allows for more compact automata. Using transition-based acceptance often allows for more compact automata.
The typical example is the LTL formula =GFa= (infinitely often $a$) For instance the above automaton would need at least 3 states with
that can be represented using a one-state transition-based Büchi
automaton:
#+NAME: tgba-example2
#+BEGIN_SRC sh
ltl2tgba 'GFa' -d
#+END_SRC
#+BEGIN_SRC dot :file concept-tgba2.svg :var txt=tgba-example2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:concept-tgba2.svg]]
While the same property require a 2-state Büchi automaton using
state-based acceptance: state-based acceptance:
#+NAME: tgba-example3 #+NAME: tgba-example3
#+BEGIN_SRC sh #+BEGIN_SRC sh
ltl2tgba 'GFa' -B -d ltl2tgba 'GF(a & X(a U b))' -B -d
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file concept-tba-vs-ba.svg :var txt=tgba-example3 :exports results #+BEGIN_SRC dot :file concept-tba-vs-ba.svg :var txt=tgba-example3 :exports results
$txt $txt