diff --git a/alib2algo/src/automaton/transform/RHPDAToPDA.cpp b/alib2algo/src/automaton/transform/RHPDAToPDA.cpp index 0382ec32d684116e49f9af40ad555a1b169add16..caa08a288fc7cae5be7e8d50ac37dddb4ec3030d 100644 --- a/alib2algo/src/automaton/transform/RHPDAToPDA.cpp +++ b/alib2algo/src/automaton/transform/RHPDAToPDA.cpp @@ -22,6 +22,37 @@ namespace automaton { +template < class T > +void constructTransitions ( const std::tuple < automaton::State, alphabet::Symbol, std::vector < alphabet::Symbol > > & stFirst, const std::map < automaton::State, std::set < std::tuple < std::vector < alphabet::Symbol >, automaton::State, std::vector < alphabet::Symbol > > > > & epsilonTransitions, const automaton::State & toState, std::vector < alphabet::Symbol > pops, std::vector < alphabet::Symbol > pushes, T & res ) { + auto epsIter = epsilonTransitions.find ( toState ); + + if ( ( epsIter != epsilonTransitions.end ( ) ) && !epsIter->second.empty ( ) ) { + if ( epsIter->second.size ( ) == 1 ) { + const auto & epsilonT = * epsIter->second.begin ( ); + + pops.insert ( pops.end ( ), std::get < 0 > ( epsilonT ).begin ( ), std::get < 0 > ( epsilonT ).end ( ) ); + pushes.insert ( pushes.begin ( ), std::get < 2 > ( epsilonT ).rbegin ( ), std::get < 2 > ( epsilonT ).rend ( ) ); + + constructTransitions ( stFirst, epsilonTransitions, std::get < 1 > ( epsilonT ), std::move ( pops ), std::move ( pushes ), res ); + } else { + for ( const auto & epsilonT : epsIter->second ) { + std::vector < alphabet::Symbol > popsCopy = pops; + std::vector < alphabet::Symbol > pushesCopy = pushes; + + popsCopy.insert ( popsCopy.end ( ), std::get < 0 > ( epsilonT ).begin ( ), std::get < 0 > ( epsilonT ).end ( ) ); + pushesCopy.insert ( pushesCopy.begin ( ), std::get < 2 > ( epsilonT ).rbegin ( ), std::get < 2 > ( epsilonT ).rend ( ) ); + + constructTransitions ( stFirst, epsilonTransitions, std::get < 1 > ( epsilonT ), std::move ( popsCopy ), std::move ( pushesCopy ), res ); + } + } + } else { + res.addState ( std::get < 0 > ( stFirst ) ); + res.addState ( toState ); + + res.addTransition ( std::get < 0 > ( stFirst ), std::get < 1 > ( stFirst ), std::move ( pops ), toState, std::move ( pushes ) ); + } +} + automaton::DPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterministicDPDA & pda ) { std::map < std::tuple < automaton::State, alphabet::Symbol, std::vector < alphabet::Symbol > >, std::set < std::pair < automaton::State, std::vector < alphabet::Symbol > > > > readingTransitions; std::map < automaton::State, std::set < std::tuple < std::vector < alphabet::Symbol >, automaton::State, std::vector < alphabet::Symbol > > > > epsilonTransitions; @@ -64,19 +95,28 @@ automaton::DPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist } } - for ( const auto & st : epsilonTransitions ) - if ( st.second.size ( ) != 1 ) throw exception::AlibException ( "Temporary states has more than one leaving transition" ); + for ( const auto & st : epsilonTransitions ) { + bool allPops = true; + + for ( const auto & elems : st.second ) + allPops &= std::get < 2 > ( elems ).empty ( ); // if some pushes it will clear allPops variable + + if ( st.second.size ( ) == 1 ) continue; + + if ( ( st.second.size ( ) > 1 ) && allPops ) continue; + + throw exception::AlibException ( "Temporary states has more than one leaving transition" ); + } if ( epsilonTransitions[pda.getInitialState ( )].empty ( ) ) throw exception::AlibException ( "Cannot determine initial pushdown store symbol" ); - const auto & st = * epsilonTransitions[pda.getInitialState ( )].begin ( ); + // -------------------------------------------------------------------- initial state and initial stack symbol - std::vector < alphabet::Symbol > pops; - std::vector < alphabet::Symbol > pushes; + const auto & st = * epsilonTransitions[pda.getInitialState ( )].begin ( ); - pops.insert ( pops.end ( ), std::get < 0 > ( st ).begin ( ), std::get < 0 > ( st ).end ( ) ); - pushes.insert ( pushes.begin ( ), std::get < 2 > ( st ).rbegin ( ), std::get < 2 > ( st ).rend ( ) ); + std::vector < alphabet::Symbol > pops ( std::get < 0 > ( st ).begin ( ), std::get < 0 > ( st ).end ( ) ); + std::vector < alphabet::Symbol > pushes ( std::get < 2 > ( st ).rbegin ( ), std::get < 2 > ( st ).rend ( ) ); automaton::State toState = std::get < 1 > ( st ); @@ -92,6 +132,8 @@ automaton::DPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist if ( ( pops.size ( ) != 0 ) && ( pushes.size ( ) != 1 ) ) throw exception::AlibException ( "Cannot convert" ); + // -------------------------------------------------------------------- initial state and initial stack symbol + automaton::DPDA res ( toState, pushes[0] ); res.setInputAlphabet ( pda.getInputAlphabet ( ) ); @@ -100,27 +142,10 @@ automaton::DPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist for ( const auto & st : readingTransitions ) for ( const auto & to : st.second ) { - std::vector < alphabet::Symbol > pops; - std::vector < alphabet::Symbol > pushes; - - pops.insert ( pops.end ( ), std::get < 2 > ( st.first ).begin ( ), std::get < 2 > ( st.first ).end ( ) ); - pushes.insert ( pushes.begin ( ), to.second.rbegin ( ), to.second.rend ( ) ); - - automaton::State toState = to.first; + std::vector < alphabet::Symbol > pops ( std::get < 2 > ( st.first ).begin ( ), std::get < 2 > ( st.first ).end ( ) ); + std::vector < alphabet::Symbol > pushes ( to.second.rbegin ( ), to.second.rend ( ) ); - while ( !epsilonTransitions[toState].empty ( ) ) { - const auto & epsilonT = * epsilonTransitions[toState].begin ( ); - - pops.insert ( pops.end ( ), std::get < 0 > ( epsilonT ).begin ( ), std::get < 0 > ( epsilonT ).end ( ) ); - pushes.insert ( pushes.begin ( ), std::get < 2 > ( epsilonT ).rbegin ( ), std::get < 2 > ( epsilonT ).rend ( ) ); - - toState = std::get < 1 > ( epsilonT ); - } - - res.addState ( std::get < 0 > ( st.first ) ); - res.addState ( toState ); - - res.addTransition ( std::get < 0 > ( st.first ), std::get < 1 > ( st.first ), pops, toState, pushes ); + constructTransitions ( st.first, epsilonTransitions, to.first, std::move ( pops ), std::move ( pushes ), res ); } res.setFinalStates ( pda.getFinalStates ( ) ); @@ -185,8 +210,14 @@ automaton::NPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist } } - for ( const auto & st : epsilonTransitions ) - if ( st.second.size ( ) != 1 ) throw exception::AlibException ( "Temporary states has more than one leaving transition" ); + for ( const auto & st : epsilonTransitions ) { + bool allPops = true; + + for ( const auto & elems : st.second ) + allPops &= std::get < 2 > ( elems ).empty ( ); // if some pushes it will clear allPops variable + + if ( ( st.second.size ( ) != 1 ) && !allPops ) throw exception::AlibException ( "Temporary states has more than one leaving transition" ); + } if ( pda.getInitialStates ( ).size ( ) != 1 ) throw exception::AlibException ( "Cannot convert" ); @@ -196,14 +227,12 @@ automaton::NPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist if ( epsilonTransitions[initialState].empty ( ) ) throw exception::AlibException ( "Cannot convert" ); - // -------------------------------------------------------------------- initial state and initial stack symbol - const auto & st = * epsilonTransitions[initialState].begin ( ); + // -------------------------------------------------------------------- initial state and initial stack symbol - std::vector < alphabet::Symbol > pops; - std::vector < alphabet::Symbol > pushes; + const auto & st = * epsilonTransitions[initialState].begin ( ); - pops.insert ( pops.end ( ), std::get < 0 > ( st ).begin ( ), std::get < 0 > ( st ).end ( ) ); - pushes.insert ( pushes.begin ( ), std::get < 2 > ( st ).rbegin ( ), std::get < 2 > ( st ).rend ( ) ); + std::vector < alphabet::Symbol > pops ( std::get < 0 > ( st ).begin ( ), std::get < 0 > ( st ).end ( ) ); + std::vector < alphabet::Symbol > pushes ( std::get < 2 > ( st ).rbegin ( ), std::get < 2 > ( st ).rend ( ) ); automaton::State toState = std::get < 1 > ( st ); @@ -229,27 +258,10 @@ automaton::NPDA RHPDAToPDA::convert ( const automaton::RealTimeHeightDeterminist for ( const auto & st : readingTransitions ) for ( const auto & to : st.second ) { - std::vector < alphabet::Symbol > pops; - std::vector < alphabet::Symbol > pushes; - - pops.insert ( pops.end ( ), std::get < 2 > ( st.first ).begin ( ), std::get < 2 > ( st.first ).end ( ) ); - pushes.insert ( pushes.begin ( ), to.second.rbegin ( ), to.second.rend ( ) ); - - automaton::State toState = to.first; - - while ( !epsilonTransitions[toState].empty ( ) ) { - const auto & epsilonT = * epsilonTransitions[toState].begin ( ); - - pops.insert ( pops.end ( ), std::get < 0 > ( epsilonT ).begin ( ), std::get < 0 > ( epsilonT ).end ( ) ); - pushes.insert ( pushes.begin ( ), std::get < 2 > ( epsilonT ).rbegin ( ), std::get < 2 > ( epsilonT ).rend ( ) ); - - toState = std::get < 1 > ( epsilonT ); - } - - res.addState ( std::get < 0 > ( st.first ) ); - res.addState ( toState ); + std::vector < alphabet::Symbol > pops ( std::get < 2 > ( st.first ).begin ( ), std::get < 2 > ( st.first ).end ( ) ); + std::vector < alphabet::Symbol > pushes ( to.second.rbegin ( ), to.second.rend ( ) ); - res.addTransition ( std::get < 0 > ( st.first ), std::get < 1 > ( st.first ), pops, toState, pushes ); + constructTransitions ( st.first, epsilonTransitions, to.first, std::move ( pops ), std::move ( pushes ), res ); } res.setFinalStates ( pda.getFinalStates ( ) );