2402d721a9
* doc/org/spot2.svg: New file. * doc/Makefile.am: Distribute it. * doc/org/.gitignore: Adjust. * doc/org/setup.org: Display it. * doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.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, doc/org/upgrade2.org: Include setup.org instead of declaring it as SETUPFILE. * doc/org/spot.css: Add entries for the logo. * python/ajax/trans.html: Use the new logo. * python/ajax/logos/mail.png, python/ajax/logos/spot64s.png: Delete. * python/ajax/Makefile.am: Adjust.
173 lines
3.4 KiB
Org Mode
173 lines
3.4 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: Alternation removal
|
|
#+DESCRIPTION: Code example for removing alternation in Spot
|
|
#+INCLUDE: 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 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
|