diff --git a/doc/Makefile.am b/doc/Makefile.am
index a143b785c..40e27448e 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -65,6 +65,7 @@ ORG_FILES = \
   org/csv.org \
   org/dstar2tgba.org \
   org/genltl.org \
+  org/hoa.org \
   org/ioltl.org \
   org/ltl2tgba.org \
   org/ltl2tgta.org \
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
new file mode 100644
index 000000000..2db9478d3
--- /dev/null
+++ b/doc/org/hoa.org
@@ -0,0 +1,819 @@
+#+TITLE: Support for the Hanoi Omega Automata (HOA) Format
+#+SETUPFILE: setup.org
+#+HTML_LINK_UP: tools.html
+
+
+The [[http://adl.github.io/hoaf/][Hanoi Omega-Automa format]] is a textual representation of
+ω-automata labeled by Boolean formulas over a set of atomic
+propositions, and using an arbitrary acceptance condition. The
+typical acceptances conditions like Büchi, generalized-Büchi,
+co-Büchi, Rabin, Streett, parity, ... are all supported, but the main
+advantage of this format is that any arbitrary acceptance condition
+can be defined.  The HOA format has support for many features such as
+non-determinism, alternation, multiple initial states, transition or
+state-based acceptance, named states, and a range of property flags
+making it possible to store additional information about the
+automaton.
+
+The HOA format is already supported in [[http://adl.github.io/hoaf/support.html][several tools]].  The goal of
+this page is to detail the support of this format in Spot.  It contains
+some information that are useful to better understand the behavior
+of the tools distributed by Spot, and it also look at some lower-level,
+discussing details that are interesting when programming with Spot.
+
+* Format, files, and TωA
+
+Some note about the abbreviation first.  We usually write "HOA format"
+or occasionally HOAF to denote the format (as a specification), and
+HOA or "HOA file" to denote an automaton in that format.  In most
+examples involving HOA files, we use =*.hoa= as a filename extension
+(even if the actual extension does not matter).
+
+When an HOA file is loaded by Spot, it is stored into the
+data-structure used by Spot to represent ω-Automata.  This structure
+is called Transition-based ω-Automaton, henceforth abbreviated TωA.
+Such a TωA can be saved back as an HOA file.  If you run a command
+such as =autfilt -H input.hoa >output.hoa= this is exactly what
+happens: the file =input.hoa= is parsed to create a TωA, and this TωA
+is then printed in the HOA format into =output.hoa=.
+
+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
+
+- Alternating automata are not supported.
+
+  Only nondeterministic (in the broad sense, meaning "not
+  deterministic" or "deterministic") automata are currently supported
+  by Spot.
+
+- The maximum number of acceptance sets used is (currently) limited
+  to 32.
+
+  This limit is not very hard to increase in the source code,
+  however we want to keep it until it becomes an actual problem.  So
+  please report to us if you suffer from it.  In the past, this
+  limitation has forced us to improve some of our algorithms to be
+  less wasteful and not introduce useless acceptance sets.
+
+- Multiple initial states emulated.
+
+  The internal TωA representation used by Spot supports only a single
+  initial state.  When an HOA with multiple initial state is read, it
+  is transformed into an equivalent TωA by merging the initial states
+  into a single one.  The merged state can either be one of the
+  original initial states (if one of those has no incoming edge) or a
+  new state introduced for that purpose.
+
+- =Fin(!x)= and =Inf(!x)= are rewritten away.
+
+  Internally Spot only deals with acceptance conditions involving the
+  primitives =Fin(x)= or =Inf(x)=.  When the parser encounters the
+  variants =Fin(!x)= or =Inf(!x)=, it automatically complements the
+  set =x= so that the resulting acceptance uses only =Fin(x)= and
+  =Inf(x)=.  For instance =Fin(0)&Inf(!1)= gets rewritten into
+  =Fin(0)&Inf(1)= and the membership of all transitions to the set =1=
+  is reversed.
+
+  If =x= was already used without complementation in another
+  primitive, then a new set has to be created.  For instance the
+  acceptance =Inf(0)&Inf(!0)= can only be fixed by adding a new set,
+  =1=, that stores the complement of set =0=, and using
+  =Inf(0)&Inf(1)=.
+
+* Internal representations of some features
+
+In this section we discuss features of the format that are fully
+supported, but in a way that so people could find unexpected.  These
+design choices do not affect the semantics of the HOA format in any
+way.
+
+** State-based vs. transition-based acceptance
+
+A Transition-based ω-Automaton (TωA), as its name implies, uses
+transition-based acceptance sets.  Each edge is stored as a
+quadruplet $(s,d,\ell,F)$ where $s$ and $d$ are the source and
+destination state numbers, $\ell$ is a Binary Decision Diagram (BDD)
+representing the Boolean function labeling the edge, and $F$ is a
+bit-vector representing the membership of the transition to each
+declared acceptance set.
+
+States are just numbers, and may not belong to any accepting set.
+When reading a HOA file that use state-based acceptance (or even
+a mix of state-based and transitions-based acceptance), all the
+acceptance are pushed onto the outgoing transitions.
+
+So an automaton represented as an HOA file with this transition
+structure:
+
+#+BEGIN_SRC sh :results verbatim :exports none
+cat >stvstracc.hoa <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0 {0 1}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1 {0}
+[0] 1 {1}
+[0&1] 2
+State: 2
+[!0] 1 {0}
+[0]  2 {1}
+--END--
+EOF
+#+END_SRC
+
+#+RESULTS:
+
+#+BEGIN_SRC sh :results verbatim :exports results
+sed -n '/--BODY/,/--END/p' stvstracc.hoa | grep -v -- --
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+/* state-based acceptance */
+State: 0 {0 1}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+/* mixed state- and transition-based acceptance */
+State: 1 {0}
+[0] 1 {1}
+[0&1] 2
+/* transition-based acceptance */
+State: 2
+[!0] 1 {0}
+[0]  2 {1}
+#+end_example
+
+will always be stored as a TωA with this transition structure:
+
+#+BEGIN_SRC sh :results verbatim :export results
+autfilt -Ht stvstracc.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+State: 0
+[0&!1] 0 {0 1}
+[0&1] 1 {0 1}
+[!0] 2 {0 1}
+State: 1
+[0] 1 {0 1}
+[0&1] 2 {0}
+State: 2
+[!0] 1 {0}
+[0] 2 {1}
+#+end_example
+
+#+BEGIN_SRC sh :results verbatim :exports none
+rm -f stvstracc.hoa
+#+END_SRC
+
+Even if an input HOA file uses only state-based acceptance, Spot
+internally stores it using transition-based acceptance.  However in
+that case the TωA will have a property bit indicating that it actually
+represents an automaton with the "state-based acceptance" property:
+this implies that transitions leaving one state all belong to the same
+acceptance sets.  A couple of algorithms in Spot checks for this
+property, and enable specialized treatments of state-based automata.
+
+Furthermore, even if an automaton does not have the "state-based
+acceptance" property bit set, the HOA output routine may detect that
+the automaton satisfies this property.  In that case, it output the
+automaton with state-based acceptance.
+
+For instance in the following automaton, the outgoing transitions of
+each states belong to the same sets:
+
+#+NAME: state-based-example
+#+BEGIN_SRC sh :results verbatim :exports both
+cat >sba.hoa <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1
+[0] 1 {1}
+[0&1] 2 {1}
+State: 2
+[!0] 1 {0 1}
+[0]  2 {0 1}
+--END--
+EOF
+autfilt -H sba.hoa
+#+END_SRC
+
+so the HOA output of =autfilt= automatically uses state-based acceptance:
+
+#+RESULTS: state-based-example
+#+begin_example
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1 {1}
+[0] 1
+[0&1] 2
+State: 2 {0 1}
+[!0] 1
+[0] 2
+--END--
+#+end_example
+
+The rational for this automatic switch to state-based acceptance is as follows:
+- Tools that support transition-based acceptance can easily see
+  state-based acceptance as syntactic sugar, so they should be
+  able to process state-based or transition-based acceptance
+  indifferently.
+- Tools that support only state-based acceptance, cannot easily
+  process automata with transition-based acceptance.  So by using
+  state-based acceptance whenever possible, we are making these
+  automata compatible with a larger number of tools.
+- Using state-based acceptance is slightly more space efficient,
+  because there is less redundancy in the output file.
+
+Nevertheless, should you really insist on having an output with
+transition-based acceptance, you can do so by passing the option =t=
+to the HOA printer:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+autfilt -Ht sba.hoa
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0&!1] 0 {0}
+[0&1] 1 {0}
+[!0] 2 {0}
+State: 1
+[0] 1 {1}
+[0&1] 2 {1}
+State: 2
+[!0] 1 {0 1}
+[0] 2 {0 1}
+--END--
+#+end_example
+
+#+BEGIN_SRC sh :results verbatim :exports nond\e
+rm sba.hoa
+#+END_SRC
+
+By default, the output uses either state-based acceptance, or
+transition-based acceptance.  However there is no restriction in the
+format to prevents mixing the two: if you use =-Hm=, the decision of
+using state or transition-based acceptance will be made for each state
+separately.  For instance:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+ltl2tgba -Hm 'GFa | Fb'
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+name: "F(b | GFa)"
+States: 3
+Start: 1
+AP: 2 "b" "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels complete stutter-invariant
+--BODY--
+State: 0 {0}
+[t] 0
+State: 1
+[0] 0
+[!0] 1
+[!0&1] 2
+State: 2
+[1] 2 {0}
+[!1] 2
+--END--
+#+end_example
+
+
+So far we have discussed transforming state-based acceptance into
+transition-based acceptance (this can be seen as removing syntactic
+sugar), and representing transition-based acceptance into state-based
+acceptance when this is possible (adding syntactic sugar) to do so
+without adding states.
+
+It is also possible to transform automata with transition-based
+acceptance into automata with state-based acceptance, adding states
+when necessary.  Most tools have a =-S= option (or
+=--state-based-acceptance=) for this purpose.  Compare the following
+output with the previous one.
+
+#+BEGIN_SRC sh :results verbatim :exports both
+ltl2tgba -S -Hm 'GFa | Fb'
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+name: "F(b | GFa)"
+States: 4
+Start: 0
+AP: 2 "b" "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels complete stutter-invariant
+--BODY--
+State: 0
+[0] 1
+[!0] 0
+[!0&1] 2
+State: 1 {0}
+[t] 1
+State: 2 {0}
+[1] 2
+[!1] 3
+State: 3
+[1] 2
+[!1] 3
+--END--
+#+end_example
+
+** Generic acceptance
+
+Currently, Spot's parser for HOA ignores the optional =acc-name:=
+line, and only uses the mandatory =Acceptance:= line.  As explained
+earlier, if this line contains primitives of the form =Inf(!x)= or
+=Fin(!x)= these are rewritten away, because internally Spot only works
+with primitives of the form =Inf(x)= or =Fin(x)=.  This also means
+that Spot will never produce an acceptance condition containing
+=Fin(!x)= or =Inf(!x)=.
+
+Whenever an HOA file is output, Spot attempts to recognize the
+acceptance condition to give it a suitable =acc-name:= (even if Spot
+does not use this line, it is useful to tools only deal with one
+specific acceptance condition and that do not want to parse the
+=Acceptance:= line).  However the HOA output routine has no idea of
+what type of automata you are trying to output: it is only looking at
+the acceptance condition and trying to name it as precisely as
+possible.  This could be a problem when a given condition accepts
+multiple names.
+
+For instance according to the [[http://adl.github.io/hoaf/#canonical-acceptance-specifications-for-classical-conditions][canonical encodings specified by the HOA
+format]] the condition =Inf(0)= could be called =Buchi=, or
+=generalized-Buchi 1=, or (why not?) =parity min even 1= or =parity
+max even 1=.  Spot will always call this acceptance condition =Buchi=.
+
+Similarly the acceptance condition =t= is always called =all= (not
+=generalized-Buchi 0= or =Rabin 0=, etc.), and while =f= is always
+named =none=.
+
+
+One of the consequence is that when you run =ltl2tgba= with its
+default settings (which are to produce automata with transition-based
+generalized Büchi acceptance) you actually obtain an output that:
+- has an =Acceptance:= line that is a conjunction of =Inf(x)= primitives (or =t=), because
+  that is what generalized Büchi is;
+- has an =acc-name:= line that can be either =generalized-Buchi n=
+  (for $n>1$) or =Buchi= (corresponding to $n=1$) or =all= (corresponding to $n=0$).
+
+The use of =Buchi= or =all= instead of =generalized-Buchi n= follow
+the same idea as our use of state-based acceptance whenever possible.
+By using the name of these inferior acceptance conditions, we hope
+that the resulting automaton can be easier to use with tools that only
+deal with such inferior acceptance conditions.  However, unlike for
+state vs. transition-based acceptance, there is currently no means to
+request another acceptance name to be used.
+
+The [[http://adl.github.io/hoaf/#canonical-acceptance-specifications-for-classical-conditions][canonical encodings for acceptance conditions]] are specified quite
+strictly in the HOA format.  For instance =generalized-Buchi 2=
+corresponds to =Inf(0)&Inf(1)=, not to =Inf(1)&Inf(0)=, even though
+the two formulas are equivalent.  Spot's HOA output routine contains
+some limited form of equivalence check (based mostly on associativity
+and commutativity of the Boolean operators), so that if it detects
+such a simple inversion, it will output it in the order required to be
+allowed to name the acceptance condition.
+
+In the following example, you can see =autfilt= removing the duplicate
+Rabin pair, and reordering the remaining pair to fit the syntax
+corresponding to =Rabin 1=.
+
+#+BEGIN_SRC sh :results verbatim :exports both
+autfilt -H <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 2 (Inf(1) & Fin(0)) | (Inf(1) & Fin(0))
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1
+[0] 1 {1}
+[0&1] 2 {1}
+State: 2
+[!0] 1 {0 1}
+[0]  2 {0 1}
+--END--
+EOF
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1 {1}
+[0] 1
+[0&1] 2
+State: 2 {0 1}
+[!0] 1
+[0] 2
+--END--
+#+end_example
+
+
+
+Internally, the acceptance condition is stored as an array in reverse
+polish notation, and the primitives =Inf= and =Fin= are actually
+parametered by bitsets representing multiple sets numbers.  For
+instance the generalized Büchi acceptance
+=Inf(0)&Inf(1)&Inf(2)&Inf(3)= is actually stored as a single term
+=Inf({0,1,2,3})=.  Similarly, =Fin({1,3,5})= is our internal encoding
+for =Fin(1)|Fin(3)|Fin(5)=.
+
+A more complex acceptance condition, such as
+=(Fin(0)&Inf(1))|(Fin(2)&Inf(3)&Inf(4))|Fin(5)= (a generalized-Rabin
+acceptance), would be encoded as the following 8-element array.
+
+: Fin({5}) Inf({3,4}) Fin({2}) 2& Inf({1}) Fin(0) 2& 3|
+
+This has to be read as a [[http://en.wikipedia.org/wiki/Reverse_Polish_notation][reverse Polish notation]] where the numbers in
+front of the operators =&= and =|= indicate the number of arguments
+they consume (these operators are n-ary).
+
+When you look at an acceptance condition output by Spot, you can
+actually spot the terms that have been grouped together internally by
+looking at the spacing around operators =&= and =|=.  For instance:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+randaut -A"Fin(0)|Fin(1)|Fin(2)&Fin(3)&Inf(4)&Inf(5)" -H 0 | grep Acceptance:
+#+END_SRC
+
+#+RESULTS:
+: Acceptance: 6 (Fin(0)|Fin(1)) | (Fin(2) & Fin(3) & (Inf(4)&Inf(5)))
+
+Here =Fin(0)|Fin(1)= is actually a single internal term =Fin({0,1})=,
+and likewise for =Inf(4)&Inf(5)=.
+
+** Property bits
+
+The =HOA= format supports a number of optional =property:= tokens.
+Currently most of those are ignored by Spot, or used only to
+double-check automata that are read.  For instance is it interesting
+for Spot to know that an automaton is deterministic, but this can be
+automatically determined when the automaton is read, so it is not
+necessary to say so on the =property:= line.  (If =property:
+deterministic= is present, the parser will just make sure that the
+automaton is indeed deterministic, and output an error otherwise.)
+Some of the properties are not as easy to check, and will be stored
+in the future.
+
+Internally, each TωA object carries a set of named bits representing
+properties about the automaton.  Currently these properties are quite
+limited: they will tell for instance if an automaton is deterministic,
+if it uses state-based acceptance (as discussed above), if it is
+stutter-invariant or stutter-sensitive, if it is unambiguous, or if it
+is inherently weak.  This set of supported properties will grow in the
+future.
+
+It should be noted that these bits are only implications.  When such a
+bit is false, it only means that it is unknown whether the property is
+true.  For instance if in some algorithm you want to know whether an
+automaton is deterministic (the equivalent of calling =autfilt -q
+--is-deterministic aut.hoa= from the command-line), you not call the
+method =aut->is_deterministic()= because that only check the property
+bit, and it might be false even if the =aut= is deterministic.
+Instead, call the function =is_deterministic(aut)=.  This function
+will first test the property bit, and do the actual check if it has
+to.
+
+Algorithms that update a TωA should call the method =prop_keep()= and
+use the argument to specify which of the properties they preserve.
+Algorithms that input a TωA and output a new one may call the method
+=prop_copy()= to copy over the subset of properties they preserve.
+Using these two functions ensure that in the future, whenever a new
+property is added to the TωA class, we cannot forget to update all the
+calls =prop_copy()= or =prop_keep()= (because these functions will
+take a new argument).
+
+** Named properties
+
+In addition to the bit properties discussed above, a TωA can carry
+named properties of any type.  When attaching a property to a TωA, you
+only supply a name for the property, a pointer, and an optional
+destructor function.
+
+They are currently two named properties related to the HOA format.
+
+- =name= :: Is a string that stores the name of the automaton (the one given after =name:= in the HOA format)
+- =state-names= :: is a vector of strings that stores the name of the states (in case states are named in the HOA format)
+
+You can see these properties being preserved when an automaton is read and then immediately output:
+
+#+NAME: hello-world
+#+BEGIN_SRC sh :results verbatim :exports both
+cat >hw.hoa <<EOF
+HOA: v1
+name: "hello world!"
+States: 3
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1 "I am a state"
+[0] 1 {1}
+[0&1] 2 {1}
+State: 2 "so am I"
+[!0] 1 {0 1}
+[0]  2 {0 1}
+--END--
+EOF
+autfilt -H hw.hoa
+#+END_SRC
+
+#+RESULTS: hello-world
+#+begin_example
+HOA: v1
+name: "hello world!"
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[0&!1] 0
+[0&1] 1
+[!0] 2
+State: 1 "I am a state" {1}
+[0] 1
+[0&1] 2
+State: 2 "so am I" {0 1}
+[!0] 1
+[0] 2
+--END--
+#+end_example
+
+However if =autfilt= performs some transformation, and actually has to
+construct a new automaton, those properties will not be quarried over
+to the new automaton.  First because it is not obvious that the new
+automaton should have the same name, and second because if a new
+automaton is created, there might not be clear correspondence between
+the old states and the new ones.
+
+
+Here is for instance the result when =autfilt= is instructed to
+simplify the automaton:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+autfilt -H --small hw.hoa
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0&!1] 0
+[0&1] 1 {0}
+[!0] 2 {0}
+State: 1
+[0&!1] 1
+[0&1] 2
+State: 2
+[!0] 1 {0}
+[0] 2 {0}
+--END--
+#+end_example
+
+
+Note that if the name of the automaton is important to you, it can be
+fixed via the =--name= option.  For instance =--name=%M= will
+construct the new name by simply copying the one of the original
+automaton.
+
+#+BEGIN_SRC sh :results verbatim :exports both
+autfilt -H --small hw.hoa --name=%M
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+name: "hello world!"
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0&!1] 0
+[0&1] 1 {0}
+[!0] 2 {0}
+State: 1
+[0&!1] 1
+[0&1] 2
+State: 2
+[!0] 1 {0}
+[0] 2 {0}
+--END--
+#+end_example
+
+The page about [[file:oaut.org][common output option for automata]] has a section showing
+how =--name= can be used to construct complex pipelines with automata that
+preserve their equivalent LTL formula in the =name:= field.
+
+* Streaming support
+
+The HOA format has been designed to easily allow multiple automata to
+be concatenated together (in the same file, or in a pipe) and
+processed in batch.  Spot's parser supports this scenario and can be
+called repeatedly to read the next automaton from the input stream.
+
+For instance the following creates 3 formulas of the form $\bigwedge_i
+\mathsf{G}\mathsf{F} p_i$, translates those into Büchi automata output
+in the HOA format, and then read those automata with =autfilt= to
+randomize the order of their transitions and states before printing
+them in HOA format.
+
+#+BEGIN_SRC sh :results verbatim :exports both
+genltl --and-gf=1..3 | ltl2tgba -B -F- -H | autfilt --randomize -H
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+HOA: v1
+name: "GFp1"
+States: 2
+Start: 1
+AP: 1 "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0] 1
+[!0] 0
+State: 1 {0}
+[!0] 0
+[0] 1
+--END--
+HOA: v1
+name: "G(Fp1 & Fp2)"
+States: 3
+Start: 1
+AP: 2 "p1" "p2"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!0&1] 2
+[0&1] 1
+[!1] 0
+State: 1 {0}
+[0&1] 1
+[!0&1] 2
+[!1] 0
+State: 2
+[!0] 2
+[0] 1
+--END--
+HOA: v1
+name: "G(Fp1 & Fp2 & Fp3)"
+States: 4
+Start: 1
+AP: 3 "p1" "p2" "p3"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!2] 0
+[!1&2] 2
+[0&1&2] 1
+[!0&1&2] 3
+State: 1 {0}
+[!0&1&2] 3
+[!1&2] 2
+[0&1&2] 1
+[!2] 0
+State: 2
+[0&1] 1
+[!0&1] 3
+[!1] 2
+State: 3
+[0] 1
+[!0] 3
+--END--
+#+end_example
+
+
+It should be noted that the HOA parser is less efficient when it reads
+from a pipe than when it reads from a file.  The reason is that if two
+commands =A | B= exchange automata via a pipe, the command =A= may
+require some time between the output of two automata, so if =B= does a
+block read on its input to fill the parser's buffer, it might not be
+able to process any automaton before =A= has produced enough automata
+to fill the buffer.  To avoid this delay, whenever =B= detects that
+the input is a pipe (or a terminal), it switches to an interactive
+mode, where the input is read one character at a time.  This way an
+automaton can be processed by =B= as soon as its =--END--= has been
+received.
+
+The HOA format has support for a =--ABORT--= token, that can be used
+by tools that produce automata in a stream to cancel the current one.
+This makes sense for instance when the automaton is constructed
+on-the-fly, while it is being output.  This scenario does not occur in
+Spot (automata are constructed before they are output), so it does not
+emit =--ABORT--=.  However the input parser is fully aware of this
+token.  Tools like =autfilt= will diagnose aborted automata in the
+input, and continue processing with the next automaton.  The Python
+bindings for the HOA parser can be configured in two modes: skip
+aborted automata, or flag them as errors.
+
+* Error recovery
+
+The HOA parser does a fair amount of error recovery.  It is important
+that when parsing a stream of automata, a syntax error in one
+automaton does not invalidate the following automata (the parser
+should at least be able to ignore everything up to =--END--= if it
+cannot recover before).
+
+Another scenario where syntax errors are more frequent is when an HOA
+file is hand-edited.  For instance one could edit an HOA file to add a
+few states and transitions, and forget to update the total number of
+states in the format.  In that case the parser will diagnose the problem,
+and fix the number of states.
+
+* Checked properties
+
+When an automaton is output in HOA format, the =property:= lines
+includes property registered into the automaton (see the Property
+bits section above), and property that are trivial to compute.
+
+Command-line with a HOA output all have a =--check= option that can be
+used to request additional checks such as testing whether the
+automaton is stutter-invariant, or unambiguous.
diff --git a/doc/org/oaut.org b/doc/org/oaut.org
index 965bc0310..c39c34620 100644
--- a/doc/org/oaut.org
+++ b/doc/org/oaut.org
@@ -61,11 +61,12 @@ strange to ask a tool to not output anything, but it makes sense when
 only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check
 whether an input automaton has some property) or for timing purposes.
 
-* HOAF output
+* HOA output
 
-The [[http://adl.github.io/hoaf/][HOAF]] output should be the preferred format to use if you want to
+The [[http://adl.github.io/hoaf/][HOA]] output should be the preferred format to use if you want to
 pass automata between different tools.  This format can be requested
-using the =-H= option.
+using the =-H= option.  (Details about supported features of the HOA
+format can be found on a [[file:hoa.org][separate page]].)
 
 Here is an example where [[file:ltl2tgba.org][=ltl2tgba=]] is used to construct two automata:
 one for =a U b= and one for =(Ga -> Gb) W c=.
@@ -480,7 +481,7 @@ output in GraphViz's format.
 ltl2tgba '(Ga -> Gb) W c'
 #+END_SRC
 
-#+BEGIN_SRC sh :results verbatim :exports result
+#+BEGIN_SRC sh :results verbatim :exports results
 SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot=
 #+END_SRC
 
diff --git a/doc/org/tools.org b/doc/org/tools.org
index 69f76bc71..a73fe6538 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -29,10 +29,11 @@ Parts of these documents (e.g., lists of options) are actually the
 results of shell commands and will be presented as above, even if the
 corresponding commands are hidden.
 
-* Common options
+* Documentation common to multiple tools
 
 - [[file:ioltl.org][common input and output options for LTL/PSL formulas]]
 - [[file:oaut.org][common output options for automata]]
+- [[file:hoa.org][input and output support for the HOA format]]
 
 * Command-line tools