Add code example using the postprocessor.
* doc/org/tut30.org: New file. * doc/Makefile.am, doc/org/tut.org: Add it.
This commit is contained in:
Alexandre Duret-Lutz
parent
87cb58d0a1
commit
61bf5daab4
3 changed files with 290 additions and 0 deletions
|
|
@ -91,6 +91,7 @@ ORG_FILES = \
|
|||
org/tut20.org \
|
||||
org/tut21.org \
|
||||
org/tut22.org \
|
||||
org/tut30.org \
|
||||
org/satmin.org \
|
||||
org/satmin.tex \
|
||||
org/setup.org \
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ three interfaces supported by Spot: shell commands, Python, or C++.
|
|||
- [[file:tut02.org][Relabeling Formulas]]
|
||||
- [[file:tut10.org][Translating an LTL formula into a never claim]]
|
||||
- [[file:tut20.org][Converting a never claim into HOA]]
|
||||
- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]]
|
||||
|
||||
* Examples in Python and C++
|
||||
|
||||
|
|
|
|||
288
doc/org/tut30.org
Normal file
288
doc/org/tut30.org
Normal file
|
|
@ -0,0 +1,288 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tut.html
|
||||
|
||||
Consider the following Rabin automaton, generated by =ltl2dstar=:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' -H > tut30.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
||||
#+NAME: tut30in
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
autfilt tut30.hoa --dot=.a
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: tut30in
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<(Fin(<font color="#5DA5DA">â¿</font>) & Inf(<font color="#F17CB0">â¶</font>)) | (Fin(<font color="#FAA43A">â·</font>) & Inf(<font color="#B276B2">â¸</font>)) | (Fin(<font color="#60BD68">â¹</font>) & Inf(<font color="#F15854">âº</font>))>
|
||||
labelloc="t"
|
||||
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 -> 6
|
||||
0 [label=<0<br/><font color="#FAA43A">â·</font><font color="#F15854">âº</font>>]
|
||||
0 -> 2 [label=<!p1>]
|
||||
0 -> 4 [label=<p1>]
|
||||
1 [label=<1<br/><font color="#FAA43A">â·</font><font color="#F15854">âº</font>>]
|
||||
1 -> 4 [label=<!p1>]
|
||||
1 -> 3 [label=<p1>]
|
||||
2 [label=<2<br/><font color="#B276B2">â¸</font><font color="#60BD68">â¹</font>>]
|
||||
2 -> 0 [label=<!p1>]
|
||||
2 -> 4 [label=<p1>]
|
||||
3 [label=<3<br/><font color="#B276B2">â¸</font><font color="#60BD68">â¹</font>>]
|
||||
3 -> 4 [label=<!p1>]
|
||||
3 -> 1 [label=<p1>]
|
||||
4 [label=<4<br/><font color="#F17CB0">â¶</font><font color="#FAA43A">â·</font><font color="#60BD68">â¹</font>>]
|
||||
4 -> 4 [label=<!p1>]
|
||||
4 -> 4 [label=<p1>]
|
||||
5 [label=<5<br/><font color="#FAA43A">â·</font><font color="#60BD68">â¹</font>>]
|
||||
5 -> 2 [label=<!p1>]
|
||||
5 -> 3 [label=<p1>]
|
||||
6 [label=<6<br/><font color="#FAA43A">â·</font><font color="#60BD68">â¹</font>>]
|
||||
6 -> 5 [label=<!p1>]
|
||||
6 -> 5 [label=<p1>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file tut30in.png :cmdline -Tpng :var txt=tut30in :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:tut30in.png]]
|
||||
|
||||
Our goal is to generate an equivalent Büchi automaton, preserving
|
||||
determinism if possible. However nothing of what we will write is
|
||||
specific to Rabin acceptance: the same code will convert automata with
|
||||
any acceptance to Büchi acceptance.
|
||||
|
||||
* Shell
|
||||
|
||||
We use =autfilt= with option =-B= to request Büchi acceptance and
|
||||
state-based output, =-D= to express a preference for deterministic
|
||||
output, and =-H= for output in the HOA format. Using option
|
||||
=-D/--deterministic= (or =--small=) actually activates the
|
||||
"postprocessing" 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.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
autfilt -B -D -H tut30.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 1
|
||||
AP: 1 "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic inherently-weak
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[t] 2
|
||||
State: 2
|
||||
[!0] 3
|
||||
[0] 4
|
||||
State: 3
|
||||
[0] 0
|
||||
[!0] 3
|
||||
State: 4
|
||||
[!0] 0
|
||||
[0] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
#+NAME: tut30out
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
autfilt -B -D tut30.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: tut30out
|
||||
#+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", peripheries=2]
|
||||
0 -> 0 [label=<1>]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label=<1>]
|
||||
2 [label="2"]
|
||||
2 -> 3 [label=<!p1>]
|
||||
2 -> 4 [label=<p1>]
|
||||
3 [label="3"]
|
||||
3 -> 0 [label=<p1>]
|
||||
3 -> 3 [label=<!p1>]
|
||||
4 [label="4"]
|
||||
4 -> 0 [label=<!p1>]
|
||||
4 -> 4 [label=<p1>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file tut30out.png :cmdline -Tpng :var txt=tut30out :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:tut30out.png]]
|
||||
|
||||
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
|
||||
the result further.
|
||||
|
||||
|
||||
* Python
|
||||
|
||||
The Python version uses the =postprocess()= routine:
|
||||
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic')
|
||||
print(aut.to_str('hoa'))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 1
|
||||
AP: 1 "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic inherently-weak
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[t] 2
|
||||
State: 2
|
||||
[!0] 3
|
||||
[0] 4
|
||||
State: 3
|
||||
[0] 0
|
||||
[!0] 3
|
||||
State: 4
|
||||
[!0] 0
|
||||
[0] 4
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
The =postprocess()= function has an interface similar to
|
||||
[[file:tut10.org][the =translate()= function discussed previously]]:
|
||||
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
help(spot.postprocess)
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
Help on function postprocess in module spot:
|
||||
|
||||
postprocess(automaton, *args)
|
||||
Post process an automaton.
|
||||
|
||||
This applies a number of simlification 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'.
|
||||
|
||||
The optional arguments should be strings among the following:
|
||||
- at most one in 'Generic', 'TGBA', 'BA', or 'Monitor'
|
||||
(type of automaton to build)
|
||||
- at most one in 'Small', 'Deterministic', 'Any'
|
||||
(preferred characteristics of the produced automaton)
|
||||
- at most one in 'Low', 'Medium', 'High'
|
||||
(optimization level)
|
||||
- any combination of 'Complete' and 'StateBasedAcceptance'
|
||||
(or 'SBAcc' for short)
|
||||
|
||||
The default corresponds to 'generic', 'small' and 'high'.
|
||||
|
||||
#+end_example
|
||||
|
||||
|
||||
* C++
|
||||
|
||||
The C++ version of this code is a bit more verbose, because the
|
||||
=postprocess()= function does not exist. You have to instantiate a
|
||||
=postprocessor= object, configure it, and then call it for each
|
||||
automaton to process.
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <iostream>
|
||||
#include "parseaut/public.hh"
|
||||
#include "twaalgos/postproc.hh"
|
||||
#include "twaalgos/hoa.hh"
|
||||
|
||||
int main()
|
||||
{
|
||||
std::string input = "tut30.hoa";
|
||||
spot::parse_aut_error_list pel;
|
||||
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
|
||||
spot::parsed_aut_ptr pa = parse_aut(input, pel, dict);
|
||||
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
||||
return 1;
|
||||
if (pa->aborted)
|
||||
{
|
||||
std::cerr << "--ABORT-- read\n";
|
||||
return 1;
|
||||
}
|
||||
spot::postprocessor post;
|
||||
post.set_type(spot::postprocessor::BA);
|
||||
post.set_pref(spot::postprocessor::Deterministic);
|
||||
post.set_level(spot::postprocessor::High);
|
||||
auto aut = post.run(pa->aut);
|
||||
spot::print_hoa(std::cout, aut) << '\n';
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 1
|
||||
AP: 1 "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic inherently-weak
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[t] 2
|
||||
State: 2
|
||||
[!0] 3
|
||||
[0] 4
|
||||
State: 3
|
||||
[0] 0
|
||||
[!0] 3
|
||||
State: 4
|
||||
[!0] 0
|
||||
[0] 4
|
||||
--END--
|
||||
#+end_example
|
||||
Loading…
Add table
Add a link
Reference in a new issue