diff --git a/adeterminize2/src/adeterminize.cpp b/adeterminize2/src/adeterminize.cpp index 780b1ceb7a0c60357861a7f156d48ee342b8f36b..126f52b6036de331276b5155aa76fba06b231283 100644 --- a/adeterminize2/src/adeterminize.cpp +++ b/adeterminize2/src/adeterminize.cpp @@ -6,20 +6,15 @@ #include "automaton/Automaton.h" #include "automaton/FSM/NFA.h" #include "automaton/FSM/DFA.h" -//#include "automaton/PDA/PDA.h" +#include "automaton/PDA/NPDA.h" #include "factory/DataFactory.hpp" #include "exception/AlibException.h" #include "determinize/nfa/NFADeterminizer.h" #include "determinize/idpda/IDPDADeterminizer.h" #include "determinize/vpa/VPADeterminizer.h" -//#include "vpa/VpaDeterminizer.h" -//#include "vpa/VpaDeterminizer2.h" -//#include "vpa/VpaDeterminizer3.h" -//#include "rhdpda/RhdpdaDeterminizer.h" -//#include "rhdpda/RhdpdaDeterminizer2.h" -//#include "rhdpda/RhdpdaDeterminizer3.h" -//#include "rhdpda/RhdpdaDeterminizer4.h" +#include "automaton/PDAToRHPDA.h" +#include "automaton/RHPDAToPDA.h" #define VERSION "0.0.1" @@ -28,12 +23,6 @@ #define TYPE_VPA "vpa" #define TYPE_RHDPDA "rhdpda" -#define VERSION_1 "1" -#define VERSION_2 "2" -#define VERSION_3 "3" -#define VERSION_4 "4" - - /** * Prints help to standard output. */ @@ -43,7 +32,6 @@ void printHelp() { std::cout << "Usage: adeterminize -t TYPE [SWITCH...]" << std::endl; std::cout << "Possible arguments:" << std::endl; std::cout << " -t, --type=TYPE \t Specifies type of input automaton, possible values are 'FSM' for final-state machine, 'IDPDA' for input-driven pushdown automaton, 'VPA' for visible pushdown automaton and 'RHDPDA' for real-time height deterministic pushdown automaton." << std::endl; - std::cout << " -a, --algorithm=VERSION_OF_ALGORITHM \t Specifies version of algorithm. This argument works only with VPA or RHDPDA type. VPA determinization has 3 versions (use numbers 1, 2 and 3) and RHDPDA determinization has 4 versions (use numbers 1, 2, 3 and 4). Default value is always number 1." << std::endl; std::cout << " -h, --help \t Displays this help message." << std::endl; std::cout << std::endl; } @@ -125,11 +113,13 @@ int main(int argc, char** argv) { automaton::VisiblyPushdownNPDA dpda = determinize::VPADeterminizer::determinize(npda); alib::DataFactory::toStdout(dpda); return 0; - } -/* } else if (type == TYPE_RHDPDA) { - return getRhdpdaDeterminizer(automaton, version); - }*/ + automaton::NPDA npda = alib::DataFactory::fromTokens<automaton::NPDA>(tokens); + automaton::RealTimeHeightDeterministicNPDA rhpda = automaton::PDAToRHPDA::convert(npda); + automaton::NPDA npda2 = automaton::RHPDAToPDA::convert(rhpda); + alib::DataFactory::toStdout(npda2); + return 0; + } printHelp(); // should not be reached return 2; diff --git a/alib2algo/src/automaton/PDAToRHPDA.cpp b/alib2algo/src/automaton/PDAToRHPDA.cpp index ab9e561e3e9f77f27f87776490c914703cef7c21..ed76fbebf069f222ee40f94394ce76305360c1c1 100644 --- a/alib2algo/src/automaton/PDAToRHPDA.cpp +++ b/alib2algo/src/automaton/PDAToRHPDA.cpp @@ -29,7 +29,9 @@ automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton: res.setInputSymbols(pda.getInputAlphabet()); res.setStates(pda.getStates()); res.setFinalStates(pda.getFinalStates()); - res.setStackSymbols(pda.getStackAlphabet()); + std::set<alphabet::Symbol> stackSymbols = pda.getStackAlphabet(); + stackSymbols.insert( alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } ); + res.setStackSymbols(stackSymbols); automaton::State q0 = automaton::createUniqueState(automaton::State("q0"), res.getStates()); res.addState(q0); @@ -39,6 +41,8 @@ automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton: for(const alphabet::Symbol& symbol : pda.getInitialSymbols()) res.addCallTransition(q0, state, symbol); + std::string us("us"); + int i = 0; for(const auto& transition : pda.getTransitions()) { for(const auto& to : transition.second) { if(std::get<2>(transition.first).size() == 0 && to.second.size() == 0) @@ -51,9 +55,11 @@ automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton: int popPushIndex = 0; int popPushSymbols = std::get<2>(transition.first).size() + to.second.size(); + automaton::State lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(i)), res.getStates()); for(const alphabet::Symbol& pop : std::get<2>(transition.first)) { - automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : automaton::createUniqueState(automaton::State("us"), res.getStates()); - automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : automaton::createUniqueState(automaton::State("us"), res.getStates()); + automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS; + if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates()); + automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS; res.addState(fromState); res.addState(toState); @@ -65,8 +71,9 @@ automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton: popPushIndex++; } for(const alphabet::Symbol& push : to.second) { - automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : automaton::createUniqueState(automaton::State("us"), res.getStates()); - automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : automaton::createUniqueState(automaton::State("us"), res.getStates()); + automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS; + if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates()); + automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS; res.addState(fromState); res.addState(toState); diff --git a/alib2algo/src/automaton/RHPDAToPDA.cpp b/alib2algo/src/automaton/RHPDAToPDA.cpp new file mode 100644 index 0000000000000000000000000000000000000000..cc3924ef35d20d2a5b4076c2c5d7c9206e7e3ec5 --- /dev/null +++ b/alib2algo/src/automaton/RHPDAToPDA.cpp @@ -0,0 +1,211 @@ +/* + * RHPDAToPDA.cpp + * + * Created on: 23. 3. 2014 + * Author: Jan Travnicek + */ + +#include "RHPDAToPDA.h" + +#include <exception/AlibException.h> +#include <automaton/PDA/RealTimeHeightDeterministicNPDA.h> +#include <automaton/PDA/NPDA.h> + +#include <alphabet/BottomOfTheStackSymbol.h> + +#include <set> +#include <map> +#include <queue> +#include <iostream> + +namespace automaton { + +automaton::NPDA RHPDAToPDA::convert( const automaton::RealTimeHeightDeterministicNPDA & pda ) { + automaton::NPDA res; + + res.setInputSymbols(pda.getInputAlphabet()); + + res.setStackSymbols(pda.getStackAlphabet()); + + 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; + + for(const auto& transition : pda.getCallTransitions()) { + if(std::get<1>(transition.first).is<string::Epsilon>()) { + auto& epsT = epsilonTransitions[std::get<0>(transition.first)]; + for(const auto& to : transition.second) { + if(to.second.getData() == alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK) throw exception::AlibException("Cannot convert"); + epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{}, to.first, std::vector<alphabet::Symbol>{to.second})); + } + } else { + auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{})]; + for(const auto& to : transition.second) { + readT.insert(std::make_pair(to.first, std::vector<alphabet::Symbol>{to.second})); + } + } + } + + for(const auto& transition : pda.getLocalTransitions()) { + if(std::get<1>(transition.first).is<string::Epsilon>()) { + auto& epsT = epsilonTransitions[std::get<0>(transition.first)]; + for(const auto& to : transition.second) { + epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{}, to, std::vector<alphabet::Symbol>{})); + } + } else { + auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{})]; + for(const auto& to : transition.second) { + readT.insert(std::make_pair(to, std::vector<alphabet::Symbol>{})); + } + } + } + + for(const auto& transition : pda.getReturnTransitions()) { + if(std::get<1>(transition.first).is<string::Epsilon>()) { + auto& epsT = epsilonTransitions[std::get<0>(transition.first)]; + for(const auto& to : transition.second) { + if(std::get<2>(transition.first).getData() == alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK) throw exception::AlibException("Cannot convert"); + epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{std::get<2>(transition.first)}, to, std::vector<alphabet::Symbol>{})); + } + } else { + auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{std::get<2>(transition.first)})]; + for(const auto& to : transition.second) { + readT.insert(std::make_pair(to, std::vector<alphabet::Symbol>{})); + } + } + } + + 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 : 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.end(), to.second.begin(), to.second.end()); + + 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.end(), std::get<2>(epsilonT).begin(), std::get<2>(epsilonT).end()); + + 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); + } + } + + if(pda.getInitialStates().size() != 1) + throw exception::AlibException("Cannot convert"); + + for(const automaton::State& initialState : pda.getInitialStates()) { + if(!epsilonTransitions[initialState].empty()) { + const auto& st = *epsilonTransitions[initialState].begin(); + + std::vector<alphabet::Symbol> pops; + std::vector<alphabet::Symbol> pushes; + + pops.insert(pops.end(), std::get<0>(st).begin(), std::get<0>(st).end()); + pushes.insert(pushes.end(), std::get<2>(st).begin(), std::get<2>(st).end()); + + automaton::State toState = std::get<1>(st); + 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.end(), std::get<2>(epsilonT).begin(), std::get<2>(epsilonT).end()); + + toState = std::get<1>(epsilonT); + } + res.addState(toState); + + if(pops.size() != 0 && pushes.size() != 1) + throw exception::AlibException("Cannot convert"); + + res.setInitialStates({toState}); + res.setInitialSymbols({pushes[0]}); + } + } + + res.setFinalStates(pda.getFinalStates()); + + return res; +} + +automaton::Automaton RHPDAToPDA::convert(const Automaton& automaton) { + automaton::Automaton* out = NULL; + automaton.getData().Accept((void*) &out, RHPDAToPDA::RHPDA_TO_PDA); + automaton::Automaton res(std::move(*out)); + delete out; + return std::move(res); +} + +void RHPDAToPDA::Visit(void*, const UnknownAutomaton&) const { + throw exception::AlibException("Unsupported automaton type UnknownAutomaton"); +} + +void RHPDAToPDA::Visit(void*, const EpsilonNFA&) const { + throw exception::AlibException("Unsupported automaton type EpsilonNFA"); +} + +void RHPDAToPDA::Visit(void*, const NFA&) const { + throw exception::AlibException("Unsupported automaton type NFA"); +} + +void RHPDAToPDA::Visit(void*, const DFA&) const { + throw exception::AlibException("Unsupported automaton type DFA"); +} + +void RHPDAToPDA::Visit(void*, const ExtendedNFA&) const { + throw exception::AlibException("Unsupported automaton type ExtendedDFA"); +} + +void RHPDAToPDA::Visit(void*, const CompactNFA&) const { + throw exception::AlibException("Unsupported automaton type CompactNFA"); +} + +void RHPDAToPDA::Visit(void*, const DPDA&) const { + throw exception::AlibException("Unsupported automaton type DPDA"); +} + +void RHPDAToPDA::Visit(void*, const SinglePopDPDA&) const { + throw exception::AlibException("Unsupported automaton type SinglePopDPDA"); +} + +void RHPDAToPDA::Visit(void*, const InputDrivenNPDA&) const { + throw exception::AlibException("Unsupported automaton type InputDrivenNPDA"); +} + +void RHPDAToPDA::Visit(void*, const VisiblyPushdownNPDA&) const { + throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA"); +} + +void RHPDAToPDA::Visit(void* data, const RealTimeHeightDeterministicNPDA& automaton) const { + automaton::Automaton*& out = *((automaton::Automaton**) data); + out = new automaton::Automaton(this->convert(automaton)); +} + +void RHPDAToPDA::Visit(void*, const NPDA&) const { + throw exception::AlibException("Unsupported automaton type NPDA"); +} + +void RHPDAToPDA::Visit(void*, const SinglePopNPDA&) const { + throw exception::AlibException("Unsupported automaton type SinglePopNPDA"); +} + +void RHPDAToPDA::Visit(void*, const OneTapeDTM&) const { + throw exception::AlibException("Unsupported automaton type OneTapeDTM"); +} + +const RHPDAToPDA RHPDAToPDA::RHPDA_TO_PDA; + +} + diff --git a/alib2algo/src/automaton/RHPDAToPDA.h b/alib2algo/src/automaton/RHPDAToPDA.h new file mode 100644 index 0000000000000000000000000000000000000000..2bc2ef9e42104e231e7095ac8ff03ffefeb75443 --- /dev/null +++ b/alib2algo/src/automaton/RHPDAToPDA.h @@ -0,0 +1,50 @@ +/* + * RHPDAToPDA.h + * + * Created on: 23. 3. 2014 + * Author: Jan Travnicek + */ + +#ifndef RHPDA_TO_PDA_H_ +#define RHPDA_TO_PDA_H_ + +#include <algorithm> +#include <deque> +#include <set> + +#include "automaton/Automaton.h" +#include <automaton/common/State.h> + +namespace automaton { + +class RHPDAToPDA : public VisitableAutomatonBase::const_visitor_type { +public: + static automaton::NPDA convert( const automaton::RealTimeHeightDeterministicNPDA & pda); + static automaton::NPDA convert( const automaton::NPDA & pda); + + /** + * Computes epsilon closure of a state in epsilon nonfree automaton + */ + static automaton::Automaton convert( const automaton::Automaton & automaton ); +private: + void Visit(void*, const UnknownAutomaton& automaton) const; + void Visit(void*, const EpsilonNFA& automaton) const; + void Visit(void*, const NFA& automaton) const; + void Visit(void*, const DFA& automaton) const; + void Visit(void*, const ExtendedNFA& automaton) const; + void Visit(void*, const CompactNFA& automaton) const; + void Visit(void*, const DPDA& automaton) const; + void Visit(void*, const SinglePopDPDA& automaton) const; + void Visit(void*, const InputDrivenNPDA& automaton) const; + void Visit(void*, const VisiblyPushdownNPDA& automaton) const; + void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const; + void Visit(void*, const NPDA& automaton) const; + void Visit(void*, const SinglePopNPDA& automaton) const; + void Visit(void*, const OneTapeDTM& automaton) const; + + static const RHPDAToPDA RHPDA_TO_PDA; +}; + +} + +#endif /* RHPDA_TO_PDA_H_ */ diff --git a/alib2data/test-src/automaton/AutomatonTest.cpp b/alib2data/test-src/automaton/AutomatonTest.cpp index 856d67b0fb5c53b700efb268cbd3ca5affeaac58..4ad07395882056271f094dab6d8b435d95313ad5 100644 --- a/alib2data/test-src/automaton/AutomatonTest.cpp +++ b/alib2data/test-src/automaton/AutomatonTest.cpp @@ -284,6 +284,41 @@ void AutomatonTest::testExtendedNFAAlphabet() { CPPUNIT_ASSERT_NO_THROW(automaton.addTransition(s0, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpEpsilon())}, s1)); } +void AutomatonTest::testNPDATransitions() { + automaton::NPDA automaton; + + automaton.setStates({automaton::State(0), automaton::State(1), automaton::State(2), automaton::State(3), automaton::State(4)}); + automaton.setInitialStates({automaton::State(0)}); + automaton.setInputSymbols({alphabet::symbolFrom("a2"), alphabet::symbolFrom("a1"), alphabet::symbolFrom("a0")}); + automaton.setStackSymbols({alphabet::symbolFrom("T"), alphabet::symbolFrom("R")}); + automaton.setInitialSymbols({alphabet::symbolFrom("T")}); + + automaton.addTransition(automaton::State(0), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("T")}, automaton::State(0), {alphabet::symbolFrom("T"), alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(0), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("T")}, automaton::State(0), {alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(0), alphabet::symbolFrom("a0"), {alphabet::symbolFrom("T")}, automaton::State(0), {}); + + automaton.addTransition(automaton::State(0), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("T")}, automaton::State(1), {alphabet::symbolFrom("R"), alphabet::symbolFrom("T")}); + + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("T")}, automaton::State(1), {alphabet::symbolFrom("T"), alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("R")}, automaton::State(1), {alphabet::symbolFrom("T"), alphabet::symbolFrom("R")}); + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("T")}, automaton::State(1), {alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("R")}, automaton::State(1), {alphabet::symbolFrom("R")}); + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a0"), {alphabet::symbolFrom("T")}, automaton::State(1), {}); + automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a0"), {alphabet::symbolFrom("R")}, automaton::State(2), {}); + + automaton.addTransition(automaton::State(2), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("T")}, automaton::State(3), {alphabet::symbolFrom("R")}); + + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("T")}, automaton::State(3), {alphabet::symbolFrom("T"), alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a2"), {alphabet::symbolFrom("R")}, automaton::State(3), {alphabet::symbolFrom("T"), alphabet::symbolFrom("R")}); + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("T")}, automaton::State(3), {alphabet::symbolFrom("T")}); + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a1"), {alphabet::symbolFrom("R")}, automaton::State(3), {alphabet::symbolFrom("R")}); + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a0"), {alphabet::symbolFrom("T")}, automaton::State(3), {}); + automaton.addTransition(automaton::State(3), alphabet::symbolFrom("a0"), {alphabet::symbolFrom("R")}, automaton::State(4), {}); + + automaton.setFinalStates({automaton::State(4)}); + alib::DataFactory::toStdout(automaton); +} + void AutomatonTest::testRHPDATransitions() { automaton::RealTimeHeightDeterministicNPDA automaton(alphabet::Symbol(alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK)); automaton.setStates({automaton::State(1), automaton::State(2), automaton::State(3)}); diff --git a/alib2data/test-src/automaton/AutomatonTest.h b/alib2data/test-src/automaton/AutomatonTest.h index c4c2a6ba303ed3013eec4d6ef93fc9ec86bffb41..87d1ce8104b813f67fed926fc928c1e48825d8ff 100644 --- a/alib2data/test-src/automaton/AutomatonTest.h +++ b/alib2data/test-src/automaton/AutomatonTest.h @@ -13,6 +13,7 @@ class AutomatonTest : public CppUnit::TestFixture CPPUNIT_TEST( DPDATransitions ); CPPUNIT_TEST( testExtendedNFAAlphabet ); CPPUNIT_TEST( testRHPDATransitions ); + CPPUNIT_TEST( testNPDATransitions ); CPPUNIT_TEST_SUITE_END(); public: @@ -26,6 +27,7 @@ public: void DPDATransitions(); void testExtendedNFAAlphabet(); void testRHPDATransitions(); + void testNPDATransitions(); }; #endif // AUTOMATON_TEST_H_ diff --git a/examples2/automaton/NPDA.xml b/examples2/automaton/NPDA.xml new file mode 100644 index 0000000000000000000000000000000000000000..3fcd608678079187dd2eac10854d1d314d736c89 --- /dev/null +++ b/examples2/automaton/NPDA.xml @@ -0,0 +1,431 @@ +<?xml version="1.0"?> +<NPDA> + <states> + <IntegerLabel>0</IntegerLabel> + <IntegerLabel>1</IntegerLabel> + <IntegerLabel>2</IntegerLabel> + <IntegerLabel>3</IntegerLabel> + <IntegerLabel>4</IntegerLabel> + </states> + <inputAlphabet> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </inputAlphabet> + <stackAlphabet> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </stackAlphabet> + <initialStates> + <IntegerLabel>0</IntegerLabel> + </initialStates> + <initialStackSymbols> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </initialStackSymbols> + <finalStates> + <IntegerLabel>4</IntegerLabel> + </finalStates> + <transitions> + <transition> + <from> + <IntegerLabel>0</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>0</IntegerLabel> + </to> + <push/> + </transition> + <transition> + <from> + <IntegerLabel>0</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>0</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>0</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>0</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>0</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>2</IntegerLabel> + </to> + <push/> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push/> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>1</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>1</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>2</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>4</IntegerLabel> + </to> + <push/> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a0</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push/> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a1</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>R</StringLabel> + </LabeledSymbol> + </push> + </transition> + <transition> + <from> + <IntegerLabel>3</IntegerLabel> + </from> + <input> + <LabeledSymbol> + <StringLabel>a2</StringLabel> + </LabeledSymbol> + </input> + <pop> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </pop> + <to> + <IntegerLabel>3</IntegerLabel> + </to> + <push> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + <LabeledSymbol> + <StringLabel>T</StringLabel> + </LabeledSymbol> + </push> + </transition> + </transitions> +</NPDA>