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.
3.5 KiB
3.5 KiB
Alternation removal
Consider the following alternating co-Büchi automaton (see how to create it):
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--
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 TGBA for weak input, but the smallest automata are obtained
if the input is very-weak.
Shell
We simply use autfilt with option --tgba:
autfilt --tgba tut31.hoaHOA: 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--
Python
In the Python version we call remove_alternation()
import spot
aut = spot.remove_alternation(spot.automaton('tut31.hoa'))
print(aut.to_str('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--C++
The C++ version calls remove_alternation() too.
#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;
}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--