From bd19d4ae2166121290163b5b1d357c9ab06f5fcd Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Tue, 3 Nov 2015 15:14:06 +0100
Subject: [PATCH] patch up determinisation of RHDPDA

---
 .../determinize/DeterminizeRHDPDAPart.cxx     | 71 +++++++++++++------
 .../determinize/DeterminizeVPAPart.cxx        |  9 ++-
 .../determinize/common/RHDPDACommon.cpp       | 46 ++++++++----
 .../determinize/common/RHDPDACommon.h         |  8 +--
 4 files changed, 91 insertions(+), 43 deletions(-)

diff --git a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.cxx b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.cxx
index 1be3c7ed82..7415179a09 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.cxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.cxx
@@ -14,6 +14,7 @@
 #include "label/Label.h"
 #include "exception/AlibException.h"
 #include <set>
+#include <common/GlobalData.h>
 
 namespace automaton {
 
@@ -27,7 +28,7 @@ void addRetTransition(const automaton::State& from, const std::variant<string::E
 	deterministic.addReturnTransition(from, input, dvpdaSymbol, to);
 }
 
-void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
+void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic, std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& rubbishReturnTransitions) {
 	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
 
 	std::set<std::pair<label::Label, label::Label>> S1;
@@ -47,10 +48,16 @@ void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol
 		}
 	}
 
-	addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S1))), deterministic);
+	automaton::State to(packToStateLabel(std::move(S1)));
+	if(S1.empty()) {
+		std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol> key(state, input, pdaSymbol);
+		rubbishReturnTransitions.insert(std::make_pair(key, to));
+	} else {
+		addRetTransition(state, input, pdaSymbol, to, deterministic);
+	}
 }
 
-void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
+void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic, std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& rubbishReturnTransitions) {
 	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
 	std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>> pdaSymbolUnpack = unpackFromDRHDPDAStackSymbol(pdaSymbol);
 	const std::set<std::pair<label::Label, label::Label>>& S1 = pdaSymbolUnpack.first;
@@ -97,7 +104,13 @@ void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const
 		}
 	}
 
