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

@@ -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().

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 \

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 <<EOF
+HOA: v1
+States: 5
+Start: 0
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+AP: 2 "a" "b"
+properties: trans-labels explicit-labels state-acc univ-branch very-weak
+--BODY--
+State: 0 "GF(a <-> 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

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=                        |

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
 

doc/org/tut23.org

+# -*- 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 <<EOF
+$txt
+EOF
+#+END_SRC
+
+#+BEGIN_SRC dot :file tut23-aut.png :cmdline -Tpng :var txt=tut23-dot :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:tut23-aut.png]]
+
+
+Note that the code is very similar to the [[file:tut22.org][previous example]]: in Spot an
+alternating automaton is just an automaton that uses a mix of standard
+edges (declared with =new_edge()=) and universal edges (declared with
+=new_univ_edge()=).
+
+* C++
+  :PROPERTIES:
+  :CUSTOM_ID: cpp
+  :END:
+
+#+NAME: tut23-cpp
+#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
+  #include <iostream>
+  #include <spot/twaalgos/hoa.hh>
+  #include <spot/twa/twagraph.hh>
+
+  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..

doc/org/tut24.org

+# -*- 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
+<<tut24in>>
+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 <string>
+  #include <iostream>
+  #include <spot/parseaut/public.hh>
+  #include <spot/twaalgos/hoa.hh>
+  #include <spot/twa/bddprint.hh>
+
+  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
+  <<nonalt-main>>
+  void custom_print(spot::twa_graph_ptr& aut)
+  {
+    <<nonalt-body>>
+  }
+#+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
+  <<nonalt-main>>
+  void custom_print(spot::twa_graph_ptr& aut)
+  {
+    <<nonalt-body2>>
+  }
+#+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

doc/org/tut31.org

+# -*- 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--