61602a3bba
Suggested in #299. * doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org, doc/org/tut11.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: Adjust all dot outputs to produce svg. * doc/org/arch.tex, doc/org/hierarchy.tex, doc/org/satmin.tex: Adjust to produce a pdf with 12pt text. * doc/Makefile.am: Adjust the generation of arch.svg, hierarchy.svg, and satmin.svg: From above. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust dot arguments to produce svg with 12pt text (the default was 14pt). * doc/org/spot.css: Use Lato as the main font for consistency with automata. * HACKING: pdf2svg is now required to build the doc.
287 lines
7.1 KiB
Org Mode
287 lines
7.1 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it
|
|
#+DESCRIPTION: Code example for converting ω-automata in Spot
|
|
#+SETUPFILE: setup.org
|
|
#+HTML_LINK_UP: tut.html
|
|
|
|
Consider the following Rabin automaton, generated by =ltl2dstar=:
|
|
|
|
#+BEGIN_SRC sh :results silent :exports both
|
|
ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' > 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.svg :var txt=tut30in :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:tut30in.svg]]
|
|
|
|
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 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
|
|
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 :wrap SRC hoa
|
|
autfilt -B -D tut30.hoa
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+BEGIN_SRC hoa
|
|
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 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_SRC
|
|
|
|
#+NAME: tut30out
|
|
#+BEGIN_SRC sh :results verbatim :exports none
|
|
autfilt -B -D -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.svg :var txt=tut30out :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:tut30out.svg]]
|
|
|
|
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 :wrap SRC hoa
|
|
import spot
|
|
aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic')
|
|
print(aut.to_str('hoa'))
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+BEGIN_SRC hoa
|
|
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 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_SRC
|
|
|
|
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 :wrap SRC hoa
|
|
#include <iostream>
|
|
#include <spot/parseaut/public.hh>
|
|
#include <spot/twaalgos/postproc.hh>
|
|
#include <spot/twaalgos/hoa.hh>
|
|
|
|
int main()
|
|
{
|
|
spot::parsed_aut_ptr pa = parse_aut("tut30.hoa", spot::make_bdd_dict());
|
|
if (pa->format_errors(std::cerr))
|
|
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_SRC hoa
|
|
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 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_SRC
|
|
|
|
#+BEGIN_SRC sh :results silent :exports results
|
|
rm -f tut30.hoa
|
|
#+END_SRC
|