-	addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S2))), deterministic);
+	automaton::State to(packToStateLabel(std::move(S2)));
+	if(S2.empty()) {
+		std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol> key(state, input, pdaSymbol);
+		rubbishReturnTransitions.insert(std::make_pair(key, to));
+	} else {
+		addRetTransition(state, input, pdaSymbol, to, deterministic);
+	}
 }
 
 void addCallTransition(const automaton::State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::State& to, const alphabet::Symbol& dvpdaSymbol, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
@@ -108,7 +121,7 @@ void addCallTransition(const automaton::State& from, const std::variant<string::
 	deterministic.addCallTransition(from, input, to, dvpdaSymbol);
 }
 
-void call(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
+void call(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic, std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions) {
 	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
 
 	std::set<label::Label> R = retrieveDSubSet(S);
@@ -127,7 +140,13 @@ void call(const automaton::State& state, const std::variant<string::Epsilon, alp
 		}
 	}
 
-	addCallTransition(state, input, automaton::State(packToStateLabel(createIdentity(std::move(R1)))), alphabet::Symbol(alphabet::LabeledSymbol(packToStackSymbolLabel(std::make_pair(std::move(S), input)))), deterministic);
+	automaton::State to(packToStateLabel(createIdentity(std::move(R1))));
+	alphabet::Symbol push(alphabet::LabeledSymbol(packToStackSymbolLabel(std::make_pair(std::move(S), input))));
+	if(R1.empty()) {
+		rubbishCallTransitions.insert(std::make_pair(std::make_pair(state, input), std::make_pair(to, push)));
+	} else {
+		addCallTransition(state, input, to, push, deterministic);
+	}
 }
 
 void addLocalTransition(const automaton::State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::State& to, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
@@ -137,7 +156,7 @@ void addLocalTransition(const automaton::State& from, const std::variant<string:
 	deterministic.addLocalTransition(from, input, to);
 }
 
-void local(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic) {
+void local(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicDPDA& deterministic, std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& rubbishLocalTransitions ) {
 	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
 	std::set<std::pair<label::Label, label::Label>> S1;
 
@@ -156,7 +175,12 @@ void local(const automaton::State& state, const std::variant<string::Epsilon, al
 		}
 	}
 
-	addLocalTransition(state, input, automaton::State(packToStateLabel(std::move(S1))), deterministic);
+	automaton::State to(packToStateLabel(std::move(S1)));
+	if(S1.empty()) {
+		rubbishLocalTransitions.insert(std::make_pair(std::make_pair(state, input), to));
+	} else {
+		addLocalTransition(state, input, to, deterministic);
+	}
 }
 
 std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> getLocalCallRetPartitioning(const automaton::RealTimeHeightDeterministicNPDA& n, const automaton::State& state) {
@@ -181,15 +205,6 @@ std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<s
 			ret.insert(std::get<1>(transition.first));
 	}
 
-	if(!std::empty_intersection(local, call))
-		throw exception::AlibException("Automaton is not real time height deterministic pushdown");
-
-	if(!std::empty_intersection(local, ret))
-		throw exception::AlibException("Automaton is not real time height deterministic pushdown");
-
-	if(!std::empty_intersection(call, ret))
-		throw exception::AlibException("Automaton is not real time height deterministic pushdown");
-
 	return std::make_tuple(local, call, ret);
 }
 
@@ -199,37 +214,47 @@ automaton::RealTimeHeightDeterministicDPDA Determinize::determinize(const automa
 	automaton::RealTimeHeightDeterministicDPDA d(automaton::State(initialLabel), n.getBottomOfTheStackSymbol());
 	d.setInputAlphabet(n.getInputAlphabet());
 
+	std::set<automaton::State> rubbishStates = {automaton::State(packToStateLabel({}))};
+	std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State> rubbishReturnTransitions;
+	std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> > rubbishCallTransitions;
+	std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State> rubbishLocalTransitions;
+
 	for(;;) {
-		std::set<std::pair<automaton::State, alphabet::Symbol>> stateSymbols = existsDirtyStateSymbol(d, n);
-		std::set<automaton::State> states = existsDirtyState(d, n);
+		std::set<std::pair<automaton::State, alphabet::Symbol>> stateSymbols = existsDirtyStateSymbol(d, rubbishStates, rubbishCallTransitions, rubbishReturnTransitions, n);
+		std::set<automaton::State> states = existsDirtyState(d, rubbishStates, rubbishCallTransitions, rubbishLocalTransitions, n);
 
 		if(stateSymbols.empty() && states.empty()) break;
 
 		for(const auto& stateSymbol : stateSymbols) {
+			if ( common::GlobalData::verbose )
+				std::clog << "Dirty state symbol: " << stateSymbol << std::endl;
+
 			std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> partitioning = getLocalCallRetPartitioning(n, stateSymbol.first);
 
 			std::set<std::variant<string::Epsilon, alphabet::Symbol>>& retPart = std::get<2>(partitioning);
 
 			for(const auto& symbol : retPart) {
 				if(stateSymbol.second == d.getBottomOfTheStackSymbol()) {
-					retInitial(stateSymbol.first, stateSymbol.second, symbol, n, d);
+					retInitial(stateSymbol.first, stateSymbol.second, symbol, n, d, rubbishReturnTransitions);
 				} else {
-					ret(stateSymbol.first, stateSymbol.second, symbol, n, d);
+					ret(stateSymbol.first, stateSymbol.second, symbol, n, d, rubbishReturnTransitions);
 				}
 			}
 		}
 
 		for(const auto& state : states) {
+			if ( common::GlobalData::verbose )
+				std::clog << "Dirty state: " << state << std::endl;
 			std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> partitioning = getLocalCallRetPartitioning(n, state);
 
 			std::set<std::variant<string::Epsilon, alphabet::Symbol>>& localPart = std::get<0>(partitioning);
 			std::set<std::variant<string::Epsilon, alphabet::Symbol>>& callPart = std::get<1>(partitioning);
 
 			for(const auto& symbol : localPart) {
-				local(state, symbol, n, d);
+				local(state, symbol, n, d, rubbishLocalTransitions);
 			}
 			for(const auto& symbol : callPart) {
-				call(state, symbol, n, d);
+				call(state, symbol, n, d, rubbishCallTransitions);
 			}
 		}
 	}
diff --git a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.cxx b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.cxx
index dc904a1359..2be0234c93 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.cxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.cxx
@@ -166,9 +166,14 @@ automaton::VisiblyPushdownDPDA Determinize::determinize(const automaton::Visibly
 	d.setLocalInputAlphabet(n.getLocalInputAlphabet());
 	d.setReturnInputAlphabet(n.getReturnInputAlphabet());
 
+	std::set<automaton::State> rubbishStates = {automaton::State(packToStateLabel({}))};
+	std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State> rubbishReturnTransitions;
+	std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> > rubbishCallTransitions;
+	std::map<std::pair<State, alphabet::Symbol>, State> rubbishLocalTransitions;
+
 	for(;;) {
-		std::set<std::pair<automaton::State, alphabet::Symbol>> stateSymbols = existsDirtyStateSymbol(d, n);
-		std::set<automaton::State> states = existsDirtyState(d, n);
+		std::set<std::pair<automaton::State, alphabet::Symbol>> stateSymbols = existsDirtyStateSymbol(d, rubbishStates, rubbishCallTransitions, rubbishReturnTransitions, n);
+		std::set<automaton::State> states = existsDirtyState(d, rubbishStates, rubbishCallTransitions, rubbishLocalTransitions, n);
 
 		if(stateSymbols.empty() && states.empty()) break;
 
diff --git a/alib2algo/src/automaton/determinize/common/RHDPDACommon.cpp b/alib2algo/src/automaton/determinize/common/RHDPDACommon.cpp
index 3a92fcdab7..dffadfeddc 100644
--- a/alib2algo/src/automaton/determinize/common/RHDPDACommon.cpp
+++ b/alib2algo/src/automaton/determinize/common/RHDPDACommon.cpp
@@ -89,11 +89,20 @@ std::set<std::pair<label::Label, label::Label>> createIdentity(std::set<label::L
 	return id;
 }
 
-template<class T, class R>
-std::set<automaton::State> existsDirtyState(const T& d, const R& n) {
+template<class T, class S, class R>
+std::set<automaton::State> existsDirtyState(const T& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, S>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::pair<State, S>, State>& rubbishLocalTransitions, const R& n) {
 	std::set<automaton::State> dirtyStates;
 
-	for(const automaton::State& state : d.getStates()) {
+	std::set<automaton::State> states = d.getStates();
+	states.insert(rubbishStates.begin(), rubbishStates.end());
+
+	auto callTransitions = d.getCallTransitions();
+	callTransitions.insert(rubbishCallTransitions.begin(), rubbishCallTransitions.end());
+
+	auto localTransitions = d.getLocalTransitions();
+	localTransitions.insert(rubbishLocalTransitions.begin(), rubbishLocalTransitions.end());
+
+	for(const automaton::State& state : states) {
 		const label::Label& stateLabel = state.getName();
 		const std::set<label::Label> dSubSet = retrieveDSubSet(unpackFromStateLabel(stateLabel));
 
@@ -114,13 +123,13 @@ std::set<automaton::State> existsDirtyState(const T& d, const R& n) {
 		if(!originalCallsLocals) continue;
 		bool deterministicCallLocals = false;
 
-		for(const auto& transition : d.getCallTransitions()) {
+		for(const auto& transition : callTransitions) {
 			if(stateLabel == transition.first.first.getName()) {
 				deterministicCallLocals = true;
 				break;
 			}
 		}
-		if(deterministicCallLocals) for(const auto& transition : d.getLocalTransitions()) {
+		if(deterministicCallLocals) for(const auto& transition : localTransitions) {
 			if(stateLabel == transition.first.first.getName()) {
 				deterministicCallLocals = true;
 				break;
@@ -133,8 +142,8 @@ std::set<automaton::State> existsDirtyState(const T& d, const R& n) {
 	return dirtyStates;
 }
 
-template std::set<automaton::State> existsDirtyState(const automaton::VisiblyPushdownDPDA& d, const automaton::VisiblyPushdownNPDA& n);
-template std::set<automaton::State> existsDirtyState(const automaton::RealTimeHeightDeterministicDPDA& d, const automaton::RealTimeHeightDeterministicNPDA& n);
+template std::set<automaton::State> existsDirtyState(const automaton::VisiblyPushdownDPDA& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::pair<State, alphabet::Symbol>, State>& rubbishLocalTransitions, const automaton::VisiblyPushdownNPDA& n);
+template std::set<automaton::State> existsDirtyState(const automaton::RealTimeHeightDeterministicDPDA& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& rubbishLocalTransitions, const automaton::RealTimeHeightDeterministicNPDA& n);
 
 template<class T>
 void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const T& d) {
@@ -172,11 +181,20 @@ void localClosure(std::set<label::Label>& states, const std::set<label::Label>&
 template void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const automaton::VisiblyPushdownDPDA& d);
 template void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const automaton::RealTimeHeightDeterministicDPDA& d);
 
-template<class T, class R>
-std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const T& d, const R& n) {
+template<class T, class S, class R>
+std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const T& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, S>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::tuple<State, S, alphabet::Symbol>, State>& rubbishReturnTransitions,  const R& n) {
 	std::set<std::pair<automaton::State, alphabet::Symbol>> dirtyStateSymbols;
 
-	for(const automaton::State& state : d.getStates()) {
+	std::set<automaton::State> states = d.getStates();
+	states.insert(rubbishStates.begin(), rubbishStates.end());
+
+	auto callTransitions = d.getCallTransitions();
+	callTransitions.insert(rubbishCallTransitions.begin(), rubbishCallTransitions.end());
+
+	auto returnTransitions = d.getReturnTransitions();
+	returnTransitions.insert(rubbishReturnTransitions.begin(), rubbishReturnTransitions.end());
+
+	for(const automaton::State& state : states) {
 		const label::Label& stateLabel = state.getName();
 
 		std::set<label::Label> lc { stateLabel };
@@ -197,7 +215,7 @@ break2:		if(!originalPops) continue;
 
 		std::set<alphabet::Symbol> topSymbols;
 		for(const label::Label& localState : lc) {
-			for(const auto& transition : d.getCallTransitions()) {
+			for(const auto& transition : callTransitions) {
 				const auto& to = transition.second;
 				if(localState != to.first.getName()) continue;
 
@@ -209,7 +227,7 @@ break2:		if(!originalPops) continue;
 			}
 		}
 
-		for(const auto& transition : d.getReturnTransitions()) {
+		for(const auto& transition : returnTransitions) {
 			if(stateLabel != std::get<0>(transition.first).getName()) continue;
 
 			topSymbols.erase(std::get<2>(transition.first));
@@ -221,8 +239,8 @@ break2:		if(!originalPops) continue;
 	return dirtyStateSymbols;
 }
 
-template std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const automaton::VisiblyPushdownDPDA& d, const automaton::VisiblyPushdownNPDA& n);
-template std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const automaton::RealTimeHeightDeterministicDPDA& d, const automaton::RealTimeHeightDeterministicNPDA& n);
+template std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const automaton::VisiblyPushdownDPDA& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& rubbishReturnTransitions, const automaton::VisiblyPushdownNPDA& n);
+template std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const automaton::RealTimeHeightDeterministicDPDA& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& rubbishReturnTransitions, const automaton::RealTimeHeightDeterministicNPDA& n);
 
 std::set<label::Label> retrieveLabels(const std::set<automaton::State>& states) {
 	std::set<label::Label> labels;
diff --git a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
index cfeb72c6ba..5e93f6775a 100644
--- a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
+++ b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
@@ -29,14 +29,14 @@ std::set<label::Label> retrieveDSubSet(const std::set<std::pair<label::Label, la
 
 std::set<std::pair<label::Label, label::Label>> createIdentity(std::set<label::Label>&& states);
 
-template<class T, class R>
-std::set<automaton::State> existsDirtyState(const T& d, const R& n);
+template<class T, class S, class R>
+std::set<automaton::State> existsDirtyState(const T& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, S>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::pair<State, S>, State>& rubbishLocalTransitions, const R& n);
 
 template<class T>
 void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const T& d);
 
-template<class T, class R>
-std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const T& d, const R& n);
+template<class T, class S, class R>
+std::set<std::pair<automaton::State, alphabet::Symbol>> existsDirtyStateSymbol(const T& d, const std::set<automaton::State>& rubbishStates, const std::map<std::pair<State, S>, std::pair<State, alphabet::Symbol> >& rubbishCallTransitions, const std::map<std::tuple<State, S, alphabet::Symbol>, State>& rubbishReturnTransitions,  const R& n);
 
 std::set<label::Label> retrieveLabels(const std::set<automaton::State>& states);
 
-- 
GitLab