diff --git a/alib2data/src/automaton/PDA/DPDA.h b/alib2data/src/automaton/PDA/DPDA.h
index fe3d46ff626b83a0c0e131df0740314e8e2c5c9a..76029dfddc43b0c4eaf8bbd216b88b577f491dae 100644
--- a/alib2data/src/automaton/PDA/DPDA.h
+++ b/alib2data/src/automaton/PDA/DPDA.h
@@ -54,7 +54,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol,
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a \times \alpha -> B \times \beta, where A, B \in Q, a \in T \cup { \eps }, and \alpha, \beta \in G*,
diff --git a/alib2data/src/automaton/PDA/InputDrivenDPDA.h b/alib2data/src/automaton/PDA/InputDrivenDPDA.h
index 21e27b3dc1dabaf555354f01d9215fd12ceba364..443d7b5d194c4f8395d2bc789c81c18b2fbc0bfc 100644
--- a/alib2data/src/automaton/PDA/InputDrivenDPDA.h
+++ b/alib2data/src/automaton/PDA/InputDrivenDPDA.h
@@ -56,7 +56,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, \zeta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol,
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a -> B, where A, B \in Q and a \in T,
diff --git a/alib2data/src/automaton/PDA/InputDrivenNPDA.h b/alib2data/src/automaton/PDA/InputDrivenNPDA.h
index 1779edba8c62a1d0de60b147e0feca62d1f6738e..7991f9d9a4f86922833e741b313c9d6a5dbe8a64 100644
--- a/alib2data/src/automaton/PDA/InputDrivenNPDA.h
+++ b/alib2data/src/automaton/PDA/InputDrivenNPDA.h
@@ -56,7 +56,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, \zeta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to NFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol,
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a -> P(Q), where A \in Q, a \in T, and P(Q) is a powerset of states,
diff --git a/alib2data/src/automaton/PDA/NPDA.h b/alib2data/src/automaton/PDA/NPDA.h
index f029d6ee132ed09799816de9b9970b0683615c46..a17be011e7139354f97479f4e5c0bc343f8364b1 100644
--- a/alib2data/src/automaton/PDA/NPDA.h
+++ b/alib2data/src/automaton/PDA/NPDA.h
@@ -55,7 +55,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol,
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a \times \alpha -> B \times \beta, where A, B \in Q, a \in T \cup { \eps }, and \alpha, \beta \in G*,
diff --git a/alib2data/src/automaton/PDA/NPDTA.h b/alib2data/src/automaton/PDA/NPDTA.h
index e20f800e741dd057107f35e8c9d86d8a4b8934da..bd8deff0a6d4a7b36f2a2c7e4365d9552a34cce1 100644
--- a/alib2data/src/automaton/PDA/NPDTA.h
+++ b/alib2data/src/automaton/PDA/NPDTA.h
@@ -55,7 +55,7 @@ class InitialState;
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
  * T (OutputAlphabet) = finite set of output symbols - having this empty won't let automaton do translation at all,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol,
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a \times \alpha -> B \times \beta \times \gamma, where A, B \in Q, a \in T \cup { \eps }, \alpha, \beta \in G*, and \gamma \in D*,
diff --git a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
index 889657e50502931a6061b2d6a87180a557f40463..f0f63ffb75ad1c913552c193d76e9aee56b5ca41 100644
--- a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
+++ b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
@@ -54,7 +54,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialState) = initial state,
  * Z (BottomOfTheStackSymbol) = initial pushdown store symbol
  * \delta is split to three disjoint parts
diff --git a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicNPDA.h b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicNPDA.h
index 02c4a491c3e000a8b9e02b287fd01f4c833187d5..5bbef5aa090054a9fdb357c1c079a7382952cad7 100644
--- a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicNPDA.h
+++ b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicNPDA.h
@@ -54,7 +54,7 @@ class InitialStates;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialState) = initial state,
  * Z (BottomOfTheStackSymbol) = initial pushdown store symbol
  * \delta is split to three disjoint parts
diff --git a/alib2data/src/automaton/PDA/SinglePopDPDA.h b/alib2data/src/automaton/PDA/SinglePopDPDA.h
index 005b468efc141cf5a355fde784839aa8f4ce46df..d7eeed4869bfcbde82add3df6954336e636bd609 100644
--- a/alib2data/src/automaton/PDA/SinglePopDPDA.h
+++ b/alib2data/src/automaton/PDA/SinglePopDPDA.h
@@ -55,7 +55,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a \times g -> B \times \beta, where A, B \in Q, a \in T \cup { \eps }, g \in G, and \beta \in G*,
diff --git a/alib2data/src/automaton/PDA/SinglePopNPDA.h b/alib2data/src/automaton/PDA/SinglePopNPDA.h
index 7d110f20dc89cbb0fdee9bb6471fbcd36e6e7305..c5e91897b70f16e0c0f91dd7be9fbc98026aeebd 100644
--- a/alib2data/src/automaton/PDA/SinglePopNPDA.h
+++ b/alib2data/src/automaton/PDA/SinglePopNPDA.h
@@ -53,7 +53,7 @@ class InitialState;
  * A = (Q, T, G, I, Z, \delta, F),
  * Q (States) = nonempty finite set of states,
  * T (TerminalAlphabet) = finite set of terminal symbols - having this empty won't let automaton do much though,
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialState) = initial state,
  * Z (InitialPushdownStoreSymbol) = initial pushdown store symbol
  * \delta = transition function of the form A \times a \times g -> B \times \beta, where A, B \in Q, a \in T \cup { \eps }, g \in G, and \beta \in G*,
