30 StateSet::Iterator lit;
41 FD_DF(
"UniqueInit: introducing new initial state: " << inituni);
43 FD_DF(
"UniqueInit: introduce outgoing transitions: ");
47 FD_DF(
"UniqueInit: " << inituni <<
"-" << tit->Ev <<
"-" << tit->X2);
53 FD_DF(
"UniqueInit: set marked state: " << inituni);
70 std::vector<StateSet> power_states;
71 std::vector<Idx> det_states;
81 pResGen= rResGen.
New();
88 if(pResGen != &rResGen) {
89 pResGen->
Move(rResGen);
99 rEntryStatesMap.clear();
101 std::vector<StateSet> power_states;
102 std::vector<Idx> det_states;
106 std::vector<StateSet>::size_type i;
107 for (i = 0; i < power_states.size(); ++i) {
108 rEntryStatesMap.insert(std::pair<Idx,StateSet>(det_states[i], power_states[i]));
114 std::vector<Idx>& rDetStates,
Generator& rResGen) {
119 FD_DF(
"Deterministic(): core function #" << rGen.
Size());
123 if(&rResGen== &rGen) {
124 pResGen= rResGen.
New();
129 rPowerStates.clear();
136 FD_DF(
"Deterministic B");
140 if(pResGen != &rResGen) {
141 pResGen->
Move(rResGen);
144 FD_DF(
"Deterministic(): done (empty)");
149 typedef std::multimap< Idx,std::vector<StateSet>::size_type > T_HASHMAP;
151 std::vector<StateSet>::size_type current_vecindex;
152 std::pair< std::map<StateSet,Idx>::iterator,
bool > result;
155 StateSet::Iterator lit;
156 const Idx max_idx = std::numeric_limits<Idx>::max();
169 FD_DF(
"Deterministic: setting as mstate: " << rGen.
SStr(newstate));
172 FD_DF(
"Deterministic: created subset of initial states {"
173 << newset.
ToString() <<
"} with deterministic state index "
174 << rGen.
SStr(newstate));
176 rPowerStates.push_back(newset);
177 rDetStates.push_back(newstate);
178 hashmap.insert(std::make_pair(newset.
Signature(), (
Idx)rPowerStates.size() - 1));
181 for (current_vecindex = 0; current_vecindex < rPowerStates.size();
182 ++current_vecindex) {
183 FD_WPC(current_vecindex,rPowerStates.size(),
"Deterministic(): current/size: "<< current_vecindex <<
" / " << rPowerStates.size());
184 FD_DF(
"Deterministic: current power set: {"
185 << rPowerStates[current_vecindex].ToString() <<
"} -> "
186 << rDetStates[current_vecindex]);
188 std::vector<StateSet> newset_vec;
189 std::vector<Idx> event_vec;
192 FD_DF(
"Deterministic: starting multiway merge...");
193 std::list<TransSet::Iterator> merge_iterators;
194 std::vector<Transition> trans_vec;
198 for (lit = rPowerStates[current_vecindex].Begin();
199 lit != rPowerStates[current_vecindex].End(); ++lit) {
202 merge_iterators.push_back(tit);
203 FD_DF(
"Deterministic: added merge iterator: " << rGen.
SStr(tit->X1)
204 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
209 while (! merge_iterators.empty()) {
210 Idx currentevent = max_idx;
211 std::list<TransSet::Iterator>::iterator i;
212 std::list<TransSet::Iterator>::iterator currentit = merge_iterators.end();
213 for (i = merge_iterators.begin(); i != merge_iterators.end(); ++i) {
214 if ((*i)->Ev < currentevent) {
215 currentevent = (*i)->Ev;
229 while (currentit != merge_iterators.end()) {
230 currentstate = (*currentit)->X1;
234 if (j == transrel_end) {
235 merge_iterators.erase(currentit++);
239 else if (j->X1 == currentstate) {
241 if (j->Ev == currentevent) {
242 trans_vec.push_back(*j);
243 FD_DF(
"Deterine: adding transition to list: "
244 << rGen.
SStr(j->X1) <<
"-" << rGen.
EStr(j->Ev) <<
"-"
245 << rGen.
SStr(j->X2));
255 merge_iterators.erase(currentit++);
264 FD_DF(
"Deterministic: partitioning the transition vector...");
265 std::vector<Transition>::iterator tv_it;
268 for (tv_it = trans_vec.begin(); tv_it != trans_vec.end(); ++tv_it) {
269 if ((tv_it->Ev == lastevent) || (lastevent == 0)) {
271 lastevent = tv_it->Ev;
275 <<
"} with event " << rGen.
EStr(lastevent));
276 newset_vec.push_back(newset);
277 event_vec.push_back(lastevent);
280 lastevent = tv_it->Ev;
283 if (! newset.
Empty()) {
285 <<
"} with event " << rGen.
EStr(lastevent));
286 newset_vec.push_back(newset);
287 event_vec.push_back(lastevent);
289 FD_DF(
"Deterministic: partitioning the transition vector finished");
290 FD_DF(
"Deterministic: multiway merge finished");
294 std::vector<StateSet>::size_type nsv_index;
295 for (nsv_index = 0; nsv_index < newset_vec.size(); ++nsv_index) {
296 StateSet& currentset = newset_vec[nsv_index];
297 Idx currentevent = event_vec[nsv_index];
301 std::pair<T_HASHMAP::iterator,T_HASHMAP::iterator> phit
302 = hashmap.equal_range(sig);
303 T_HASHMAP::iterator hit = phit.first;
304 for (hit = phit.first; hit != phit.second; ++hit) {
306 if (currentset == rPowerStates[hit->second]) {
307 tmp_x2 = rDetStates[hit->second];
317 rPowerStates.push_back(currentset);
318 rDetStates.push_back(tmp_x2);
319 hashmap.insert(std::make_pair(sig, (
Idx)rPowerStates.size() - 1));
320 FD_DF(
"Deterministic: added new state "
322 <<
" for new subset {" << currentset.
ToString() <<
"}");
324 for (lit = currentset.
Begin(); lit != currentset.
End(); ++lit) {
332 pResGen->
SetTransition(rDetStates[current_vecindex], currentevent, tmp_x2);
339 FD_DF(
"Deterministic: fixing names...");
341 std::vector<StateSet>::size_type i;
343 std::vector<Idx>::const_iterator dit;
344 for (i = 0; i < rPowerStates.size(); ++i) {
346 std::string name =
"{";
347 for (lit = rPowerStates[i].Begin(); lit != rPowerStates[i].End(); ++lit) {
351 name.erase(name.length() - 1);
353 FD_DF(
"Deterministic: setting state name \"" << name <<
"\" for index "
360 if(pResGen != &rResGen) {
361 pResGen->
Move(rResGen);
365 FD_DF(
"Deterministic(): core function: done");
#define FD_WPC(cntnow, contdone, message)
Idx Signature(void) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
StateSet::Iterator InitStatesBegin(void) const
const TransSet & TransRel(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const StateSet & MarkedStates(void) const
void ClearInitStates(void)
const EventSet & Alphabet(void) const
virtual void Move(vGenerator &rGen)
virtual vGenerator & Assign(const Type &rSrc)
bool InitStatesEmpty(void) const
const StateSet & InitStates(void) const
TransSet::Iterator TransRelBegin(void) const
Idx InitStatesSize(void) const
virtual vGenerator * New(void) const
void SetInitState(Idx index)
std::string StateName(Idx index) const
void Name(const std::string &rName)
TransSet::Iterator TransRelEnd(void) const
std::string EStr(Idx index) const
void SetMarkedState(Idx index)
virtual void EventAttributes(const EventSet &rEventSet)
bool StateNamesEnabled(void) const
StateSet::Iterator InitStatesEnd(void) const
std::string SStr(Idx index) const
bool ExistsMarkedState(Idx index) const
std::string UniqueStateName(const std::string &rName) const
void InjectAlphabet(const EventSet &rNewalphabet)
Iterator Begin(void) const
void UniqueInit(Generator &rGen)
void Deterministic(const Generator &rGen, Generator &rResGen)
void aDeterministic(const Generator &rGen, Generator &rResGen)
std::string ToStringInteger(Int number)
std::string CollapsString(const std::string &rString, unsigned int len)