docs: slightly improve documentation

Doxyfile.in

@@ -714,7 +714,7 @@ WARN_LOGFILE           =
 # spaces.
 # Note: If this tag is empty the current directory is searched.
 
-INPUT                  = @CMAKE_SOURCE_DIR@/include
+INPUT                  = @CMAKE_SOURCE_DIR@/include @CMAKE_SOURCE_DIR@/src
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses
@@ -735,7 +735,8 @@ INPUT_ENCODING         = UTF-8
 # *.qsf, *.as and *.js.
 
 FILE_PATTERNS          = *.h \
-                         *.hh
+                         *.hh \
+                         *.hpp
 
 # The RECURSIVE tag can be used to specify whether or not subdirectories should
 # be searched for input files as well.
@@ -783,7 +784,7 @@ EXCLUDE_SYMBOLS        =
 # that contain example code fragments that are included (see the \include
 # command).
 
-EXAMPLE_PATH           = ..
+EXAMPLE_PATH           = @CMAKE_SOURCE_DIR@/examples
 
 # If the value of the EXAMPLE_PATH tag contains directories, you can use the
 # EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and

include/mata/afa.hh

@@ -37,6 +37,14 @@
 
 namespace Mata
 {
+/**
+ * Alternating Finite Automata including structures, transitions and algorithms.
+ *
+ * In particular, this includes:
+ *   1. Structures (Automaton, Transitions, Results),
+ *   2. Algorithms (operations, checks, tests),
+ *   3. Constructions.
+ */
 namespace Afa
 {
 extern const std::string TYPE_AFA;

include/mata/nfa-algorithms.hh

@@ -26,11 +26,17 @@ namespace Mata {
 namespace Nfa {
 
 /**
- * The following namespace contains methods which would be otherwise in anonymous namespace
- * to make them accessible to users of library. Typically, that are different algorithms for
- * operations such as complement, inclusion, or universality checking.
- * In Nfa interface, there are dispatch functions calling these function according to parameters
- * provided by a user.
+ * NFA algorithms, includes implementations for operations such as complement, inclusion, or universality checking.
+ *
+ * Note, that in Mata::Nfa interface, there are dispatch functions calling these function
+ * according to parameters provided by a user.
+ *
+ * In particular, this includes algorithms for:
+ *   1. Complementation,
+ *   2. Inclusion,
+ *   3. Universality checking,
+ *   4. Intersection/concatenation with epsilon transitions, or,
+ *   5. Computing relation.
  */
 namespace Algorithms {
 

include/mata/nfa-plumbing.hh

@@ -24,6 +24,12 @@ namespace Mata {
 
 namespace Nfa {
 
+/**
+ * Simplified NFA API, used in binding to call NFA algorithms.
+ *
+ * In particular, this mostly includes operations and checks, that do not return Automaton,
+ * but instead take resulting automaton as pointer (e.g. `void f(Nfa* result, const Nfa& lhs, const Nfa& rhs)`).
+ */
 namespace Plumbing {
 
     /// Make the transition relation complete.

include/mata/nfa-strings.hh

@@ -28,6 +28,9 @@ namespace {
 }
 
 namespace Mata {
+/**
+ * NFA Algorithms usable for solving string constraints.
+ */
 namespace Strings {
     /**
      * Class mapping states to the shortest words accepted by languages of the states.
@@ -143,13 +146,13 @@ namespace Strings {
     Nfa::Nfa create_single_word_nfa(const std::vector<std::string>& word, Alphabet* alphabet = nullptr);
 
 /**
- * Operations on segment automata.
+ * Segment Automata including structs and algorithms.
+ *
+ * These are automata whose state space can be split into several segments connected by ε-transitions in a chain.
+ * No other ε-transitions are allowed. As a consequence, no ε-transitions can appear in a cycle.
+ * Segment automaton can have initial states only in the first segment and final states only in the last segment.
  */
 namespace SegNfa {
-    /// Segment automaton.
-    /// These are automata whose state space can be split into several segments connected by ε-transitions in a chain.
-    /// No other ε-transitions are allowed. As a consequence, no ε-transitions can appear in a cycle.
-    /// Segment automaton can have initial states only in the first segment and final states only in the last segment.
     using SegNfa = Nfa::Nfa;
     using VisitedEpsMap = std::map<State, std::map<Symbol, unsigned>>;
 

include/mata/nfa.hh

@@ -39,6 +39,17 @@
 #include <mata/inter-aut.hh>
 #include <mata/synchronized-iterator.hh>
 
+/**
+ * Nondeterministic Finite Automata including structures, transitions and algorithms.
+ *
+ * In particular, this includes:
+ *   1. Structures (Automaton, Transitions, Results, Delta),
+ *   2. Algorithms (operations, checks, tests),
+ *   3. Constructions.
+ *
+ * Other algorithms are including in Mata::Nfa::Plumbing (simplified API for, e.g., binding)
+ * and Mata::Nfa::Algorithms (concrete implementations of algorithms, such as for complement).
+ */
 namespace Mata::Nfa {
 extern const std::string TYPE_NFA;
 

include/mata/parser.hh

@@ -31,6 +31,11 @@
 
 namespace Mata
 {
+/**
+ * Parser from `.mata` format to automata (currently `Nfa` and `Afa` are supported).
+ *
+ * This includes parsing either from files or from other streams (strings, etc.).
+ */
 namespace Parser
 {
 

include/mata/re2parser.hh

@@ -22,6 +22,12 @@
 #include <mata/nfa.hh>
 
 namespace Mata {
+
+    /**
+     * Parser from regular expression to automata (currently `Nfa` and `Afa` are supported).
+     *
+     * TODO: Is this even needed? Could we move this to Mata::Parser?
+     */
     namespace RE2Parser {
         void create_nfa(Nfa::Nfa* nfa, const std::string &pattern, bool use_epsilon = false, int epsilon_value = 306, bool use_reduction = true);
     }

include/mata/rrt.hh

@@ -25,6 +25,14 @@
 
 namespace Mata
 {
+/**
+ * Restricted Register Transducer (over finite words) including structures and algorithms.
+ *
+ * These are restricted version of a (nondeterministic) register automaton that still has some
+ * decidable properties and closure under operations.
+ *
+ * TODO: Quite obsolete, should we remove this?
+ */
 namespace Rrt
 {
 

include/mata/util.hh

@@ -50,12 +50,31 @@
 #define DEBUG_VM_LOW_PRINT_LN(x) { PRINT_VERBOSE_LVL_LN(4, "debug VM", x); }
 #define WARN_PRINT(x) { PRINT_VERBOSE_LVL(1, "warning", x); }
 
+/**
+ * Main namespace including structs and algorithms for all automata.
+ *
+ * In particular, this includes:
+ *   1. Alphabets,
+ *   2. Formula graphs and nodes,
+ *   3. Mintermization,
+ *   4. Closed sets.
+ */
 namespace Mata
 {
 
 /// log verbosity
 extern unsigned LOG_VERBOSITY;
 
+/**
+ * Non-automata-related structures and algorithms.
+ *
+ * In particular, this includes:
+ *   1. Predicates,
+ *   2. Ordered Vectors,
+ *   3. Iterators,
+ *   4. Printers,
+ *   5. Other helper functions.
+ */
 namespace Util
 {