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

org: Update results to new output

Browse source 
The dotty output changed to be horizontal, and also
the acceptance sets are now numbers.

* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
doc/org/satmin.org: Adjust these four.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-06 18:42:49 +01:00
parent f88020035c
commit f9029858c4
4 changed files with 599 additions and 490 deletions
Download patch file Download diff file Expand all files Collapse all files

149
doc/org/dstar2tgba.org
View file

@ -74,17 +74,18 @@ dstar2tgba -B fagfb
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1"] I -> 0
1 -> 2 [label="a\n"] 0 [label="0"]
1 -> 1 [label="!a\n"] 0 -> 0 [label="!a"]
2 [label="2", peripheries=2] 0 -> 1 [label="a"]
2 -> 2 [label="b\n{Acc[1]}"] 1 [label="1", peripheries=2]
2 -> 3 [label="!b\n{Acc[1]}"] 1 -> 1 [label="b"]
3 [label="3"] 1 -> 2 [label="!b"]
3 -> 2 [label="b\n"] 2 [label="2"]
3 -> 3 [label="!b\n"] 2 -> 1 [label="b"]
2 -> 2 [label="!b"]
} }
#+end_example #+end_example
@ -97,17 +98,18 @@ dstar2tgba -B fagfb | sed 's/\\/\\\\/'
#+RESULTS: fagfb2ba #+RESULTS: fagfb2ba
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1"] I -> 0
1 -> 2 [label="a\\n"] 0 [label="0"]
1 -> 1 [label="!a\\n"] 0 -> 0 [label="!a"]
2 [label="2", peripheries=2] 0 -> 1 [label="a"]
2 -> 2 [label="b\\n{Acc[1]}"] 1 [label="1", peripheries=2]
2 -> 3 [label="!b\\n{Acc[1]}"] 1 -> 1 [label="b"]
3 [label="3"] 1 -> 2 [label="!b"]
3 -> 2 [label="b\\n"] 2 [label="2"]
3 -> 3 [label="!b\\n"] 2 -> 1 [label="b"]
2 -> 2 [label="!b"]
} }
#+end_example #+end_example
@ -127,8 +129,8 @@ dstar2tgba -s fagfb
never { never {
T0_init: T0_init:
if if
:: ((a)) -> goto accept_S2
:: ((!(a))) -> goto T0_init :: ((!(a))) -> goto T0_init
:: ((a)) -> goto accept_S2
fi; fi;
accept_S2: accept_S2:
if if
@ -199,15 +201,16 @@ dstar2tgba gfagfb
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="1"]
1 [label="1"] 1 [label="1"]
1 -> 2 [label="1\n"] 1 -> 1 [label="!a & !b"]
2 [label="2"] 1 -> 1 [label="a & !b\n{0}"]
2 -> 2 [label="a & b\n{Acc[\"1\"], Acc[\"0\"]}"] 1 -> 1 [label="!a & b\n{1}"]
2 -> 2 [label="b & !a\n{Acc[\"1\"]}"] 1 -> 1 [label="a & b\n{0,1}"]
2 -> 2 [label="a & !b\n{Acc[\"0\"]}"]
2 -> 2 [label="!a & !b\n"]
} }
#+end_example #+end_example
@ -218,15 +221,16 @@ dstar2tgba gfagfb | sed 's/\\/\\\\/g'
#+RESULTS: gfagfb2ba #+RESULTS: gfagfb2ba
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="1"]
1 [label="1"] 1 [label="1"]
1 -> 2 [label="1\\n"] 1 -> 1 [label="!a & !b"]
2 [label="2"] 1 -> 1 [label="a & !b\\n{0}"]
2 -> 2 [label="a & b\\n{Acc[\\"1\\"], Acc[\\"0\\"]}"] 1 -> 1 [label="!a & b\\n{1}"]
2 -> 2 [label="b & !a\\n{Acc[\\"1\\"]}"] 1 -> 1 [label="a & b\\n{0,1}"]
2 -> 2 [label="a & !b\\n{Acc[\\"0\\"]}"]
2 -> 2 [label="!a & !b\\n"]
} }
#+end_example #+end_example
@ -293,25 +297,36 @@ dstar2tgba --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d'
For instance using =-a --low= will skip any optional post-processing, For instance using =-a --low= will skip any optional post-processing,
should you find =dstar2tgba= too slow. should you find =dstar2tgba= too slow.
Finally, the output format can be changed with the following options: Finally, the output format can be changed with the following
[[file:oaout.org][common ouput options]]:
#+BEGIN_SRC sh :results verbatim :exports results #+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: -8, --utf8 enable UTF-8 characters in output (ignored with #+begin_example
: --lbtt or --spin) -8, --utf8 enable UTF-8 characters in output (ignored with
: --dot GraphViz's format (default) --lbtt or --spin)
: --lbtt[=t] LBTT's format (add =t to force transition-based --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose
: acceptance even on Büchi automata) (c) circular nodes, (h) horizontal layout, (v)
: -s, --spin Spin neverclaim (implies --ba) vertical layout, (n) with name, (N) without name,
: --spot SPOT's format (s) with SCCs, (t) always transition-based
: --stats=FORMAT output statistics about the automaton acceptance.
-H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters
to select (s) state-based acceptance, (t)
transition-based acceptance, (m) mixed acceptance,
(l) single-line output
--lbtt[=t] LBTT's format (add =t to force transition-based
acceptance even on Büchi automata)
--name=FORMAT set the name of the output automaton
-s, --spin Spin neverclaim (implies --ba)
--spot SPOT's format
--stats=FORMAT output statistics about the automaton
#+end_example
The =--stats= options can output statistics about the input and the The =--stats= options can output statistics about the input and the
output automaton, so it can be useful to search for particular output automaton, so it can be useful to search for particular
pattern. pattern.
For instance here is a complex command that will For instance here is a complex command that will
1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]], 1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]],
@ -333,7 +348,7 @@ output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete. deterministic, and =%p= whether the automaton is complete.
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 --tree-size=10..15 a b c | randltl -n -1 --tree-size=10..14 a b c |
ltlfilt --remove-wm -r -u --size-min=3 | ltlfilt --remove-wm -r -u --size-min=3 |
head -n 10 | head -n 10 |
while read f; do while read f; do
@ -346,26 +361,26 @@ done
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
F(a | !b) c U (c & (a | b | (Xc U (a & Xc))))
DRA: 2st.; BA: 2st.; det.? 1; complete? 1
Fa | (Xc U (c & Xc))
DRA: 5st.; BA: 5st.; det.? 1; complete? 1
X(((!b & XGc) | (b & XF!c)) U (!a & ((!b & XGc) | (b & XF!c))))
DRA: 8st.; BA: 7st.; det.? 1; complete? 0
!b | !a
DRA: 3st.; BA: 2st.; det.? 1; complete? 0 DRA: 3st.; BA: 2st.; det.? 1; complete? 0
F!a !b | F!c
DRA: 2st.; BA: 2st.; det.? 1; complete? 1 DRA: 3st.; BA: 3st.; det.? 1; complete? 1
F(Ga R (b | Ga)) (!a R F!b) R !b
DRA: 10st.; BA: 10st.; det.? 0; complete? 0 DRA: 6st.; BA: 5st.; det.? 1; complete? 0
!c U (!c & !a) b U !c
DRA: 3st.; BA: 2st.; det.? 1; complete? 0 DRA: 3st.; BA: 2st.; det.? 1; complete? 0
!c | FGb GFc
DRA: 4st.; BA: 5st.; det.? 0; complete? 0 DRA: 3st.; BA: 3st.; det.? 1; complete? 1
G(c U a) (F!c U a) R !a
DRA: 6st.; BA: 5st.; det.? 1; complete? 0
b | G!b
DRA: 4st.; BA: 3st.; det.? 1; complete? 0 DRA: 4st.; BA: 3st.; det.? 1; complete? 0
c & Gb !a R (!c & (!a | (F!b U (!a & F!b))))
DRA: 3st.; BA: 2st.; det.? 1; complete? 0 DRA: 5st.; BA: 4st.; det.? 1; complete? 0
F(a & !b & G!c)
DRA: 2st.; BA: 3st.; det.? 0; complete? 0
GF!c
DRA: 3st.; BA: 3st.; det.? 1; complete? 1
#+end_example #+end_example
An important point you should be aware of when comparing these numbers An important point you should be aware of when comparing these numbers

