From 3d0a971aa81613c20b624bcc04ab3cc1555962f5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 25 Dec 2016 12:14:57 +0100 Subject: [PATCH] org: examples with alternating automata * doc/org/tut23.org, doc/org/tut24.org, doc/org/tut31.org: New files. * doc/Makefile.am, doc/org/tut.org: Add them. * doc/org/hoa.org, doc/org/concepts.org: Adjust for alternation support. * NEWS: Add links. --- NEWS | 4 + doc/Makefile.am | 3 + doc/org/concepts.org | 83 +++++++++++-- doc/org/hoa.org | 16 ++- doc/org/tut.org | 3 + doc/org/tut23.org | 179 ++++++++++++++++++++++++++++ doc/org/tut24.org | 272 +++++++++++++++++++++++++++++++++++++++++++ doc/org/tut31.org | 173 +++++++++++++++++++++++++++ 8 files changed, 715 insertions(+), 18 deletions(-) create mode 100644 doc/org/tut23.org create mode 100644 doc/org/tut24.org create mode 100644 doc/org/tut31.org diff --git a/NEWS b/NEWS index 4c0f4b439..d01a80c50 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,10 @@ New in spot 2.2.2.dev (Not yet released) automata, it still has no simplification algorithms that work at the alternating automaton level. + - See https://www.lrde.epita.fr/tut23.html + https://www.lrde.epita.fr/tut24.html and + https://www.lrde.epita.fr/tut31.html for some code examples. + * twa objects have a new property, very-weak, that can be set or retrieved via twa::prop_very_weak(), and that can be tested by is_very_weak_automaton(). diff --git a/doc/Makefile.am b/doc/Makefile.am index 5334e6ce2..d0f9e4079 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -105,7 +105,10 @@ ORG_FILES = \ org/tut20.org \ org/tut21.org \ org/tut22.org \ + org/tut23.org \ + org/tut24.org \ org/tut30.org \ + org/tut31.org \ org/tut50.org \ org/tut51.org \ org/upgrade2.org \ diff --git a/doc/org/concepts.org b/doc/org/concepts.org index fb2cd24e1..2aaecf619 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -554,6 +554,75 @@ $txt #+RESULTS: [[file:concept-twa1.png]] + +* Alternating ω-automata + +Alternating ω-automata are ω-automata in which the destination of an +edge can be a group of states. If an edge has more than one +destination, it is called a /universal edge/, and its destinations are +referred to as its /universal destinations/. + +When an alternating automaton evaluates a word, following a universal +edge will have the same effect as forking the automaton to evaluate +the rest of the word simultaneously from each universal destination. +A run of an alternating automaton can therefore be pictured as a tree. +The tree is accepting if all its branches satisfy the acceptance condition. +(See the [[http://adl.github.io/hoaf/][Hanoi Omega-Automa format]] for more precise semantics.) + +For instance the following alternating co-Büchi ω-automaton was +generated by [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba 1.1.3=]] for the LTL formula =GF(a <-> Xb)=. + +#+NAME: concepts-alt +#+BEGIN_SRC sh :results verbatim :exports none +autfilt -d.ba < Xb)" + [(!0)] 3&0 + [(0)] 2&0 + [t] 1&0 +State: 1 "F(a <-> Xb)" {0} + [(!0)] 3 + [(0)] 2 + [t] 1 +State: 2 "b" + [(1)] 4 +State: 3 "!b" + [(!1)] 4 +State: 4 "t" + [t] 4 +--END-- +EOF +#+END_SRC + +#+BEGIN_SRC dot :file concepts-alt.png :cmdline -Tpng :var txt=concepts-alt :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concepts-alt.png]] + +In this picture, the universal edges appear as arrows with a white +tips going to a small dot, from which additional arrows connect to the +universal destinations. Here the three universal edges all leave the +initial state, and connect to two universal destinations. Note that +non-determinism is allowed between universal edges, for instance upon +reading a word starting with "=a=", this automaton should +non-deterministically decide to read the rest of the word from states +=GF(a<->Xb)= and =F(a<->Xb)= (when taking the universal transition +labeled by =1=) or from states =GF(a<->Xb)= and =b= (when taking the +universal transition labeled by =a=). + +Alternation support in Spot is currently experimental, please report +any issue. The only supported file format able to represent +alternating automata is the [[#hoa][HOA format, introduced below]]. + * Never claims :PROPERTIES: :CUSTOM_ID: neverclaim @@ -770,7 +839,7 @@ $txt The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from the [[:dstar][DSTAR format]], but extends it in many ways, including support for non-deterministic -automata and for arbitrary acceptance conditions. +automata, alternating automata, and for arbitrary acceptance conditions. #+BEGIN_SRC sh :results verbatim :exports results ltldo ltl2dstar -f 'FGp0 | GFp1' --name=%f @@ -826,13 +895,10 @@ $txt Since this file format is the only one able to represent the range of ω-automata supported by Spot, and it its default output format. -However note that Spot does not (yet?) support all automata that can -be expressed using the HOA format. For instance it has no support for -alternating automata, or for the =Alphabet:=-based automata introduced -in v1.1 of HOA (only =AP:=-based automata are supported). - -The present support for the HOA format in Spot, is discussed on [[file:hoa.org][a -separate page]]. +However note that Spot does not support all automata that can be +expressed using the HOA format. The present support for the HOA +format in Spot, is discussed on [[file:hoa.org][a separate page]], with a section +dedicated to the [[file:hoa.org::#restrictions][restrictions]]. * Linear-time Temporal Logic (LTL) :PROPERTIES: @@ -975,7 +1041,6 @@ program. Blue boxes are Python-related. :CUSTOM_ID: property-flags :END: - The automaton class used by Spot to represent ω-Automata is called =twa= (because we use TωA as a short for Transition-based ω-Automaton). As its names implies, the =twa= class supports only diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 3ba4941d5..f691e443a 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -49,15 +49,12 @@ Since the TωA structure is not a perfect one-to-one representation of the HOA format, the output may not be exactly the same as the input. * Features of the HOA format with no or limited support in Spot + :PROPERTIES: + :CUSTOM_ID: restrictions + :END: -- Alternating automata are not supported. - - Only nondeterministic (in the broad sense, meaning "not - deterministic" or "deterministic") automata are currently supported - by Spot. - -- Automata using explicit alphabet (introduced in version 1.1 of the format - via =Alphabet:=) are not supported. +- Automata using explicit alphabet (introduced in version 1.1 of the + format via =Alphabet:=) are not supported. - The maximum number of acceptance sets used is (currently) limited to 32. @@ -633,7 +630,7 @@ redundant and useless properties. For instance =deterministic= automata are necessarily =unambiguous=, and people interested in unambiguous automata know that, so Spot only outputs the =unambiguous= property if an unambiguous automaton is non-deterministic. Similarly, -while Spot only outputs non-alternating automata, it does not output +while Spot may output alternating automata, it does not output the =no-univ-branch= property because we cannot think of a situation where this would be useful. This decision can be overridden by passing the =-Hv= (or =--hoa=v=) option to the command-line tools: @@ -661,6 +658,7 @@ particular: | =state-acc= | checked | yes | checked, unless =-Ht= or =-Hm= | | | =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | | | =no-univ-branch= | ignored | no | only if =-Hv= | | +| =univ-branch= | checked | no | checked | | | =deterministic= | checked | yes | checked | | | =complete= | checked | no | checked | | | =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= | diff --git a/doc/org/tut.org b/doc/org/tut.org index c658583ab..d799d0cdc 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -26,12 +26,15 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[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]] +- [[file:tut31.org][Removing alternation]] * Examples in Python and C++ - [[file:tut03.org][Constructing and transforming formulas]] - [[file:tut21.org][Custom print of an automaton]] - [[file:tut22.org][Creating an automaton by adding states and transitions]] +- [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] +- [[file:tut24.org][Iterating over alternating automata]] * Examples in C++ only diff --git a/doc/org/tut23.org b/doc/org/tut23.org new file mode 100644 index 000000000..26fab84e4 --- /dev/null +++ b/doc/org/tut23.org @@ -0,0 +1,179 @@ +# -*- coding: utf-8 -*- +#+TITLE: Creating an alternating automaton by adding states and transitions +#+DESCRIPTION: Code example for constructing alternating ω-automata in Spot +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +This example demonstrates how to create the following alternating +co-Büchi automaton (recognizing =GFa=) and then print it. + +#+NAME: tut23-dot +#+BEGIN_SRC sh :results verbatim :exports none :var txt=tut23-cpp +autfilt --dot=.a < + #include + #include + + int main(void) + { + // The bdd_dict is used to maintain the correspondence between the + // atomic propositions and the BDD variables that label the edges of + // the automaton. + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + // This creates an empty automaton that we have yet to fill. + spot::twa_graph_ptr aut = make_twa_graph(dict); + + // Since a BDD is associated to every atomic proposition, the + // register_ap() function returns a BDD variable number that can be + // converted into a BDD using bdd_ithvar(). + bdd a = bdd_ithvar(aut->register_ap("a")); + + // Set the acceptance condition of the automaton to co-Büchi + aut->set_acceptance(1, "Fin(0)"); + + // States are numbered from 0. + aut->new_states(3); + // The default initial state is 0, but it is always better to + // specify it explicitely. + aut->set_init_state(0U); + + // new_edge() takes 3 mandatory parameters: source state, + // destination state, and label. A last optional parameter can be + // used to specify membership to acceptance sets. + // + // new_univ_edge() is similar, but the destination is a set of + // states. + aut->new_edge(0, 0, a); + aut->new_univ_edge(0, {0, 1}, !a); + aut->new_edge(1, 1, !a, {0}); + aut->new_edge(1, 2, a); + aut->new_edge(2, 2, bddtrue); + + // Print the resulting automaton. + print_hoa(std::cout, aut); + return 0; + } +#+END_SRC + +#+RESULTS: tut23-cpp +#+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 + +* Python + +#+BEGIN_SRC python :results output :exports both :wrap SRC hoa + import spot + import buddy + + # The bdd_dict is used to maintain the correspondence between the + # atomic propositions and the BDD variables that label the edges of + # the automaton. + bdict = spot.make_bdd_dict(); + # This creates an empty automaton that we have yet to fill. + aut = spot.make_twa_graph(bdict) + + # Since a BDD is associated to every atomic proposition, the register_ap() + # function returns a BDD variable number that can be converted into a BDD + # using bdd_ithvar() from the BuDDy library. + a = buddy.bdd_ithvar(aut.register_ap("a")) + + # Set the acceptance condition of the automaton to co-Büchi + aut.set_acceptance(1, "Fin(0)") + + # States are numbered from 0. + aut.new_states(3) + # The default initial state is 0, but it is always better to + # specify it explicitely. + aut.set_init_state(0); + + # new_edge() takes 3 mandatory parameters: source state, destination state, + # and label. A last optional parameter can be used to specify membership + # to acceptance sets. In the Python version, the list of acceptance sets + # the transition belongs to should be specified as a list. + # + # new_univ_edge() is similar, but the destination is a list of states. + aut.new_edge(0, 0, a); + aut.new_univ_edge(0, [0, 1], -a); + aut.new_edge(1, 1, -a, [0]); + aut.new_edge(1, 2, a); + aut.new_edge(2, 2, buddy.bddtrue); + + # Print the resulting automaton. + print(aut.to_str('hoa')) +#+END_SRC + +#+RESULTS: +#+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 + +* Additional comments + +Alternating automata in Spot can also have a universal initial state: +e.g, an automaton may start in =0&1&2=. Use =set_univ_init_state()= +to declare such as state. + +We have a [[file:tut24.org][separate page]] describing how to explore the edge of an +alternating automaton. + +Once you have built an alternating automaton, you can [[file:tut31.org][remove the +alternation]] to obtain a Büchi or generalized Büchi automaton.. diff --git a/doc/org/tut24.org b/doc/org/tut24.org new file mode 100644 index 000000000..8768053e8 --- /dev/null +++ b/doc/org/tut24.org @@ -0,0 +1,272 @@ +# -*- coding: utf-8 -*- +#+TITLE: Iterating over alternating automata +#+DESCRIPTION: Code example for iterating of alternating ω-automata in Spot +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +Alternating automata can be explored in a very similar way as +non-alternating automata. Most of the code from our [[file:tut21.org][custom automaton +printer]] will still work; the only problem is with universal edges. + +We will use the following example automaton as input (it is just a +slight variation over an [[file:tut23.org][alternating automaton created previously]] to +demonstrate a universal initial state). + +#+NAME: tut24in +#+BEGIN_SRC hoa +HOA: v1 +States: 3 +Start: 0&1 +AP: 1 "a" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +--BODY-- +State: 0 +[0] 0 +[!0] 0&1 +State: 1 +[!0] 1 {0} +[0] 2 +State: 2 +[t] 2 +--END-- +#+END_SRC + +#+NAME: tut24dot +#+BEGIN_SRC sh :results verbatim :exports none :noweb strip-export +cat >tut24.hoa <> +EOF +autfilt --dot=.a tut24.hoa +#+END_SRC + +#+BEGIN_SRC dot :file tut24in.png :cmdline -Tpng :var txt=tut24dot :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut24in.png]] + + +Let us assume that this automaton has been loaded in variable =aut=, +and that we run the following code, similar to what we did in the +[[file:tut21.org][custom automaton printer]]. + +#+NAME: nonalt-body +#+BEGIN_SRC C++ :exports code :noweb strip-export +std::cout << "Initial state: " << aut->get_init_state_number() << '\n'; + +const spot::bdd_dict_ptr& dict = aut->get_dict(); +unsigned n = aut->num_states(); +for (unsigned s = 0; s < n; ++s) + { + std::cout << "State " << s << ":\n"; + for (auto& t: aut->out(s)) + { + std::cout << " edge(" << t.src << " -> " << t.dst << ")\n label = "; + spot::bdd_print_formula(std::cout, dict, t.cond); + std::cout << "\n acc sets = " << t.acc << '\n'; + } + } +#+END_SRC + +#+NAME: nonalt-main +#+BEGIN_SRC C++ :exports none :noweb strip-export + #include + #include + #include + #include + #include + + void custom_print(spot::twa_graph_ptr& aut); + + int main() + { + spot::parsed_aut_ptr pa = parse_aut("tut24.hoa", spot::make_bdd_dict()); + if (pa->format_errors(std::cerr)) + return 1; + // This cannot occur when reading a never claim, but + // it could while reading a HOA file. + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + custom_print(pa->aut); + } +#+END_SRC + +#+NAME: nonalt-one +#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim + <> + void custom_print(spot::twa_graph_ptr& aut) + { + <> + } +#+END_SRC + +#+RESULTS: nonalt-one +#+begin_example +Initial state: 4294967292 +State 0: + edge(0 -> 0) + label = a + acc sets = {} + edge(0 -> 4294967295) + label = !a + acc sets = {} +State 1: + edge(1 -> 1) + label = !a + acc sets = {0} + edge(1 -> 2) + label = a + acc sets = {} +State 2: + edge(2 -> 2) + label = 1 + acc sets = {} +#+end_example + +This output seems correct only for non-universal edges. The reason is +that Spot always store all edges as a tuple (src,dst,label,acc sets), +but universal edges are indicated by setting the most significant bit +of the destination (or of the initial state). + +The "universality" of an edge can be tested using the +=twa_graph::is_univ_dest()= method: it takes a destination state as +input, as in =aut->is_univ_dest(t.dst)= or +=aut->is_univ_dest(aut->get_init_state_number())=. For convenience +this method can also be called on a edge, as in =aut->is_univ_dest(t)=. + +The set of destination states of a universal edge can be iterated over +via the =twa_graph::univ_dests()= method. This takes either a +destination state (=twa_graph::univ_dests(t.dst)=) or more simply an +edge (=twa_graph::univ_dests(t)=). The =univ_dests()= method will +also work on non-universal edges, but in this case it will simply +iterate on the given state. + +Therefor in order to print the universal destinations of any universal +edge in an alternating automaton, we can use =univ_dests()= +unconditionally. In this example, we simply call =is_univ_dest()= to +decide whether to enclose the destinations in braces. + +#+NAME: nonalt-body2 +#+BEGIN_SRC C++ :exports code :noweb strip-export + unsigned init = aut->get_init_state_number(); + std::cout << "Initial state:"; + if (aut->is_univ_dest(init)) + std::cout << " {"; + for (unsigned i: aut->univ_dests(init)) + std::cout << ' ' << i; + if (aut->is_univ_dest(init)) + std::cout << " }"; + std::cout << '\n'; + + const spot::bdd_dict_ptr& dict = aut->get_dict(); + unsigned n = aut->num_states(); + for (unsigned s = 0; s < n; ++s) + { + std::cout << "State " << s << ":\n"; + for (auto& t: aut->out(s)) + { + std::cout << " edge(" << t.src << " ->"; + if (aut->is_univ_dest(t)) + std::cout << " {"; + for (unsigned dst: aut->univ_dests(t)) + std::cout << ' ' << dst; + if (aut->is_univ_dest(t)) + std::cout << " }"; + std::cout << ")\n label = "; + spot::bdd_print_formula(std::cout, dict, t.cond); + std::cout << "\n acc sets = " << t.acc << '\n'; + } + } +#+END_SRC + +#+NAME: nonalt-two +#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim + <> + void custom_print(spot::twa_graph_ptr& aut) + { + <> + } +#+END_SRC + +#+RESULTS: nonalt-two +#+begin_example +Initial state: { 0 1 } +State 0: + edge(0 -> 0) + label = a + acc sets = {} + edge(0 -> { 0 1 }) + label = !a + acc sets = {} +State 1: + edge(1 -> 1) + label = !a + acc sets = {0} + edge(1 -> 2) + label = a + acc sets = {} +State 2: + edge(2 -> 2) + label = 1 + acc sets = {} +#+end_example + +* Python + +Here is the Python version of this code: + +#+BEGIN_SRC python :results output :exports both + import spot + + aut = spot.automaton("tut24.hoa") + + bdict = aut.get_dict() + init = aut.get_init_state_number() + ui = aut.is_univ_dest(init) + print("Initial states: {}{}{}".format("{ " if ui else "", + " ".join(map(str, aut.univ_dests(init))), + " }" if ui else "")) + for s in range(0, aut.num_states()): + print("State {}:".format(s)) + for t in aut.out(s): + ud = aut.is_univ_dest(t) + print(" edge({} -> {}{}{})".format(t.src, + "{ " if ud else "", + " ".join(map(str, aut.univ_dests(t))), + " }" if ud else "")) + print(" label =", spot.bdd_format_formula(bdict, t.cond)) + print(" acc sets =", t.acc) +#+END_SRC + +#+RESULTS: +#+begin_example +Initial states: { 0 1 } +State 0: + edge(0 -> 0) + label = a + acc sets = {} + edge(0 -> { 0 1 }) + label = !a + acc sets = {} +State 1: + edge(1 -> 1) + label = !a + acc sets = {0} + edge(1 -> 2) + label = a + acc sets = {} +State 2: + edge(2 -> 2) + label = 1 + acc sets = {} +#+end_example + + +#+BEGIN_SRC sh :results silent :exports results +rm -f tut24.hoa +#+END_SRC diff --git a/doc/org/tut31.org b/doc/org/tut31.org new file mode 100644 index 000000000..86ea66b26 --- /dev/null +++ b/doc/org/tut31.org @@ -0,0 +1,173 @@ +# -*- 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 +autfilt --dot=.a tut31.hoa +#+END_SRC + +#+BEGIN_SRC dot :file tut31in.png :cmdline -Tpng :var txt=tut31dot :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut31in.png]] + +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.png :cmdline -Tpng :var txt=tut31out :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut31out.png]] + +* 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 + #include + #include + #include + + 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