diff --git a/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h
index 28a1360969856d38a99967dc58e4abbb5f400a52..f13ebcf6c9a00d913d984b5756b4249d5de98c01 100644
--- a/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h
+++ b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h
@@ -59,7 +59,7 @@ class InitialState;
  *   - C (CallAlphabet) = symbols used with transitions increasing the pushdown store,
  *   - R (ReturnAlphabet) = symbols used with transitions decreasing the pushdown store,
  *   - L (LocalAlphabet) = symbols used with transitions leaving the height of the pushdown store unchanged
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialState) = initial state,
  * Z (BottomOfTheStackSymbol) = initial pushdown store symbol
  * \delta is split to three disjoint parts
diff --git a/alib2data/src/automaton/PDA/VisiblyPushdownNPDA.h b/alib2data/src/automaton/PDA/VisiblyPushdownNPDA.h
index 1fa9524673d8f07297554f1f195d17c45dbfb456..3f2caf7b34be420b38b7580c93998e74f9dd1735 100644
--- a/alib2data/src/automaton/PDA/VisiblyPushdownNPDA.h
+++ b/alib2data/src/automaton/PDA/VisiblyPushdownNPDA.h
@@ -59,7 +59,7 @@ class InitialStates;
  *   - C (CallAlphabet) = symbols used with transitions increasing the pushdown store,
  *   - R (ReturnAlphabet) = symbols used with transitions decreasing the pushdown store,
  *   - L (LocalAlphabet) = symbols used with transitions leaving the height of the pushdown store unchanged
- * G (PushdownStoreAlphabet) = finite set of pushdown store symbol - having this empty makes the automaton equivalent to DFA
+ * G (PushdownStoreAlphabet) = finite set of pushdown store symbol
  * I (InitialStates) = set of initial states,
  * Z (BottomOfTheStackSymbol) = initial pushdown store symbol
  * \delta is split to three disjoint parts
diff --git a/alib2data/src/automaton/TA/EpsilonNFTA.h b/alib2data/src/automaton/TA/EpsilonNFTA.h
index 7eb4e5606b827cf8028ef4da92d1e0e8c11bb280..96461f46160478bc34084c5a1b5a460624e19a56 100644
--- a/alib2data/src/automaton/TA/EpsilonNFTA.h
+++ b/alib2data/src/automaton/TA/EpsilonNFTA.h
@@ -494,7 +494,7 @@ template < class T >
 class isEpsilonNFTA_impl : public std::false_type {};
 
 /**
- * Trait to detect whether the type parameter T is or is not DFA. Derived from std::true_type.
+ * Trait to detect whether the type parameter T is or is not EpsilonNFTA. Derived from std::true_type.
  *
  * Specialisation for EpsilonNFTA.
  *
diff --git a/alib2data/src/automaton/TA/NFTA.h b/alib2data/src/automaton/TA/NFTA.h
index d10c1f5ccfa33e1061858be4448f3ac5faefb70d..0889d259d9f83303aaa052af8dcf58d75f63d498 100644
--- a/alib2data/src/automaton/TA/NFTA.h
+++ b/alib2data/src/automaton/TA/NFTA.h
@@ -385,7 +385,7 @@ template < class T >
 class isNFTA_impl : public std::false_type {};
 
 /**
- * Trait to detect whether the type parameter T is or is not DFA. Derived from std::true_type.
+ * Trait to detect whether the type parameter T is or is not NFTA. Derived from std::true_type.
  *
  * Specialisation for NFTA.
  *
diff --git a/alib2data/src/automaton/TA/UnorderedNFTA.h b/alib2data/src/automaton/TA/UnorderedNFTA.h
index 003d1d3fcb9fab17e9ea3ba12179671c005e8fe1..0f3a8a197ba4552184eada4016f08ea553dca57e 100644
--- a/alib2data/src/automaton/TA/UnorderedNFTA.h
+++ b/alib2data/src/automaton/TA/UnorderedNFTA.h
@@ -385,7 +385,7 @@ template < class T >
 class isUnorderedNFTA_impl : public std::false_type {};
 
 /**
- * Trait to detect whether the type parameter T is or is not DFA. Derived from std::true_type.
+ * Trait to detect whether the type parameter T is or is not UnorderedNFTA. Derived from std::true_type.
  *
  * Specialisation for UnorderedNFTA.
  *