575
doc/org/ltl2tgba.org
View file

@ -20,14 +20,15 @@ ltl2tgba -f 'Fa & GFb'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 1
0 [label="0"]
0 -> 0 [label="b\n{0}"]
0 -> 0 [label="!b"]
1 [label="1"] 1 [label="1"]
1 -> 1 [label="!a\n"] 1 -> 0 [label="a"]
1 -> 2 [label="a\n"] 1 -> 1 [label="!a"]
2 [label="2"]
2 -> 2 [label="b\n{Acc[b]}"]
2 -> 2 [label="!b\n"]
} }
#+end_example #+end_example
@ -54,14 +55,15 @@ ltl2tgba "Fa & GFb" | sed 's/\\/\\\\/'
#+RESULTS: dotex #+RESULTS: dotex
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 1
0 [label="0"]
0 -> 0 [label="b\\n{0}"]
0 -> 0 [label="!b"]
1 [label="1"] 1 [label="1"]
1 -> 2 [label="a\\n"] 1 -> 0 [label="a"]
1 -> 1 [label="!a\\n"] 1 -> 1 [label="!a"]
2 [label="2"]
2 -> 2 [label="b\\n{Acc[b]}"]
2 -> 2 [label="!b\\n"]
} }
#+end_example #+end_example
@ -72,17 +74,17 @@ $txt
#+RESULTS: #+RESULTS:
[[file:dotex.png]] [[file:dotex.png]]
The string between braces, =Acc[b]=, represents an acceptance set (its The string between braces, ={0}=, represents the sets of acceptance
actual name is not really important): any transition labeled by sets a transition belongs to. In this case, there is only one
=Acc[b]= belongs to the =Acc[b]= acceptance set. You may have many acceptance set, called =0=, containing a single transition. You may
transitions in the same acceptance set, and a transition may also have many transitions in the same acceptance set, and a transition may
belong to multiple acceptance sets. An infinite path through this also belong to multiple acceptance sets. An infinite path through
automaton is accepting iff it visit each acceptance set infinitely this automaton is accepting iff it visit each acceptance set
often. Therefore, in the above example, any accepted path will infinitely often. Therefore, in the above example, any accepted path
/necessarily/ leave the initial state after a finite amount of steps, will /necessarily/ leave the initial state after a finite amount of
and then it will verify the property =b= infinitely often. It is also steps, and then it will verify the property =b= infinitely often. It
possible that an automaton do not use any acceptance set at all, in is also possible that an automaton do not use any acceptance set at
which any run is accepting. all, in which any run is accepting.
Here is a TGBA with multiple acceptance sets (we omit the call to Here is a TGBA with multiple acceptance sets (we omit the call to
=dot= to render the output of =ltl2tgba= from now on): =dot= to render the output of =ltl2tgba= from now on):
@ -91,30 +93,36 @@ Here is a TGBA with multiple acceptance sets (we omit the call to
ltl2tgba 'GFa & GFb' ltl2tgba 'GFa & GFb'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: digraph G { #+begin_example
: 0 [label="", style=invis, height=0] digraph G {
: 0 -> 1 rankdir=LR
: 1 [label="1"] I [label="", style=invis, width=0]
: 1 -> 1 [label="a & b\n{Acc[b], Acc[a]}"] I -> 0
: 1 -> 1 [label="b & !a\n{Acc[b]}"] 0 [label="0"]
: 1 -> 1 [label="a & !b\n{Acc[a]}"] 0 -> 0 [label="a & b\n{0,1}"]
: 1 -> 1 [label="!b & !a\n"] 0 -> 0 [label="!a & !b"]
: } 0 -> 0 [label="!a & b\n{1}"]
0 -> 0 [label="a & !b\n{0}"]
}
#+end_example
#+NAME: dotex2 #+NAME: dotex2
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba "GFa & GFb" | sed 's/\\/\\\\/' ltl2tgba "GFa & GFb" | sed 's/\\/\\\\/'
#+END_SRC #+END_SRC
#+RESULTS: dotex2 #+RESULTS: dotex2
: digraph G { #+begin_example
: 0 [label="", style=invis, height=0] digraph G {
: 0 -> 1 rankdir=LR
: 1 [label="1"] I [label="", style=invis, width=0]
: 1 -> 1 [label="a & b\\n{Acc[b], Acc[a]}"] I -> 0
: 1 -> 1 [label="b & !a\\n{Acc[b]}"] 0 [label="0"]
: 1 -> 1 [label="a & !b\\n{Acc[a]}"] 0 -> 0 [label="a & b\\n{0,1}"]
: 1 -> 1 [label="!b & !a\\n"] 0 -> 0 [label="!a & !b"]
: } 0 -> 0 [label="!a & b\\n{1}"]
0 -> 0 [label="a & !b\\n{0}"]
}
#+end_example
#+BEGIN_SRC dot :file dotex2.png :cmdline -Tpng :var txt=dotex2 :exports results #+BEGIN_SRC dot :file dotex2.png :cmdline -Tpng :var txt=dotex2 :exports results
$txt $txt
@ -122,9 +130,9 @@ $txt
#+RESULTS: #+RESULTS:
[[file:dotex2.png]] [[file:dotex2.png]]
The above TGBA has two acceptance sets: =Acc[a]= and =Acc[b]=. The above TGBA has two acceptance sets: =0= and =1=. The position of
The position of these acceptance sets ensures that =a= and =b= atomic these acceptance sets ensures that atomic propositions =a= and =b= must
proposition must be true infinitely often. be true infinitely often.
A Büchi automaton for the previous formula can be obtained with the A Büchi automaton for the previous formula can be obtained with the
=-B= option: =-B= option:
@ -135,19 +143,20 @@ ltl2tgba -B 'GFa & GFb'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="0", peripheries=2] I -> 0
1 -> 1 [label="a & b\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b & !a\n{Acc[1]}"] 0 -> 0 [label="a & b"]
1 -> 3 [label="!b\n{Acc[1]}"] 0 -> 1 [label="!b"]
2 [label="1"] 0 -> 2 [label="!a & b"]
2 -> 1 [label="a\n"] 1 [label="1"]
2 -> 2 [label="!a\n"] 1 -> 0 [label="a & b"]
3 [label="2"] 1 -> 1 [label="!b"]
3 -> 1 [label="a & b\n"] 1 -> 2 [label="!a & b"]
3 -> 2 [label="b & !a\n"] 2 [label="2"]
3 -> 3 [label="!b\n"] 2 -> 0 [label="a"]
2 -> 2 [label="!a"]
} }
#+end_example #+end_example
@ -158,19 +167,20 @@ ltl2tgba -B 'GFa & GFb' | sed 's/\\/\\\\/'
#+RESULTS: dotex2ba #+RESULTS: dotex2ba
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="0", peripheries=2] I -> 0
1 -> 1 [label="a & b\\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b & !a\\n{Acc[1]}"] 0 -> 0 [label="a & b"]
1 -> 3 [label="!b\\n{Acc[1]}"] 0 -> 1 [label="!b"]
2 [label="1"] 0 -> 2 [label="!a & b"]
2 -> 1 [label="a\\n"] 1 [label="1"]
2 -> 2 [label="!a\\n"] 1 -> 0 [label="a & b"]
3 [label="2"] 1 -> 1 [label="!b"]
3 -> 1 [label="a & b\\n"] 1 -> 2 [label="!a & b"]
3 -> 2 [label="b & !a\\n"] 2 [label="2"]
3 -> 3 [label="!b\\n"] 2 -> 0 [label="a"]
2 -> 2 [label="!a"]
} }
#+end_example #+end_example
@ -182,25 +192,93 @@ $txt
Although accepting states in the Büchi automaton are pictured with Although accepting states in the Büchi automaton are pictured with
double-lines, internally this automaton is still handled as a TGBA double-lines, internally this automaton is still handled as a TGBA
with a single acceptance set =Acc[1]= such that the transitions with a single acceptance set such that the transitions
leaving the state are either all accepting, or all non-accepting. leaving the state are either all accepting, or all non-accepting.
This is the reason why the =Acc[1]= sets are still shown in the You can see this underlying TGBA if you pass the =--dot=t= option
output: it shows that a Büchi automaton is (a special case of) a TGBA. (the =t= requests the use of transition-based acceptance at it
is done internally):
Various options controls the output format of =ltl2tgba=: #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba --dot=t -B 'GFa & GFb'
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
rankdir=LR
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="a & b\n{0}"]
0 -> 1 [label="!b\n{0}"]
0 -> 2 [label="!a & b\n{0}"]
1 [label="1"]
1 -> 0 [label="a & b"]
1 -> 1 [label="!b"]
1 -> 2 [label="!a & b"]
2 [label="2"]
2 -> 0 [label="a"]
2 -> 2 [label="!a"]
}
#+end_example
#+NAME: dotex2ba-t
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba --dot=t -B 'GFa & GFb' | sed 's/\\/\\\\/'
#+END_SRC
#+RESULTS: dotex2ba-t
#+begin_example
digraph G {
rankdir=LR
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="a & b\\n{0}"]
0 -> 1 [label="!b\\n{0}"]
0 -> 2 [label="!a & b\\n{0}"]
1 [label="1"]
1 -> 0 [label="a & b"]
1 -> 1 [label="!b"]
1 -> 2 [label="!a & b"]
2 [label="2"]
2 -> 0 [label="a"]
2 -> 2 [label="!a"]
}
#+end_example
#+BEGIN_SRC dot :file dotex2ba-t.png :cmdline -Tpng :var txt=dotex2ba-t :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:dotex2ba-t.png]]
As already discussed on the page about [[file:oaut.org][common output options]], various
options controls the output format of =ltl2tgba=:
#+BEGIN_SRC sh :results verbatim :exports results #+BEGIN_SRC sh :results verbatim :exports results
ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: -8, --utf8 enable UTF-8 characters in output (ignored with #+begin_example
: --lbtt or --spin) -8, --utf8 enable UTF-8 characters in output (ignored with
: --dot GraphViz's format (default) --lbtt or --spin)
: --lbtt LBTT's format --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose
: -s, --spin Spin neverclaim (implies --ba) (c) circular nodes, (h) horizontal layout, (v)
: --spot SPOT's format vertical layout, (n) with name, (N) without name,
: --stats=FORMAT output statistics about the automaton (s) with SCCs, (t) always transition-based
acceptance.
-H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters
to select (s) state-based acceptance, (t)
transition-based acceptance, (m) mixed acceptance,
(l) single-line output
--lbtt[=t] LBTT's format (add =t to force transition-based
acceptance even on Büchi automata)
--name=FORMAT set the name of the output automaton
-q, --quiet suppress all normal output
-s, --spin Spin neverclaim (implies --ba)
--spot SPOT's format
--stats=FORMAT output statistics about the automaton
#+end_example
Option =-8= can be used to improve the readability of the output Option =-8= can be used to improve the readability of the output
if your system can display UTF-8 correctly. if your system can display UTF-8 correctly.
@ -211,19 +289,20 @@ ltl2tgba -B8 'GFa & GFb'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="0", peripheries=2] I -> 0
1 -> 1 [label="a∧b\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b∧a̅\n{Acc[1]}"] 0 -> 0 [label="a∧b"]
1 -> 3 [label="b̅\n{Acc[1]}"] 0 -> 1 [label="b̅"]
2 [label="1"] 0 -> 2 [label="a̅∧b"]
2 -> 1 [label="a\n"] 1 [label="1"]
2 -> 2 [label="a̅\n"] 1 -> 0 [label="a∧b"]
3 [label="2"] 1 -> 1 [label="b̅"]
3 -> 1 [label="a∧b\n"] 1 -> 2 [label="a̅∧b"]
3 -> 2 [label="b∧a̅\n"] 2 [label="2"]
3 -> 3 [label="b̅\n"] 2 -> 0 [label="a"]
2 -> 2 [label="a̅"]
} }
#+end_example #+end_example
@ -234,19 +313,20 @@ ltl2tgba -B8 "GFa & GFb" | sed 's/\\/\\\\/'
#+RESULTS: dotex2ba8 #+RESULTS: dotex2ba8
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="0", peripheries=2] I -> 0
1 -> 1 [label="a∧b\\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b∧a̅\\n{Acc[1]}"] 0 -> 0 [label="a∧b"]
1 -> 3 [label="b̅\\n{Acc[1]}"] 0 -> 1 [label="b̅"]
2 [label="1"] 0 -> 2 [label="a̅∧b"]
2 -> 1 [label="a\\n"] 1 [label="1"]
2 -> 2 [label="a̅\\n"] 1 -> 0 [label="a∧b"]
3 [label="2"] 1 -> 1 [label="b̅"]
3 -> 1 [label="a∧b\\n"] 1 -> 2 [label="a̅∧b"]
3 -> 2 [label="b∧a̅\\n"] 2 [label="2"]
3 -> 3 [label="b̅\\n"] 2 -> 0 [label="a"]
2 -> 2 [label="a̅"]
} }
#+end_example #+end_example
@ -272,19 +352,19 @@ never { /* G(Fa & Fb) */
accept_init: accept_init:
if if
:: ((a) && (b)) -> goto accept_init :: ((a) && (b)) -> goto accept_init
:: ((b) && (!((a)))) -> goto T0_S2 :: ((!(b))) -> goto T0_S2
:: ((!((b)))) -> goto T0_S3 :: ((!(a)) && (b)) -> goto T0_S3
fi; fi;
T0_S2: T0_S2:
if if
:: ((a)) -> goto accept_init :: ((a) && (b)) -> goto accept_init
:: ((!((a)))) -> goto T0_S2 :: ((!(b))) -> goto T0_S2
:: ((!(a)) && (b)) -> goto T0_S3
fi; fi;
T0_S3: T0_S3:
if if
:: ((a) && (b)) -> goto accept_init :: ((a)) -> goto accept_init
:: ((b) && (!((a)))) -> goto T0_S2 :: ((!(a))) -> goto T0_S3
:: ((!((b)))) -> goto T0_S3
fi; fi;
} }
#+end_example #+end_example
@ -348,18 +428,19 @@ ltl2tgba 'Ga|Gb|Gc'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1"] I -> 0
1 -> 2 [label="b\n"] 0 [label="0", peripheries=2]
1 -> 3 [label="c\n"] 0 -> 1 [label="a"]
1 -> 4 [label="a\n"] 0 -> 2 [label="b"]
2 [label="2"] 0 -> 3 [label="c"]
2 -> 2 [label="b\n"] 1 [label="1", peripheries=2]
3 [label="3"] 1 -> 1 [label="a"]
3 -> 3 [label="c\n"] 2 [label="2", peripheries=2]
4 [label="4"] 2 -> 2 [label="b"]
4 -> 4 [label="a\n"] 3 [label="3", peripheries=2]
3 -> 3 [label="c"]
} }
#+end_example #+end_example
@ -370,18 +451,19 @@ ltl2tgba "Ga|Gb|Gc" | sed 's/\\/\\\\/'
#+RESULTS: gagbgc1 #+RESULTS: gagbgc1
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1"] I -> 0
1 -> 2 [label="c\\n"] 0 [label="0", peripheries=2]
1 -> 3 [label="b\\n"] 0 -> 1 [label="a"]
1 -> 4 [label="a\\n"] 0 -> 2 [label="b"]
2 [label="2"] 0 -> 3 [label="c"]
2 -> 2 [label="c\\n"] 1 [label="1", peripheries=2]
3 [label="3"] 1 -> 1 [label="a"]
3 -> 3 [label="b\\n"] 2 [label="2", peripheries=2]
4 [label="4"] 2 -> 2 [label="b"]
4 -> 4 [label="a\\n"] 3 [label="3", peripheries=2]
3 -> 3 [label="c"]
} }
#+end_example #+end_example
@ -397,34 +479,35 @@ ltl2tgba -D 'Ga|Gb|Gc'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="6"] I -> 6
1 -> 1 [label="a & b & c\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b & c & !a\n{Acc[1]}"] 0 -> 0 [label="c"]
1 -> 3 [label="a & c & !b\n{Acc[1]}"] 1 [label="1", peripheries=2]
1 -> 4 [label="c & !a & !b\n{Acc[1]}"] 1 -> 0 [label="!b & c"]
1 -> 5 [label="a & b & !c\n{Acc[1]}"] 1 -> 1 [label="b & c"]
1 -> 6 [label="b & !a & !c\n{Acc[1]}"] 1 -> 2 [label="b & !c"]
1 -> 7 [label="a & !b & !c\n{Acc[1]}"] 2 [label="2", peripheries=2]
2 [label="2"] 2 -> 2 [label="b"]
2 -> 2 [label="b & c\n{Acc[1]}"] 3 [label="3", peripheries=2]
2 -> 4 [label="c & !b\n{Acc[1]}"] 3 -> 2 [label="!a & b"]
2 -> 6 [label="b & !c\n{Acc[1]}"] 3 -> 3 [label="a & b"]
3 [label="4"] 3 -> 5 [label="a & !b"]
3 -> 3 [label="a & c\n{Acc[1]}"] 4 [label="4", peripheries=2]
3 -> 4 [label="c & !a\n{Acc[1]}"] 4 -> 0 [label="!a & c"]
3 -> 7 [label="a & !c\n{Acc[1]}"] 4 -> 4 [label="a & c"]
4 [label="1"] 4 -> 5 [label="a & !c"]
4 -> 4 [label="c\n{Acc[1]}"] 5 [label="5", peripheries=2]
5 [label="5"] 5 -> 5 [label="a"]
5 -> 5 [label="a & b\n{Acc[1]}"] 6 [label="6", peripheries=2]
5 -> 6 [label="b & !a\n{Acc[1]}"] 6 -> 0 [label="!a & !b & c"]
5 -> 7 [label="a & !b\n{Acc[1]}"] 6 -> 1 [label="!a & b & c"]
6 [label="3"] 6 -> 2 [label="!a & b & !c"]
6 -> 6 [label="b\n{Acc[1]}"] 6 -> 3 [label="a & b & !c"]
7 [label="0"] 6 -> 4 [label="a & !b & c"]
7 -> 7 [label="a\n{Acc[1]}"] 6 -> 5 [label="a & !b & !c"]
6 -> 6 [label="a & b & c"]
} }
#+end_example #+end_example
@ -435,34 +518,35 @@ ltl2tgba -D 'Ga|Gb|Gc' | sed 's/\\/\\\\/'
#+RESULTS: gagbgc2 #+RESULTS: gagbgc2
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="6"] I -> 6
1 -> 1 [label="a & b & c\\n{Acc[1]}"] 0 [label="0", peripheries=2]
1 -> 2 [label="b & c & !a\\n{Acc[1]}"] 0 -> 0 [label="c"]
1 -> 3 [label="a & c & !b\\n{Acc[1]}"] 1 [label="1", peripheries=2]
1 -> 4 [label="c & !a & !b\\n{Acc[1]}"] 1 -> 0 [label="!b & c"]
1 -> 5 [label="a & b & !c\\n{Acc[1]}"] 1 -> 1 [label="b & c"]
1 -> 6 [label="b & !a & !c\\n{Acc[1]}"] 1 -> 2 [label="b & !c"]
1 -> 7 [label="a & !b & !c\\n{Acc[1]}"] 2 [label="2", peripheries=2]
2 [label="1"] 2 -> 2 [label="b"]
2 -> 2 [label="b & c\\n{Acc[1]}"] 3 [label="3", peripheries=2]
2 -> 4 [label="c & !b\\n{Acc[1]}"] 3 -> 2 [label="!a & b"]
2 -> 6 [label="b & !c\\n{Acc[1]}"] 3 -> 3 [label="a & b"]
3 [label="2"] 3 -> 5 [label="a & !b"]
3 -> 3 [label="a & c\\n{Acc[1]}"] 4 [label="4", peripheries=2]
3 -> 4 [label="c & !a\\n{Acc[1]}"] 4 -> 0 [label="!a & c"]
3 -> 7 [label="a & !c\\n{Acc[1]}"] 4 -> 4 [label="a & c"]
4 [label="0"] 4 -> 5 [label="a & !c"]
4 -> 4 [label="c\\n{Acc[1]}"] 5 [label="5", peripheries=2]
5 [label="4"] 5 -> 5 [label="a"]
5 -> 5 [label="a & b\\n{Acc[1]}"] 6 [label="6", peripheries=2]
5 -> 6 [label="b & !a\\n{Acc[1]}"] 6 -> 0 [label="!a & !b & c"]
5 -> 7 [label="a & !b\\n{Acc[1]}"] 6 -> 1 [label="!a & b & c"]
6 [label="3"] 6 -> 2 [label="!a & b & !c"]
6 -> 6 [label="b\\n{Acc[1]}"] 6 -> 3 [label="a & b & !c"]
7 [label="5"] 6 -> 4 [label="a & !b & c"]
7 -> 7 [label="a\\n{Acc[1]}"] 6 -> 5 [label="a & !b & !c"]
6 -> 6 [label="a & b & c"]
} }
#+end_example #+end_example
@ -556,14 +640,18 @@ ltl2tgba --help | sed -n '/^ *%/p'
%% a single % %% a single %
%a number of acceptance sets %a number of acceptance sets
%c number of SCCs %c number of SCCs
%d 1 if the automaton is deterministic, 0 otherwise %d 1 if the output is deterministic, 0 otherwise
%e number of edges %e number of edges
%f the formula, in Spot's syntax %f the formula, in Spot's syntax
%n number of nondeterministic states %F name of the input file
%p 1 if the automaton is complete, 0 otherwise %L location in the input file
%r translation time (including pre- and %m name of the automaton
%n number of nondeterministic states in output
%p 1 if the output is complete, 0 otherwise
%r processing time (excluding parsing) in seconds
%s number of states %s number of states
%t number of transitions %t number of transitions
%w one word accepted by the output automaton
#+end_example #+end_example
For instance we can study the size of the automata generated for the For instance we can study the size of the automata generated for the
@ -618,19 +706,21 @@ ltl2tgba -M '(Xa & Fb) | Gc'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0", peripheries=2]
0 -> 1 [label="1"]
0 -> 3 [label="c"]
1 [label="1", peripheries=2] 1 [label="1", peripheries=2]
1 -> 2 [label="1\n"] 1 -> 2 [label="a"]
1 -> 3 [label="c\n"]
2 [label="2", peripheries=2] 2 [label="2", peripheries=2]
2 -> 4 [label="a\n"] 2 -> 2 [label="1"]
3 [label="3", peripheries=2] 3 [label="3", peripheries=2]
3 -> 3 [label="c\n"] 3 -> 3 [label="c"]
4 [label="4", peripheries=2]
4 -> 4 [label="1\n"]
} }
#+end_example #+end_example
#+NAME: monitor1 #+NAME: monitor1
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba -M '(Xa & Fb) | Gc' | sed 's/\\/\\\\/' ltl2tgba -M '(Xa & Fb) | Gc' | sed 's/\\/\\\\/'
@ -639,17 +729,18 @@ ltl2tgba -M '(Xa & Fb) | Gc' | sed 's/\\/\\\\/'
#+RESULTS: monitor1 #+RESULTS: monitor1
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0", peripheries=2]
0 -> 1 [label="1"]
0 -> 3 [label="c"]
1 [label="1", peripheries=2] 1 [label="1", peripheries=2]
1 -> 2 [label="1\\n"] 1 -> 2 [label="a"]
1 -> 3 [label="c\\n"]
2 [label="2", peripheries=2] 2 [label="2", peripheries=2]
2 -> 4 [label="a\\n"] 2 -> 2 [label="1"]
3 [label="3", peripheries=2] 3 [label="3", peripheries=2]
3 -> 3 [label="c\\n"] 3 -> 3 [label="c"]
4 [label="4", peripheries=2]
4 -> 4 [label="1\\n"]
} }
#+end_example #+end_example
@ -666,20 +757,21 @@ ltl2tgba -MD '(Xa & Fb) | Gc'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 3
0 [label="0", peripheries=2]
0 -> 0 [label="1"]
1 [label="1", peripheries=2] 1 [label="1", peripheries=2]
1 -> 2 [label="c\n"] 1 -> 0 [label="a"]
1 -> 3 [label="!c\n"] 2 [label="2", peripheries=2]
2 [label="4", peripheries=2] 2 -> 2 [label="c"]
2 -> 4 [label="a\n"]
2 -> 5 [label="c & !a\n"]
3 [label="3", peripheries=2] 3 [label="3", peripheries=2]
3 -> 4 [label="a\n"] 3 -> 1 [label="!c"]
4 [label="2", peripheries=2] 3 -> 4 [label="c"]
4 -> 4 [label="1\n"] 4 [label="4", peripheries=2]
5 [label="0", peripheries=2] 4 -> 0 [label="a"]
5 -> 5 [label="c\n"] 4 -> 2 [label="!a & c"]
} }
#+end_example #+end_example
@ -691,20 +783,21 @@ ltl2tgba -MD '(Xa & Fb) | Gc' | sed 's/\\/\\\\/'
#+RESULTS: monitor2 #+RESULTS: monitor2
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 3
0 [label="0", peripheries=2]
0 -> 0 [label="1"]
1 [label="1", peripheries=2] 1 [label="1", peripheries=2]
1 -> 2 [label="c\\n"] 1 -> 0 [label="a"]
1 -> 3 [label="!c\\n"] 2 [label="2", peripheries=2]
2 [label="4", peripheries=2] 2 -> 2 [label="c"]
2 -> 4 [label="a\\n"]
2 -> 5 [label="c & !a\\n"]
3 [label="3", peripheries=2] 3 [label="3", peripheries=2]
3 -> 4 [label="a\\n"] 3 -> 1 [label="!c"]
4 [label="2", peripheries=2] 3 -> 4 [label="c"]
4 -> 4 [label="1\\n"] 4 [label="4", peripheries=2]
5 [label="0", peripheries=2] 4 -> 0 [label="a"]
5 -> 5 [label="c\\n"] 4 -> 2 [label="!a & c"]
} }
#+end_example #+end_example

