org: document named properties

* doc/org/concepts.org: Add a new section.
* doc/org/hoa.org, spot/twa/twa.hh: Link to it.
* NEWS: Mention it.

NEWS

@@ -80,6 +80,8 @@ New in spot 2.0.3a (not yet released)
 
   * A new example page shows how to test the equivalence of
     two LTL/PSL formulas.  https://spot.lrde.epita.fr/tut04.html
+  * The concepts.html page now lists all named properties
+    used by automata.
 
   Bug fixes:
 

doc/org/concepts.org

@@ -1026,3 +1026,47 @@ These automata properties are encoded into the [[file:hoa.org::#property-bits][H
 be preserved when building a processing pipeline using the shell.
 However the HOA format has support for more properties that do not
 correspond to any =twa= flag.
+
+* Named properties for automata
+   :PROPERTIES:
+   :CUSTOM_ID: named-properties
+   :END:
+
+In addition to [[#proeprty-flags][property flags]], automata in Spot can be tied to an
+arbitrary number of objects via a system of named properties that is
+implemented mostly as an =std::map= between =std::string= and =void*=.
+
+A property can be used to store additional information about the
+automaton, that is not usually available via the automaton interface.
+The property can be set via the =twa::set_named_prop(key, value)=
+method, and queried with the =twa::get_named_prop<type>(key)= template
+method.
+
+Here is a list of named properties currently used inside Spot:
+
+| key name            | (pointed) value type           | description                                                                                                                       |
+|---------------------+--------------------------------+-----------------------------------------------------------------------------------------------------------------------------------|
+| ~automaton-name~    | ~std::string~                  | A name for the automaton, for instance to display in the HOA format.                                                              |
+| ~product-states~    | ~const spot::product_states~   | A vector of pair of states giving the left and right operand of each state in a product automaton.                                |
+| ~state-names~       | ~std::vector<std::string>~     | A vector naming each state of the automaton, for display purpose.                                                                 |
+| ~highlight-edges~   | ~std::map<unsigned, unsigned>~ | A map of (edge number, color number) for highlighting the output.                                                                 |
+| ~highlight-states~  | ~std::map<unsigned, unsigned>~ | A map of (state number, color number) for highlighting the output.                                                                |
+| ~incomplete-states~ | ~std::set<unsigned>~           | A set of states numbers that should be displayed as incomplete.  Used internally by ~print_dot()~ when truncating large automata. |
+
+Objects referenced via named properties are automatically destroyed
+when the automaton is destroyed, but this can be altered by passing a
+custom destructor as a third parameter to =twa::set_named_prop()=.
+
+These properties should be considered short-lived.  They are usually
+not propagated to new automata that are created via transformation,
+unless the algorithme has been explicitely implemented to preserve
+that property.  Algorithm that update the automaton in place should
+probably call =release_named_properties()= to ensure they do not
+inadvertently keep a stale property.
+
+Most of the above properties are related to the graphical display of
+automata, or to their output in the [[file:hoa.org::#named-properties][HOA format]].  So they are usually
+set right before the automaton is output.  The notable exception is
+=product-states=, which is a property present in automata returned by
+=spot::product()= function in case it is necessary to know the origins
+of each state.

doc/org/hoa.org

@@ -692,15 +692,18 @@ The logic of not cluttering the output with all of =!terminal=,
 so only one of those is emitted unless =-Hv= is used.
 
 ** Named properties
+   :PROPERTIES:
+   :CUSTOM_ID: named-properties
+   :END:
 
 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.
+They are currently two [[file:concepts.org::#named-properties][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)
+- =automaton-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:

spot/twa/twa.hh

@@ -961,6 +961,9 @@ namespace spot
     ///
     /// When the automaton is destroyed, the \a destructor function will
     /// be called to destroy the attached object.
+    ///
+    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
+    /// for a list of named properties used by Spot.
     void set_named_prop(std::string s,
                         void* val, std::function<void(void*)> destructor);
 
@@ -975,6 +978,9 @@ namespace spot
     ///
     /// The object will be automatically destroyed when the automaton
     /// is destroyed.
+    ///
+    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
+    /// for a list of named properties used by Spot.
     template<typename T>
     void set_named_prop(std::string s, T* val)
     {
@@ -993,6 +999,9 @@ namespace spot
     /// not include the pointer.
     ///
     /// Returns a nullptr if no such named property exists.
+    ///
+    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
+    /// for a list of named properties used by Spot.
     template<typename T>
     T* get_named_prop(std::string s) const
     {