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.
173 lines
3.5 KiB
Org Mode
173 lines
3.5 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: Alternation removal
|
|
#+DESCRIPTION: Code example for removing alternation in Spot
|
|
#+SETUPFILE: setup.org
|
|
#+HTML_LINK_UP: tut.html
|
|
|
|
Consider the following alternating co-Büchi automaton (see [[file:tut23.org][how to
|
|
create it]]):
|
|
|
|
#+NAME: tut31in
|
|
#+BEGIN_SRC hoa
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
AP: 1 "a"
|
|
acc-name: co-Buchi
|
|
Acceptance: 1 Fin(0)
|
|
properties: univ-branch trans-labels explicit-labels trans-acc complete
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0
|
|
[0] 0
|
|
[!0] 0&1
|
|
State: 1
|
|
[!0] 1 {0}
|
|
[0] 2
|
|
State: 2
|
|
[t] 2
|
|
--END--
|
|
#+END_SRC
|
|
|
|
#+NAME: tut31dot
|
|
#+BEGIN_SRC sh :results verbatim :exports none :noweb strip-export
|
|
cat >tut31.hoa <<EOF
|
|
<<tut31in>>
|
|
EOF
|
|
autfilt --dot=.a tut31.hoa
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC dot :file tut31in.svg :var txt=tut31dot :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:tut31in.svg]]
|
|
|
|
Our goal is to transform this alternating automaton into a
|
|
non-alternating automaton.
|
|
|
|
Alternation support in Spot should be considered as experimental.
|
|
Currently, alternation removal is only supported for weak alternating
|
|
automata, i.e., SCCs should have all there transitions in the same
|
|
acceptance marks. The =remove_alternation()= procedure of Spot will
|
|
produce a [[file:concepts.org::#trans-acc][TGBA]] for [[file:concepts.org::#property-flags][weak]] input, but the smallest automata are obtained
|
|
if the input is [[file:concepts.org::#property-flags][very-weak]].
|
|
|
|
* Shell
|
|
|
|
We simply use =autfilt= with option =--tgba=:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
|
|
autfilt --tgba tut31.hoa
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+BEGIN_SRC hoa
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 1 "a"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels trans-acc complete
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0
|
|
[!0] 0 {0}
|
|
[0] 1 {0}
|
|
State: 1
|
|
[0] 1 {0}
|
|
[!0] 1
|
|
--END--
|
|
#+END_SRC
|
|
|
|
#+NAME: tut31out
|
|
#+BEGIN_SRC sh :results verbatim :exports none
|
|
autfilt --tgba -d tut31.hoa
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC dot :file tut31out.svg :var txt=tut31out :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:tut31out.svg]]
|
|
|
|
* Python
|
|
|
|
In the Python version we call =remove_alternation()=
|
|
|
|
#+BEGIN_SRC python :results output :exports both :wrap SRC hoa
|
|
import spot
|
|
aut = spot.remove_alternation(spot.automaton('tut31.hoa'))
|
|
print(aut.to_str('hoa'))
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+BEGIN_SRC hoa
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 1 "a"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels trans-acc complete
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0
|
|
[0] 0 {0}
|
|
[!0] 1 {0}
|
|
State: 1
|
|
[0] 0 {0}
|
|
[!0] 1
|
|
--END--
|
|
#+END_SRC
|
|
|
|
* C++
|
|
|
|
The C++ version calls =remove_alternation()= too.
|
|
|
|
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
|
|
#include <iostream>
|
|
#include <spot/parseaut/public.hh>
|
|
#include <spot/twaalgos/alternation.hh>
|
|
#include <spot/twaalgos/hoa.hh>
|
|
|
|
int main()
|
|
{
|
|
spot::parsed_aut_ptr pa = parse_aut("tut31.hoa", spot::make_bdd_dict());
|
|
if (pa->format_errors(std::cerr))
|
|
return 1;
|
|
if (pa->aborted)
|
|
{
|
|
std::cerr << "--ABORT-- read\n";
|
|
return 1;
|
|
}
|
|
auto aut = spot::remove_alternation(pa->aut);
|
|
spot::print_hoa(std::cout, aut) << '\n';
|
|
return 0;
|
|
}
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
#+BEGIN_SRC hoa
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 1 "a"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels trans-acc complete
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0
|
|
[0] 0 {0}
|
|
[!0] 1 {0}
|
|
State: 1
|
|
[0] 0 {0}
|
|
[!0] 1
|
|
--END--
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC sh :results silent :exports results
|
|
rm -f tut31.hoa
|
|
#+END_SRC
|