174
doc/org/ltl2tgta.org
View file

@ -23,22 +23,22 @@ ltl2tgta --ta --multiple-init 'a U Gb'
#+begin_example #+begin_example
digraph G { digraph G {
-1 [label="", style=invis, height=0] -1 [label="", style=invis, height=0]
-1 -> 1 [label="a & b"] -1 -> 1 [label="!a & b"]
-2 [label="", style=invis, height=0] -2 [label="", style=invis, height=0]
-2 -> 2 [label="a & !b"] -2 -> 2 [label="a & b"]
-3 [label="", style=invis, height=0] -3 [label="", style=invis, height=0]
-3 -> 3 [label="b & !a"] -3 -> 3 [label="a & !b"]
1 [label="0\na & b",shape=box] 1 [label="2\n!a & b",shape=box]
1 -> 3 [label="{a}\n"]
1 -> 2 [label="{b}\n"]
1 -> 4 [label="{a}\n"] 1 -> 4 [label="{a}\n"]
2 [label="1\na & !b"] 2 [label="1\na & b",shape=box]
2 -> 1 [label="{b}\n"] 2 -> 4 [label="{a}\n"]
2 -> 3 [label="{a, b}\n"] 2 -> 1 [label="{a}\n"]
3 [label="2\nb & !a",shape=box] 2 -> 3 [label="{b}\n"]
3 -> 4 [label="{a}\n"] 3 [label="0\na & !b"]
3 -> 2 [label="{b}\n"]
3 -> 1 [label="{a, b}\n"]
4 [label="3",peripheries=2,shape=box] 4 [label="3",peripheries=2,shape=box]
4 -> 4 [label="{a}\n{Acc[1]}"] 4 -> 4 [label="{a}\n{0}"]
} }
#+end_example #+end_example
@ -50,22 +50,22 @@ ltl2tgta --ta --multiple-init 'a U Gb' | sed 's/\\/\\\\/'
#+begin_example #+begin_example
digraph G { digraph G {
-1 [label="", style=invis, height=0] -1 [label="", style=invis, height=0]
-1 -> 1 [label="a & !b"] -1 -> 1 [label="!a & b"]
-2 [label="", style=invis, height=0] -2 [label="", style=invis, height=0]
-2 -> 2 [label="b & !a"] -2 -> 2 [label="a & b"]
-3 [label="", style=invis, height=0] -3 [label="", style=invis, height=0]
-3 -> 3 [label="a & b"] -3 -> 3 [label="a & !b"]
1 [label="2\\na & !b"] 1 [label="2\\n!a & b",shape=box]
1 -> 3 [label="{b}\\n"] 1 -> 4 [label="{a}\\n"]
1 -> 2 [label="{a, b}\\n"] 2 [label="1\\na & b",shape=box]
2 [label="0\\nb & !a",shape=box]
2 -> 4 [label="{a}\\n"] 2 -> 4 [label="{a}\\n"]
3 [label="1\\na & b",shape=box] 2 -> 1 [label="{a}\\n"]
3 -> 2 [label="{a}\\n"] 2 -> 3 [label="{b}\\n"]
3 -> 1 [label="{b}\\n"] 3 [label="0\\na & !b"]
3 -> 4 [label="{a}\\n"] 3 -> 2 [label="{b}\\n"]
3 -> 1 [label="{a, b}\\n"]
4 [label="3",peripheries=2,shape=box] 4 [label="3",peripheries=2,shape=box]
4 -> 4 [label="{a}\\n{Acc[1]}"] 4 -> 4 [label="{a}\\n{0}"]
} }
#+end_example #+end_example
@ -104,7 +104,7 @@ digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="b & !a\n"] 1 -> 2 [label="!a & b\n"]
1 -> 3 [label="a & b\n"] 1 -> 3 [label="a & b\n"]
1 -> 4 [label="a & !b\n"] 1 -> 4 [label="a & !b\n"]
2 [label="2",shape=box] 2 [label="2",shape=box]
@ -117,7 +117,7 @@ digraph G {
4 -> 3 [label="{b}\n"] 4 -> 3 [label="{b}\n"]
4 -> 2 [label="{a, b}\n"] 4 -> 2 [label="{a, b}\n"]
5 [label="4",peripheries=2,shape=box] 5 [label="4",peripheries=2,shape=box]
5 -> 5 [label="{a}\n{Acc[1]}"] 5 -> 5 [label="{a}\n{0}"]
} }
#+end_example #+end_example
@ -131,20 +131,20 @@ digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="b & !a\\n"] 1 -> 2 [label="!a & b\\n"]
1 -> 3 [label="a & b\\n"] 1 -> 3 [label="a & b\\n"]
1 -> 4 [label="a & !b\\n"] 1 -> 4 [label="a & !b\\n"]
2 [label="2",shape=box] 2 [label="2",shape=box]
2 -> 5 [label="{a}\\n"] 2 -> 5 [label="{a}\\n"]
3 [label="3",shape=box] 3 [label="3",shape=box]
3 -> 5 [label="{a}\\n"]
3 -> 2 [label="{a}\\n"] 3 -> 2 [label="{a}\\n"]
3 -> 4 [label="{b}\\n"] 3 -> 4 [label="{b}\\n"]
3 -> 5 [label="{a}\\n"]
4 [label="1"] 4 [label="1"]
4 -> 3 [label="{b}\\n"] 4 -> 3 [label="{b}\\n"]
4 -> 2 [label="{a, b}\\n"] 4 -> 2 [label="{a, b}\\n"]
5 [label="4",peripheries=2,shape=box] 5 [label="4",peripheries=2,shape=box]
5 -> 5 [label="{a}\\n{Acc[1]}"] 5 -> 5 [label="{a}\\n{0}"]
} }
#+end_example #+end_example
@ -157,7 +157,7 @@ $txt
The =--gba= option can be used to request a Generalized Testing The =--gba= option can be used to request a Generalized Testing
Automaton, i.e., a Testing Automaton with Generalized Büchi Automaton, i.e., a Testing Automaton with Generalized Büchi
acceptance. In that case double-enclosures are not used anymore, and acceptance. In that case double-enclosures are not used anymore, and
Büchi accepting transitions are marked with the same ={Acc[x],Acc[y]}= Büchi accepting transitions are marked with the same ={0,1}=
notation used in TGBA. notation used in TGBA.
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
@ -170,22 +170,22 @@ digraph G {
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="a & b\n"] 1 -> 2 [label="a & b\n"]
1 -> 3 [label="b & !a\n"] 1 -> 3 [label="!a & b\n"]
1 -> 4 [label="a & !b\n"] 1 -> 4 [label="a & !b\n"]
1 -> 5 [label="!b & !a\n"] 1 -> 5 [label="!a & !b\n"]
2 [label="1",shape=box] 2 [label="1",shape=box]
2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"] 2 -> 3 [label="{a}\n{0,1}"]
2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"] 2 -> 4 [label="{b}\n{0,1}"]
2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"] 2 -> 5 [label="{a, b}\n{0,1}"]
3 [label="4"] 3 [label="3"]
3 -> 2 [label="{a}\n{Acc[b]}"] 3 -> 2 [label="{a}\n{1}"]
3 -> 4 [label="{a, b}\n{Acc[b]}"] 3 -> 4 [label="{a, b}\n{1}"]
3 -> 5 [label="{b}\n{Acc[b]}"] 3 -> 5 [label="{b}\n{1}"]
4 [label="2"] 4 [label="2"]
4 -> 2 [label="{b}\n{Acc[a]}"] 4 -> 2 [label="{b}\n{0}"]
4 -> 3 [label="{a, b}\n{Acc[a]}"] 4 -> 3 [label="{a, b}\n{0}"]
4 -> 5 [label="{a}\n{Acc[a]}"] 4 -> 5 [label="{a}\n{0}"]
5 [label="3"] 5 [label="4"]
5 -> 2 [label="{a, b}\n"] 5 -> 2 [label="{a, b}\n"]
5 -> 3 [label="{b}\n"] 5 -> 3 [label="{b}\n"]
5 -> 4 [label="{a}\n"] 5 -> 4 [label="{a}\n"]
@ -203,22 +203,22 @@ digraph G {
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="a & b\\n"] 1 -> 2 [label="a & b\\n"]
1 -> 3 [label="b & !a\\n"] 1 -> 3 [label="!a & b\\n"]
1 -> 4 [label="a & !b\\n"] 1 -> 4 [label="a & !b\\n"]
1 -> 5 [label="!b & !a\\n"] 1 -> 5 [label="!a & !b\\n"]
2 [label="1",shape=box] 2 [label="1",shape=box]
2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"] 2 -> 3 [label="{a}\\n{0,1}"]
2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"] 2 -> 4 [label="{b}\\n{0,1}"]
2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"] 2 -> 5 [label="{a, b}\\n{0,1}"]
3 [label="4"] 3 [label="3"]
3 -> 2 [label="{a}\\n{Acc[b]}"] 3 -> 2 [label="{a}\\n{1}"]
3 -> 4 [label="{a, b}\\n{Acc[b]}"] 3 -> 4 [label="{a, b}\\n{1}"]
3 -> 5 [label="{b}\\n{Acc[b]}"] 3 -> 5 [label="{b}\\n{1}"]
4 [label="2"] 4 [label="2"]
4 -> 2 [label="{b}\\n{Acc[a]}"] 4 -> 2 [label="{b}\\n{0}"]
4 -> 3 [label="{a, b}\\n{Acc[a]}"] 4 -> 3 [label="{a, b}\\n{0}"]
4 -> 5 [label="{a}\\n{Acc[a]}"] 4 -> 5 [label="{a}\\n{0}"]
5 [label="3"] 5 [label="4"]
5 -> 2 [label="{a, b}\\n"] 5 -> 2 [label="{a, b}\\n"]
5 -> 3 [label="{b}\\n"] 5 -> 3 [label="{b}\\n"]
5 -> 4 [label="{a}\\n"] 5 -> 4 [label="{a}\\n"]
@ -233,7 +233,7 @@ $txt
The interpretation is similar to that of the TA. Execution that The interpretation is similar to that of the TA. Execution that
stutter in a livelock-accepting (square) state are accepting as well stutter in a livelock-accepting (square) state are accepting as well
as execution that visit the =Acc[a]= and =Acc[b]= acceptance sets as execution that visit the =0= and =1= acceptance sets
infinitely often. Those acceptance sets are carried by transitions, infinitely often. Those acceptance sets are carried by transitions,
as in TGBAs. as in TGBAs.
@ -252,23 +252,23 @@ digraph G {
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="a & b\n"] 1 -> 2 [label="a & b\n"]
1 -> 3 [label="b & !a\n"] 1 -> 3 [label="!a & b\n"]
1 -> 4 [label="a & !b\n"] 1 -> 4 [label="a & !b\n"]
1 -> 5 [label="!b & !a\n"] 1 -> 5 [label="!a & !b\n"]
2 [label="3"] 2 [label="3"]
2 -> 3 [label="{a}\n{Acc[b], Acc[a]}"] 2 -> 3 [label="{a}\n{0,1}"]
2 -> 4 [label="{b}\n{Acc[b], Acc[a]}"] 2 -> 4 [label="{b}\n{0,1}"]
2 -> 5 [label="{a, b}\n{Acc[b], Acc[a]}"] 2 -> 5 [label="{a, b}\n{0,1}"]
2 -> 2 [label="{}\n{Acc[b], Acc[a]}"] 2 -> 2 [label="{}\n{0,1}"]
3 [label="4"] 3 [label="2"]
3 -> 2 [label="{a}\n{Acc[b]}"] 3 -> 2 [label="{a}\n{1}"]
3 -> 4 [label="{a, b}\n{Acc[b]}"] 3 -> 4 [label="{a, b}\n{1}"]
3 -> 5 [label="{b}\n{Acc[b]}"] 3 -> 5 [label="{b}\n{1}"]
3 -> 3 [label="{}\n"] 3 -> 3 [label="{}\n"]
4 [label="2"] 4 [label="4"]
4 -> 2 [label="{b}\n{Acc[a]}"] 4 -> 2 [label="{b}\n{0}"]
4 -> 3 [label="{a, b}\n{Acc[a]}"] 4 -> 3 [label="{a, b}\n{0}"]
4 -> 5 [label="{a}\n{Acc[a]}"] 4 -> 5 [label="{a}\n{0}"]
4 -> 4 [label="{}\n"] 4 -> 4 [label="{}\n"]
5 [label="1"] 5 [label="1"]
5 -> 2 [label="{a, b}\n"] 5 -> 2 [label="{a, b}\n"]
@ -289,25 +289,25 @@ digraph G {
0 -> 1 0 -> 1
1 [label=init] 1 [label=init]
1 -> 2 [label="a & b\\n"] 1 -> 2 [label="a & b\\n"]
1 -> 3 [label="b & !a\\n"] 1 -> 3 [label="!a & b\\n"]
1 -> 4 [label="a & !b\\n"] 1 -> 4 [label="a & !b\\n"]
1 -> 5 [label="!b & !a\\n"] 1 -> 5 [label="!a & !b\\n"]
2 [label="1"] 2 [label="3"]
2 -> 3 [label="{a}\\n{Acc[b], Acc[a]}"] 2 -> 3 [label="{a}\\n{0,1}"]
2 -> 4 [label="{b}\\n{Acc[b], Acc[a]}"] 2 -> 4 [label="{b}\\n{0,1}"]
2 -> 5 [label="{a, b}\\n{Acc[b], Acc[a]}"] 2 -> 5 [label="{a, b}\\n{0,1}"]
2 -> 2 [label="{}\\n{Acc[b], Acc[a]}"] 2 -> 2 [label="{}\\n{0,1}"]
3 [label="4"] 3 [label="2"]
3 -> 2 [label="{a}\\n{Acc[b]}"] 3 -> 2 [label="{a}\\n{1}"]
3 -> 4 [label="{a, b}\\n{Acc[b]}"] 3 -> 4 [label="{a, b}\\n{1}"]
3 -> 5 [label="{b}\\n{Acc[b]}"] 3 -> 5 [label="{b}\\n{1}"]
3 -> 3 [label="{}\\n"] 3 -> 3 [label="{}\\n"]
4 [label="3"] 4 [label="4"]
4 -> 2 [label="{b}\\n{Acc[a]}"] 4 -> 2 [label="{b}\\n{0}"]
4 -> 3 [label="{a, b}\\n{Acc[a]}"] 4 -> 3 [label="{a, b}\\n{0}"]
4 -> 5 [label="{a}\\n{Acc[a]}"] 4 -> 5 [label="{a}\\n{0}"]
4 -> 4 [label="{}\\n"] 4 -> 4 [label="{}\\n"]
5 [label="2"] 5 [label="1"]
5 -> 2 [label="{a, b}\\n"] 5 -> 2 [label="{a, b}\\n"]
5 -> 3 [label="{b}\\n"] 5 -> 3 [label="{b}\\n"]
5 -> 4 [label="{a}\\n"] 5 -> 4 [label="{a}\\n"]

191
doc/org/satmin.org
View file

@ -103,28 +103,27 @@ ltl2tgba -D -x sat-minimize "GF(a <-> XXb)"
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="!b\n{0}"]
0 -> 1 [label="a & b"]
0 -> 2 [label="!a & b"]
1 [label="1"] 1 [label="1"]
1 -> 1 [label="a & !b\n"] 1 -> 1 [label="a & b\n{0}"]
1 -> 2 [label="!b & !a\n"] 1 -> 1 [label="a & !b"]
1 -> 2 [label="b & !a\n{Acc[1]}"] 1 -> 2 [label="!a & !b"]
1 -> 3 [label="a & b\n{Acc[1]}"] 1 -> 3 [label="!a & b\n{0}"]
2 [label="2"] 2 [label="2"]
2 -> 4 [label="!b & !a\n"] 2 -> 0 [label="a & !b"]
2 -> 4 [label="b & !a\n{Acc[1]}"] 2 -> 1 [label="b\n{0}"]
2 -> 3 [label="a & !b\n"] 2 -> 3 [label="!a & !b"]
2 -> 3 [label="a & b\n{Acc[1]}"] 3 [label="3"]
3 [label="4"] 3 -> 0 [label="a & b"]
3 -> 1 [label="a & !b\n{Acc[1]}"] 3 -> 0 [label="a & !b\n{0}"]
3 -> 1 [label="a & b\n"] 3 -> 3 [label="!a & b"]
3 -> 2 [label="!b & !a\n{Acc[1]}"] 3 -> 3 [label="!a & !b\n{0}"]
3 -> 2 [label="b & !a\n"]
4 [label="3"]
4 -> 2 [label="!b & !a\n{Acc[1]}"]
4 -> 4 [label="b & !a\n"]
4 -> 3 [label="a & !b\n{Acc[1]}"]
4 -> 3 [label="a & b\n"]
} }
#+end_example #+end_example
@ -135,28 +134,27 @@ ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/'
#+RESULTS: gfaexxb3 #+RESULTS: gfaexxb3
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="!b\\n{0}"]
0 -> 1 [label="a & b"]
0 -> 2 [label="!a & b"]
1 [label="1"] 1 [label="1"]
1 -> 1 [label="a & !b\\n"] 1 -> 1 [label="a & b\\n{0}"]
1 -> 1 [label="a & b\\n{Acc[1]}"] 1 -> 1 [label="a & !b"]
1 -> 2 [label="!b & !a\\n"] 1 -> 2 [label="!a & !b"]
1 -> 2 [label="b & !a\\n{Acc[1]}"] 1 -> 3 [label="!a & b\\n{0}"]
2 [label="2"] 2 [label="2"]
2 -> 3 [label="!b & !a\\n"] 2 -> 0 [label="a & !b"]
2 -> 3 [label="b & !a\\n{Acc[1]}"] 2 -> 1 [label="b\\n{0}"]
2 -> 4 [label="a & !b\\n"] 2 -> 3 [label="!a & !b"]
2 -> 4 [label="a & b\\n{Acc[1]}"]
3 [label="3"] 3 [label="3"]
3 -> 1 [label="a & !b\\n{Acc[1]}"] 3 -> 0 [label="a & b"]
3 -> 3 [label="b & !a\\n"] 3 -> 0 [label="a & !b\\n{0}"]
3 -> 4 [label="!b & !a\\n{Acc[1]}"] 3 -> 3 [label="!a & b"]
3 -> 4 [label="a & b\\n"] 3 -> 3 [label="!a & !b\\n{0}"]
4 [label="4"]
4 -> 1 [label="a & !b\\n{Acc[1]}"]
4 -> 1 [label="a & b\\n"]
4 -> 2 [label="!b & !a\\n{Acc[1]}"]
4 -> 2 [label="b & !a\\n"]
} }
#+end_example #+end_example
@ -177,34 +175,36 @@ ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)"
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1", peripheries=2] I -> 0
1 -> 2 [label="!a\n{Acc[1]}"] 0 [label="0"]
1 -> 3 [label="a & !b\n{Acc[1]}"] 0 -> 0 [label="!a & b"]
1 -> 4 [label="a & b\n{Acc[1]}"] 0 -> 1 [label="!a & !b"]
2 [label="2", peripheries=2] 0 -> 2 [label="a & !b"]
2 -> 1 [label="!b & !a\n{Acc[1]}"] 0 -> 3 [label="a & b"]
2 -> 4 [label="a\n{Acc[1]}"] 1 [label="1"]
2 -> 5 [label="b & !a\n{Acc[1]}"] 1 -> 0 [label="!a & b\n{0}"]
3 [label="4"] 1 -> 2 [label="a & !b\n{0}"]
3 -> 1 [label="a & b\n"] 1 -> 3 [label="a & b\n{0}"]
3 -> 2 [label="b & !a\n"] 1 -> 4 [label="!a & !b\n{0}"]
3 -> 3 [label="a & !b\n"] 2 [label="2"]
3 -> 6 [label="!b & !a\n"] 2 -> 4 [label="!a\n{0}"]
4 [label="3"] 2 -> 5 [label="a\n{0}"]
4 -> 1 [label="!b\n"] 3 [label="3"]
4 -> 3 [label="a & b\n"] 3 -> 1 [label="!a & !b"]
4 -> 6 [label="b & !a\n"] 3 -> 2 [label="a & !b"]
5 [label="6"] 3 -> 4 [label="!a & b"]
5 -> 1 [label="!b\n"] 3 -> 5 [label="a & b"]
5 -> 4 [label="a & b\n"] 4 [label="4"]
5 -> 5 [label="b & !a\n"] 4 -> 0 [label="!a & !b"]
6 [label="5"] 4 -> 1 [label="!a & b"]
6 -> 1 [label="a & b\n"] 4 -> 2 [label="a & b"]
6 -> 2 [label="b & !a\n"] 4 -> 3 [label="a & !b"]
6 -> 4 [label="a & !b\n"] 5 [label="5"]
6 -> 5 [label="!b & !a\n"] 5 -> 1 [label="b"]
5 -> 4 [label="!a & !b"]
5 -> 5 [label="a & !b"]
} }
#+end_example #+end_example
@ -215,35 +215,36 @@ ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/'
#+RESULTS: gfaexxb4 #+RESULTS: gfaexxb4
#+begin_example #+begin_example
digraph G { digraph G {
0 [label="", style=invis, height=0] rankdir=LR
0 -> 1 I [label="", style=invis, width=0]
1 [label="1", peripheries=2] I -> 0
1 -> 1 [label="!b & !a\\n{Acc[1]}"] 0 [label="0"]
1 -> 2 [label="b & !a\\n{Acc[1]}"] 0 -> 0 [label="!a & b"]
1 -> 3 [label="a\\n{Acc[1]}"] 0 -> 1 [label="!a & !b"]
0 -> 2 [label="a & !b"]
0 -> 3 [label="a & b"]
1 [label="1"]
1 -> 0 [label="!a & b\\n{0}"]
1 -> 2 [label="a & !b\\n{0}"]
1 -> 3 [label="a & b\\n{0}"]
1 -> 4 [label="!a & !b\\n{0}"]
2 [label="2"] 2 [label="2"]
2 -> 1 [label="!b & !a\\n"] 2 -> 4 [label="!a\\n{0}"]
2 -> 2 [label="b & !a\\n"] 2 -> 5 [label="a\\n{0}"]
2 -> 3 [label="a & !b\\n"] 3 [label="3"]
2 -> 4 [label="a & b\\n"] 3 -> 1 [label="!a & !b"]
3 [label="3", peripheries=2] 3 -> 2 [label="a & !b"]
3 -> 5 [label="!a\\n{Acc[1]}"] 3 -> 4 [label="!a & b"]
3 -> 6 [label="a\\n{Acc[1]}"] 3 -> 5 [label="a & b"]
4 [label="5"] 4 [label="4"]
4 -> 1 [label="!b & !a\\n"] 4 -> 0 [label="!a & !b"]
4 -> 5 [label="b & !a\\n"] 4 -> 1 [label="!a & b"]
4 -> 3 [label="a & !b\\n"] 4 -> 2 [label="a & b"]
4 -> 6 [label="a & b\\n"] 4 -> 3 [label="a & !b"]
5 [label="4"] 5 [label="5"]
5 -> 1 [label="b & !a\\n"] 5 -> 1 [label="b"]
5 -> 2 [label="!b & !a\\n"] 5 -> 4 [label="!a & !b"]
5 -> 3 [label="a & b\\n"] 5 -> 5 [label="a & !b"]
5 -> 4 [label="a & !b\\n"]
6 [label="6"]
6 -> 1 [label="b & !a\\n"]
6 -> 5 [label="!b & !a\\n"]
6 -> 3 [label="a & b\\n"]
6 -> 6 [label="a & !b\\n"]
} }
#+end_example #+end_example