diff --git a/alib2algo/src/automaton/simplify/Minimize.cpp b/alib2algo/src/automaton/simplify/Minimize.cpp
index 8b51f0729dfc291fc0e0f88f2dafa35349e460dc..7cd64184fe8b4d8ec780443c4f0f0226a7c1a378 100644
--- a/alib2algo/src/automaton/simplify/Minimize.cpp
+++ b/alib2algo/src/automaton/simplify/Minimize.cpp
@@ -7,15 +7,6 @@
#include "Minimize.h"
-#include <map>
-#include <set>
-#include <iomanip>
-#include <sstream>
-
-#include <alphabet/Symbol.h>
-
-#include <global/GlobalData.h>
-
namespace automaton {
namespace simplify {
@@ -24,201 +15,6 @@ automaton::Automaton Minimize::minimize(const automaton::Automaton& automaton) {
return dispatch(automaton.getData());
}
-automaton::DFA<> Minimize::minimize(const automaton::DFA<>& dfa) {
- if(dfa.getFinalStates().size() == 0) {
- automaton::DFA < > result(dfa.getInitialState());
- result.setInputAlphabet(dfa.getInputAlphabet());
- return result;
- }
-
- std::map<label::Label, std::map<alphabet::Symbol, label::Label > > refactor;
-
- for(const label::Label& state : dfa.getStates()) {
- refactor.insert(std::make_pair(state, std::map<alphabet::Symbol, label::Label>()));
- }
-
- for(const std::pair<const std::pair<label::Label, alphabet::Symbol>, label::Label>& transition : dfa.getTransitions()) {
- refactor[transition.first.first].insert(std::make_pair(transition.first.second, transition.second));
- }
-
- std::map<label::Label, label::Label> toEquvivalentStates1; //original state to equivalent state
- std::map<std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> > minimizedTransitionFunction1; //mapped to the original state
-
- std::map<label::Label, label::Label> toEquvivalentStates2;
- std::map<std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> > minimizedTransitionFunction2;
-
- const label::Label *firstFinal = NULL, *firstNonfinal = NULL;
- for(const label::Label& state : dfa.getStates()) {
- if(dfa.getFinalStates().count(state) == 0) { // not a final state
- if(!firstNonfinal) firstNonfinal = &state;
- toEquvivalentStates2.insert(std::pair<label::Label, label::Label>(state, *firstNonfinal));
- } else {
- if(!firstFinal) firstFinal = &state;
- toEquvivalentStates2.insert(std::pair<label::Label, label::Label>(state, *firstFinal));
- }
- }
-
- for(const std::pair<const label::Label, std::map<alphabet::Symbol, label::Label> >& transition : refactor) {
- const label::Label& from = toEquvivalentStates2.find(transition.first)->second;
- std::set<std::pair<alphabet::Symbol, label::Label> > transitionFunction;
-
- for(const std::pair<const alphabet::Symbol, label::Label> & transitionFromState : transition.second) {
- transitionFunction.insert(std::make_pair(transitionFromState.first, toEquvivalentStates2.find(transitionFromState.second)->second));
- }
-
- minimizedTransitionFunction2[std::make_pair(from, transitionFunction)].insert(transition.first);
- }
-
- size_t delta_iter = 0;
- if(common::GlobalData::verbose) {
- print_progress(dfa, minimizedTransitionFunction2, delta_iter++);
- }
-
- do {
- toEquvivalentStates1 = toEquvivalentStates2;
- minimizedTransitionFunction1 = minimizedTransitionFunction2;
-
- toEquvivalentStates2.clear();
- minimizedTransitionFunction2.clear();
-
- for(const std::pair<const std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& transition : minimizedTransitionFunction1) {
- for(const label::Label& target : transition.second) {
- toEquvivalentStates2.insert(std::make_pair(target, *(transition.second.begin())));
- }
- }
-
- for(const std::pair<const label::Label, std::map<alphabet::Symbol, label::Label> >& transition : refactor) {
- const label::Label& from = toEquvivalentStates2.find(transition.first)->second;
- std::set<std::pair<alphabet::Symbol, label::Label> > transitionFunction;
-
- for(const std::pair<const alphabet::Symbol, label::Label> & transitionFromState : transition.second) {
- transitionFunction.insert(std::make_pair(transitionFromState.first, toEquvivalentStates2.find(transitionFromState.second)->second));
- }
-
- minimizedTransitionFunction2[std::make_pair(from, transitionFunction)].insert(transition.first);
- }
-
- if(common::GlobalData::verbose) {
- print_progress(dfa, minimizedTransitionFunction2, delta_iter++);
- }
-
- } while(minimizedTransitionFunction1.size() != minimizedTransitionFunction2.size());
-
- const label::Label* initialState = NULL;
- for(const std::pair<const std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& transition : minimizedTransitionFunction2) {
- if(transition.second.count(dfa.getInitialState())) {
- initialState = &(transition.first.first);
- break;
- }
- }
-
- automaton::DFA<> result(*initialState);
-
- result.setInputAlphabet(dfa.getInputAlphabet());
-
- for(const std::pair<const std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& transition : minimizedTransitionFunction2) {
- result.addState(transition.first.first);
- if(dfa.getFinalStates().count(*(transition.second.begin()))) {
- result.addFinalState(transition.first.first);
- }
- }
-
- for(const std::pair<const std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& transition : minimizedTransitionFunction2) {
- for(const std::pair<alphabet::Symbol, label::Label>& transitionFromState : transition.first.second) {
- result.addTransition(transition.first.first, transitionFromState.first, transitionFromState.second);
- }
- }
-
- return result;
-}
-
-#define RESETSS(x) {(x).clear(); (x).str("");}
-
-void Minimize::print_progress(const automaton::DFA<>& dfa, const std::map<std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& minimizedTransitionFunction, size_t iter) {
- std::clog << "delta " << iter << std::endl;
-
- //std::map<std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> > minimizedTransitionFunction1; //mapped to the original state
-
- /* need to restruct this first so we have table like: orig state | new state | trans_symb_1 | trans_symb_2 | ... | trans_symb_n */
- // we surely have DFA here (transition map hence)
- std::map<std::pair<label::Label, label::Label>, std::map<alphabet::Symbol, label::Label>> printMap;
- for(const auto& kv: minimizedTransitionFunction) {
- for(const auto& state : kv.second) {
- std::map<alphabet::Symbol, label::Label> stateTransMap;
- for(const auto& transition : kv.first.second) {
- stateTransMap.insert(std::make_pair(transition.first, transition.second));
- }
- printMap.insert(std::make_pair(std::make_pair(state, kv.first.first), stateTransMap));
- }
- }
-
- size_t stateWidth = 1, stateMapWidth = 1;
- std::map<alphabet::Symbol, size_t> colWidths;
- std::ostringstream ss;
-
- for(const alphabet::Symbol& symbol : dfa.getInputAlphabet()) {
- ss << symbol;
- colWidths[symbol] = ss.str().size();
- RESETSS(ss);
- }
- for(const auto& kv : printMap) {
- ss << kv.first.first;
- stateWidth = std::max(stateWidth, ss.str().size());
- RESETSS(ss);
-
- ss << kv.first.second;
- stateMapWidth = std::max(stateMapWidth, ss.str().size());
- RESETSS(ss);
-
- for(const alphabet::Symbol& symbol : dfa.getInputAlphabet()) {
- auto it = kv.second.find(symbol);
- if(it != kv.second.end())
- {
- ss << it -> second;
- colWidths[symbol] = std::max(colWidths[symbol], ss.str().size());
- RESETSS(ss);
- }
- }
- }
-
- std::clog << std::setw(stateWidth) << "";
- std::clog << " | ";
- std::clog << std::setw(stateMapWidth) << "";
- std::clog << " | ";
- for(const alphabet::Symbol& symbol : dfa.getInputAlphabet()) {
- ss << symbol;
- std::clog << std::setw(colWidths[symbol]) << ss.str() << " | ";
- RESETSS(ss);
- }
- std::clog << std::endl;
- for(const auto& kv : printMap) {
- ss << kv.first.first;
- std::clog << std::setw(stateWidth) << ss.str() << " | ";
- RESETSS(ss);
-
- ss << kv.first.second;
- std::clog << std::setw(stateMapWidth) << ss.str() << " | ";
- RESETSS(ss);
-
- for(const auto& symbol : dfa.getInputAlphabet()) {
- auto it = kv.second.find(symbol);
- if(it != kv.second.end())
- {
- ss << it -> second;
- std::clog << std::setw(colWidths[symbol]) << ss.str();
- RESETSS(ss);
- }
- else
- {
- std::clog << std::setw(colWidths[symbol]) << "";
- }
- std::clog << " | ";
- }
- std::clog << std::endl;
- }
- std::clog << std::endl;
-}
-
auto MinimizeNFA = Minimize::RegistratorWrapper<automaton::DFA<>, automaton::DFA<>>( Minimize::minimize );
} /* namespace simplify */
diff --git a/alib2algo/src/automaton/simplify/Minimize.h b/alib2algo/src/automaton/simplify/Minimize.h
index 11e0d876cb8861507264f39887e54214c6448309..41dde5759a5faf1cf4e6218f39a9b218dc1484ff 100644
--- a/alib2algo/src/automaton/simplify/Minimize.h
+++ b/alib2algo/src/automaton/simplify/Minimize.h
@@ -12,6 +12,13 @@
#include <automaton/Automaton.h>
#include <automaton/FSM/DFA.h>
+#include <map>
+#include <set>
+#include <iomanip>
+#include <sstream>
+
+#include <global/GlobalData.h>
+
namespace automaton {
namespace simplify {
@@ -23,12 +30,208 @@ public:
*/
static automaton::Automaton minimize(const automaton::Automaton& dfa);
- static automaton::DFA<> minimize(const automaton::DFA<>& dfa);
+ template < class SymbolType, class StateType >
+ static automaton::DFA < SymbolType, StateType > minimize(const automaton::DFA < SymbolType, StateType >& dfa);
private:
- static void print_progress(const automaton::DFA<>& dfa, const std::map<std::pair<label::Label, std::set<std::pair<alphabet::Symbol, label::Label> > >, std::set<label::Label> >& minimizedTransitionFunction, size_t iter);
+ template < class SymbolType, class StateType >
+ static void print_progress(const automaton::DFA < SymbolType, StateType >& dfa, const std::map<std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& minimizedTransitionFunction, size_t iter);
};
+template < class SymbolType, class StateType >
+automaton::DFA < SymbolType, StateType > Minimize::minimize(const automaton::DFA < SymbolType, StateType >& dfa) {
+ if(dfa.getFinalStates().size() == 0) {
+ automaton::DFA < SymbolType, StateType > result(dfa.getInitialState());
+ result.setInputAlphabet(dfa.getInputAlphabet());
+ return result;
+ }
+
+ std::map<StateType, std::map<SymbolType, StateType > > refactor;
+
+ for(const StateType& state : dfa.getStates()) {
+ refactor.insert(std::make_pair(state, std::map<SymbolType, StateType>()));
+ }
+
+ for(const std::pair<const std::pair<StateType, SymbolType>, StateType>& transition : dfa.getTransitions()) {
+ refactor[transition.first.first].insert(std::make_pair(transition.first.second, transition.second));
+ }
+
+ std::map<StateType, StateType> toEquvivalentStates1; //original state to equivalent state
+ std::map<std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> > minimizedTransitionFunction1; //mapped to the original state
+
+ std::map<StateType, StateType> toEquvivalentStates2;
+ std::map<std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> > minimizedTransitionFunction2;
+
+ const StateType *firstFinal = NULL, *firstNonfinal = NULL;
+ for(const StateType& state : dfa.getStates()) {
+ if(dfa.getFinalStates().count(state) == 0) { // not a final state
+ if(!firstNonfinal) firstNonfinal = &state;
+ toEquvivalentStates2.insert(std::pair<StateType, StateType>(state, *firstNonfinal));
+ } else {
+ if(!firstFinal) firstFinal = &state;
+ toEquvivalentStates2.insert(std::pair<StateType, StateType>(state, *firstFinal));
+ }
+ }
+
+ for(const std::pair<const StateType, std::map<SymbolType, StateType> >& transition : refactor) {
+ const StateType& from = toEquvivalentStates2.find(transition.first)->second;
+ std::set<std::pair<SymbolType, StateType> > transitionFunction;
+
+ for(const std::pair<const SymbolType, StateType> & transitionFromState : transition.second) {
+ transitionFunction.insert(std::make_pair(transitionFromState.first, toEquvivalentStates2.find(transitionFromState.second)->second));
+ }
+
+ minimizedTransitionFunction2[std::make_pair(from, transitionFunction)].insert(transition.first);
+ }
+
+ size_t delta_iter = 0;
+ if(common::GlobalData::verbose) {
+ print_progress(dfa, minimizedTransitionFunction2, delta_iter++);
+ }
+
+ do {
+ toEquvivalentStates1 = toEquvivalentStates2;
+ minimizedTransitionFunction1 = minimizedTransitionFunction2;
+
+ toEquvivalentStates2.clear();
+ minimizedTransitionFunction2.clear();
+
+ for(const std::pair<const std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& transition : minimizedTransitionFunction1) {
+ for(const StateType& target : transition.second) {
+ toEquvivalentStates2.insert(std::make_pair(target, *(transition.second.begin())));
+ }
+ }
+
+ for(const std::pair<const StateType, std::map<SymbolType, StateType> >& transition : refactor) {
+ const StateType& from = toEquvivalentStates2.find(transition.first)->second;
+ std::set<std::pair<SymbolType, StateType> > transitionFunction;
+
+ for(const std::pair<const SymbolType, StateType> & transitionFromState : transition.second) {
+ transitionFunction.insert(std::make_pair(transitionFromState.first, toEquvivalentStates2.find(transitionFromState.second)->second));
+ }
+
+ minimizedTransitionFunction2[std::make_pair(from, transitionFunction)].insert(transition.first);
+ }
+
+ if(common::GlobalData::verbose) {
+ print_progress(dfa, minimizedTransitionFunction2, delta_iter++);
+ }
+
+ } while(minimizedTransitionFunction1.size() != minimizedTransitionFunction2.size());
+
+ const StateType* initialState = NULL;
+ for(const std::pair<const std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& transition : minimizedTransitionFunction2) {
+ if(transition.second.count(dfa.getInitialState())) {
+ initialState = &(transition.first.first);
+ break;
+ }
+ }
+
+ automaton::DFA < SymbolType, StateType > result(*initialState);
+
+ result.setInputAlphabet(dfa.getInputAlphabet());
+
+ for(const std::pair<const std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& transition : minimizedTransitionFunction2) {
+ result.addState(transition.first.first);
+ if(dfa.getFinalStates().count(*(transition.second.begin()))) {
+ result.addFinalState(transition.first.first);
+ }
+ }
+
+ for(const std::pair<const std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& transition : minimizedTransitionFunction2) {
+ for(const std::pair<SymbolType, StateType>& transitionFromState : transition.first.second) {
+ result.addTransition(transition.first.first, transitionFromState.first, transitionFromState.second);
+ }
+ }
+
+ return result;
+}
+
+#define RESETSS(x) {(x).clear(); (x).str("");}
+
+template < class SymbolType, class StateType >
+void Minimize::print_progress(const automaton::DFA < SymbolType, StateType >& dfa, const std::map<std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> >& minimizedTransitionFunction, size_t iter) {
+ std::clog << "delta " << iter << std::endl;
+
+ //std::map<std::pair<StateType, std::set<std::pair<SymbolType, StateType> > >, std::set<StateType> > minimizedTransitionFunction1; //mapped to the original state
+
+ /* need to restruct this first so we have table like: orig state | new state | trans_symb_1 | trans_symb_2 | ... | trans_symb_n */
+ // we surely have DFA here (transition map hence)
+ std::map<std::pair<StateType, StateType>, std::map<SymbolType, StateType>> printMap;
+ for(const auto& kv: minimizedTransitionFunction) {
+ for(const auto& state : kv.second) {
+ std::map<SymbolType, StateType> stateTransMap;
+ for(const auto& transition : kv.first.second) {
+ stateTransMap.insert(std::make_pair(transition.first, transition.second));
+ }
+ printMap.insert(std::make_pair(std::make_pair(state, kv.first.first), stateTransMap));
+ }
+ }
+
+ size_t stateWidth = 1, stateMapWidth = 1;
+ std::map<SymbolType, size_t> colWidths;
+ std::ostringstream ss;
+
+ for(const SymbolType& symbol : dfa.getInputAlphabet()) {
+ ss << symbol;
+ colWidths[symbol] = ss.str().size();
+ RESETSS(ss);
+ }
+ for(const auto& kv : printMap) {
+ ss << kv.first.first;
+ stateWidth = std::max(stateWidth, ss.str().size());
+ RESETSS(ss);
+
+ ss << kv.first.second;
+ stateMapWidth = std::max(stateMapWidth, ss.str().size());
+ RESETSS(ss);
+
+ for(const SymbolType& symbol : dfa.getInputAlphabet()) {
+ auto it = kv.second.find(symbol);
+ if(it != kv.second.end()) {
+ ss << it -> second;
+ colWidths[symbol] = std::max(colWidths[symbol], ss.str().size());
+ RESETSS(ss);
+ }
+ }
+ }
+
+ std::clog << std::setw(stateWidth) << "";
+ std::clog << " | ";
+ std::clog << std::setw(stateMapWidth) << "";
+ std::clog << " | ";
+ for(const SymbolType& symbol : dfa.getInputAlphabet()) {
+ ss << symbol;
+ std::clog << std::setw(colWidths[symbol]) << ss.str() << " | ";
+ RESETSS(ss);
+ }
+ std::clog << std::endl;
+ for(const auto& kv : printMap) {
+ ss << kv.first.first;
+ std::clog << std::setw(stateWidth) << ss.str() << " | ";
+ RESETSS(ss);
+
+ ss << kv.first.second;
+ std::clog << std::setw(stateMapWidth) << ss.str() << " | ";
+ RESETSS(ss);
+
+ for(const auto& symbol : dfa.getInputAlphabet()) {
+ auto it = kv.second.find(symbol);
+ if(it != kv.second.end()) {
+ ss << it -> second;
+ std::clog << std::setw(colWidths[symbol]) << ss.str();
+ RESETSS(ss);
+ }
+ else {
+ std::clog << std::setw(colWidths[symbol]) << "";
+ }
+ std::clog << " | ";
+ }
+ std::clog << std::endl;
+ }
+ std::clog << std::endl;
+}
+
} /* namespace simplify */
} /* namespace automaton */