algo: reachable states for Z-Automata

alib2algo/src/automaton/properties/ReachableStates.cpp

 #include "ReachableStates.h"
+#include "automaton/TA/ArcFactoredDeterministicZAutomaton.h"
 #include <registration/AlgoRegistration.hpp>
 namespace {
@@ -59,4 +60,18 @@ Using closure implementation of the BFS algorithm.\n\
 @param fta automaton\n\
 @return set of reachable states from states that read leaves of @p fta" );
+auto ReachableStatesDAFZA = registration::AbstractRegister < automaton::properties::ReachableStates, ext::set < DefaultStateType >, const automaton::ArcFactoredDeterministicZAutomaton < > & > ( automaton::properties::ReachableStates::reachableStates, "dafza" ).setDocumentation (
+"Finds all reachable states of a arc-factored deterministic z-automaton.\n\
+Using closure implementation of the BFS algorithm.\n\
+\n\
+@param dafza automaton\n\
+@return set of reachable states from states that read leaves of @p dafza" );
+
+auto ReachableStatesNAFZA = registration::AbstractRegister < automaton::properties::ReachableStates, ext::set < DefaultStateType >, const automaton::ArcFactoredNondeterministicZAutomaton < > & > ( automaton::properties::ReachableStates::reachableStates, "nafza" ).setDocumentation (
+"Finds all reachable states of a arc-factored nondeterministic z-automaton.\n\
+Using closure implementation of the BFS algorithm.\n\
+\n\
+@param nafza automaton\n\
+@return set of reachable states from states that read leaves of @p nafza" );
+
 } /* namespace */

alib2algo/src/automaton/properties/ReachableStates.h

@@ -30,6 +30,8 @@
 #include <automaton/FSM/DFA.h>
 #include <automaton/TA/DFTA.h>
 #include <automaton/TA/NFTA.h>
+#include <automaton/TA/ArcFactoredDeterministicZAutomaton.h>
+#include <automaton/TA/ArcFactoredNondeterministicZAutomaton.h>
 namespace automaton {
@@ -73,6 +75,9 @@ public:
 	 */
 	template < class T >
 	static ext::require < isDFTA < T > || isNFTA < T >, ext::set < typename T::StateType > > reachableStates ( const T & fta );
+
+	template < class T >
+	static ext::require < isDAFZA < T > || isNAFZA < T >, ext::set < typename T::StateType > > reachableStates ( const T & afza );
 };
 template < class T >
@@ -151,6 +156,38 @@ ext::require < isDFTA < T > || isNFTA < T >, ext::set < typename T::StateType >
 	return Qi.at( i );
 }
+template < class T >
+ext::require < isDAFZA < T > || isNAFZA < T >, ext::set < typename T::StateType > > ReachableStates::reachableStates( const T & afza ) {
+	using StateType = typename T::StateType;
+	using SymbolType = typename T::SymbolType;
+
+	// 1a
+	ext::deque<ext::set<StateType>> Qi;
+	Qi.push_back( ext::set<StateType>( ) );
+
+	int i = 0;
+
+	// 1bc
+	do {
+		i = i + 1;
+
+		Qi.push_back( Qi.at( i - 1) );
+
+		for( const auto & transition : afza.getTransitions ( ) ) {
+			if ( transition.first.template is < SymbolType > ( ) ) {
+				Qi.at( i ).insert ( transition.second );
+			} else if ( transition.first.template is < ext::pair < StateType, StateType > > ( ) ) {
+				const auto& [q1, q2] = transition.first.template get < ext::pair < StateType, StateType > > ( );
+				if ( Qi.at ( i - 1 ).contains ( q1 ) && Qi.at ( i - 1 ).contains ( q2 ) ) {
+					Qi.at( i ).insert ( transition.second );
+				}
+			}
+		}
+	} while ( Qi.at( i ) != Qi.at( i - 1 ) );
+
+	return Qi.at( i );
+}
+
 } /* namespace properties */
 } /* namespace automaton */