36 StateSet::Iterator lit;
48 FD_DF(
"mtcUniqueInit: introducing new initial state: " << inituni);
50 FD_DF(
"mtcUniqueInit: introduce outgoing transitions: ");
54 FD_DF(
"mtcUniqueInit: " << inituni <<
"-" << tit->Ev <<
"-" << tit->X2);
62 FD_DF(
"mtcUniqueInit: set marked state: " << inituni);
75 std::vector<StateSet> power_states;
76 std::vector<Idx> det_states;
85 rEntryStatesMap.clear();
87 std::vector<StateSet> power_states;
88 std::vector<Idx> det_states;
92 std::vector<StateSet>::size_type i;
93 for (i = 0; i < power_states.size(); ++i) {
94 rEntryStatesMap.insert(std::pair<Idx,StateSet>(det_states[i], power_states[i]));
100 std::vector<Idx>& rDetStates,
MtcSystem& rResGen) {
102 rResGen.
Name(
"Det(" + rGen.
Name() +
")");
105 rPowerStates.clear();
115 typedef std::multimap< Idx,std::vector<StateSet>::size_type > T_HASHMAP;
117 std::vector<StateSet>::size_type current_vecindex;
118 std::pair< std::map<StateSet,Idx>::iterator,
bool > result;
121 StateSet::Iterator lit;
122 const Idx max_idx = std::numeric_limits<Idx>::max();
136 FD_DF(
"mtcDeterministic: created subset of initial states {"
137 << newset.
ToString() <<
"} with deterministic state index " << rGen.
SStr(newstate));
139 rPowerStates.push_back(newset);
140 rDetStates.push_back(newstate);
141 hashmap.insert(std::make_pair(newset.
Signature(), (
Idx)rPowerStates.size() - 1));
144 for (current_vecindex = 0; current_vecindex < rPowerStates.size(); ++current_vecindex) {
145 FD_DF(
"mtcDeterministic: current power set: {" << rPowerStates[current_vecindex].ToString() <<
146 "} -> " << rDetStates[current_vecindex]);
148 std::vector<StateSet> newset_vec;
149 std::vector<Idx> event_vec;
152 FD_DF(
"mtcDeterministic: starting multiway merge...");
153 std::list<TransSet::Iterator> merge_iterators;
154 std::vector<Transition> trans_vec;
158 for (lit = rPowerStates[current_vecindex].Begin();
159 lit != rPowerStates[current_vecindex].End(); ++lit) {
162 merge_iterators.push_back(tit);
163 FD_DF(
"mtcDeterministic: added merge iterator: " << rGen.
SStr(tit->X1)
164 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
169 while (! merge_iterators.empty()) {
170 Idx currentevent = max_idx;
171 std::list<TransSet::Iterator>::iterator i;
172 std::list<TransSet::Iterator>::iterator currentit = merge_iterators.end();
173 for (i = merge_iterators.begin(); i != merge_iterators.end(); ++i) {
174 if ((*i)->Ev < currentevent) {
175 currentevent = (*i)->Ev;
189 while (currentit != merge_iterators.end()) {
190 currentstate = (*currentit)->X1;
194 if (j == transrel_end) {
195 std::list<TransSet::Iterator>::iterator tmpit = currentit;
197 merge_iterators.erase(tmpit);
201 else if (j->X1 == currentstate) {
203 if (j->Ev == currentevent) {
204 trans_vec.push_back(*j);
205 FD_DF(
"Determine: adding transition to list: " << rGen.
SStr(j->X1)
206 <<
"-" << rGen.
EStr(j->Ev) <<
"-" << rGen.
SStr(j->X2));
216 std::list<TransSet::Iterator>::iterator tmpit = currentit;
218 merge_iterators.erase(tmpit);
227 FD_DF(
"mtcDeterministic: partitioning the transition vector...");
228 std::vector<Transition>::iterator tv_it;
231 for (tv_it = trans_vec.begin(); tv_it != trans_vec.end(); ++tv_it) {
232 if ((tv_it->Ev == lastevent) || (lastevent == 0)) {
234 lastevent = tv_it->Ev;
238 <<
"} with event " << rGen.
EStr(lastevent));
239 newset_vec.push_back(newset);
240 event_vec.push_back(lastevent);
243 lastevent = tv_it->Ev;
246 if (! newset.
Empty()) {
248 <<
"} with event " << rGen.
EStr(lastevent));
249 newset_vec.push_back(newset);
250 event_vec.push_back(lastevent);
252 FD_DF(
"mtcDeterministic: partitioning the transition vector finished");
253 FD_DF(
"mtcDeterministic: multiway merge finished");
256 std::vector<StateSet>::size_type nsv_index;
257 for (nsv_index = 0; nsv_index < newset_vec.size(); ++nsv_index) {
258 StateSet& currentset = newset_vec[nsv_index];
259 Idx currentevent = event_vec[nsv_index];
263 std::pair<T_HASHMAP::iterator,T_HASHMAP::iterator> phit
264 = hashmap.equal_range(sig);
265 T_HASHMAP::iterator hit = phit.first;
266 for (hit = phit.first; hit != phit.second; ++hit) {
268 if (currentset == rPowerStates[hit->second]) {
269 tmp_x2 = rDetStates[hit->second];
279 rPowerStates.push_back(currentset);
280 rDetStates.push_back(tmp_x2);
281 hashmap.insert(std::make_pair(sig, (
Idx)rPowerStates.size() - 1));
282 FD_DF(
"mtcDeterministic: added new state " << rGen.
SStr(tmp_x2)
283 <<
" for new subset {" << currentset.
ToString() <<
"}");
285 for (lit = currentset.
Begin(); lit != currentset.
End(); ++lit) {
288 FD_DF(
"mtcDeterministic: setting as colored: " << rGen.
SStr(tmp_x2));
292 rResGen.
SetTransition(rDetStates[current_vecindex], currentevent, tmp_x2);
297 FD_DF(
"mtcDeterministic: fixing names...");
299 std::vector<StateSet>::size_type i;
301 std::vector<Idx>::const_iterator dit;
302 for (i = 0; i < rPowerStates.size(); ++i) {
304 std::string name =
"{";
305 for (lit = rPowerStates[i].Begin(); lit != rPowerStates[i].End(); ++lit) {
307 name = name + rResGen.
StateName(*lit) +
",";
313 name.erase(name.length() - 1);
316 FD_DF(
"mtcDeterministic: setting state name \"" << name <<
"\" for index " << rDetStates[i]);
332 std::stack<Idx> todo;
335 StateSet::Iterator lit;
342 FD_DF(
"mtcProjectNonDet: todo add: " << rGen.
SStr(*lit));
347 while (! todo.empty()) {
348 currentstate = todo.top();
350 done.
Insert(currentstate);
351 FD_DF(
"mtcProjectNonDet: current state: " << rGen.
SStr(currentstate));
356 FD_DF(
"mtcProjectNonDet: local reach: " << reach.
ToString());
362 while(tit != tit_end) {
363 FD_DF(
"mtcProjectNonDet: current transition: " << rGen.
SStr(tit->X1)
364 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
365 if (! rProjectAlphabet.
Exists(tit->Ev)) {
366 FD_DF(
"mtcProjectNonDet: deleting current transition");
377 FD_DF(
"mtcProjectNonDet: relinking outgoing transitions...");
378 for (lit = reach.
Begin(); lit != reach.
End(); ++lit) {
381 for (; tit != tit_end; ++tit) {
382 if (rProjectAlphabet.
Exists(tit->Ev)) {
383 FD_DF(
"mtcProjectNonDet: relinking transition: " << rGen.
TStr(*tit) <<
" to " << rGen.
SStr(currentstate) <<
"--(" << rGen.
EStr(tit->Ev) <<
")-->" << rGen.
SStr(tit->X2));
385 if (! done.
Exists(tit->X2)) {
386 FD_DF(
"mtcProjectNonDet: todo push: " << rGen.
SStr(tit->X2));
393 if (!colors.
Empty()) {
394 FD_DF(
"mtcProjectNonDet: setting colored state " << rGen.
SStr(currentstate));
404 EventSet::Iterator eit;
405 for(eit = unused.
Begin(); eit != unused.
End(); ++eit){
411 rGen.
Name(
"MtcPro(" + rGen.
Name() +
")" );
429 #ifdef FAUDES_DEBUG_FUNCTION
430 FD_WARN(
"mtcProject: debug out")
431 copyGen.
Write(
"tmp_project_nd.gen");
435 #ifdef FAUDES_DEBUG_FUNCTION
436 FD_WARN(
"mtcProject: debug out")
437 tmp.
Write(
"tmp_project_d.gen");
441 #ifdef FAUDES_DEBUG_FUNCTION
442 FD_WARN(
"mtcProject: debug out")
443 rResGen.
Write(
"tmp_project_m.gen");
448 rResGen.
Name(rResGen.
Name()+
": mtcProject");
454 std::map<Idx,StateSet>& rEntryStatesMap,
MtcSystem& rResGen) {
459 std::map<Idx,StateSet> tmp_entrystatemap;
469 std::vector<StateSet> subsets;
470 std::vector<Idx> newindices;
475 std::vector<StateSet>::size_type i;
476 std::map<Idx,StateSet>::iterator esmit;
477 StateSet::Iterator sit;
478 for (i = 0; i < subsets.size(); ++i) {
480 for (sit = subsets[i].Begin(); sit != subsets[i].End(); ++sit) {
481 esmit = tmp_entrystatemap.find(*sit);
483 if (esmit == tmp_entrystatemap.end()) {
484 FD_WARN(
"mtcproject internal error");
492 rEntryStatesMap.insert(std::make_pair(newindices[i], tmpstates));
500 if(! (rProjectAlphabet >= rGen.
Alphabet() ) ){
501 std::stringstream errstr;
502 errstr <<
"Input alphabet has to contain alphabet of generator \"" << rGen.
Name() <<
"\"";
503 throw Exception(
"InvProject(Generator,EventSet)", errstr.str(), 506);
508 FD_DF(
"mtcInvProject: adding events \"" << newevents.
ToString() <<
"\" at every state");
509 StateSet::Iterator lit;
510 EventSet::Iterator eit;
512 for (eit = newevents.
Begin(); eit != newevents.
End(); ++eit)
Idx Signature(void) const
bool Exists(const Idx &rIndex) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
const TaEventSet< EventAttr > & Alphabet(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const ATransSet & TransRel(void) const
void InjectAlphabet(const EventSet &rNewalphabet)
void ClrObservable(Idx index)
EventSet ControllableEvents(void) const
void SetControllable(Idx index)
EventSet ForcibleEvents(void) const
void SetForcible(Idx index)
EventSet UnobservableEvents(void) const
void InsColors(Idx stateIndex, const ColorSet &rColors)
void Colors(ColorSet &rColors) const
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
void Write(const Type *pContext=0) const
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
void ClearInitStates(void)
bool InitStatesEmpty(void) const
void DelEvents(const EventSet &rEvents)
TransSet::Iterator TransRelBegin(void) const
void ClrTransition(Idx x1, Idx ev, Idx x2)
SymbolTable * EventSymbolTablep(void) const
Idx InitStatesSize(void) const
void InsEvents(const EventSet &events)
bool MarkedStatesEmpty(void) const
void SetInitState(Idx index)
std::string TStr(const Transition &rTrans) const
std::string StateName(Idx index) const
void Name(const std::string &rName)
StateSet::Iterator StatesEnd(void) const
TransSet::Iterator TransRelEnd(void) const
std::string EStr(Idx index) const
void SetMarkedState(Idx index)
bool StateNamesEnabled(void) const
StateSet::Iterator InitStatesEnd(void) const
EventSet UsedEvents(void) const
EventSet UnusedEvents(void) const
virtual void ClrEventAttribute(Idx index)
std::string SStr(Idx index) const
std::string UniqueStateName(const std::string &rName) const
bool Exists(const T &rElem) const
virtual void InsertSet(const TBaseSet &rOtherSet)
Iterator Begin(void) const
void mtcProject(const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
void mtcInvProject(MtcSystem &rGen, const EventSet &rProjectAlphabet)
void mtcProjectNonDet(MtcSystem &rGen, const EventSet &rProjectAlphabet)
void mtcDeterministic(const MtcSystem &rGen, MtcSystem &rResGen)
void mtcStateMin(MtcSystem &rGen, MtcSystem &rResGen)
void mtcUniqueInit(MtcSystem &rGen)
TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid > MtcSystem
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
std::string ToStringInteger(Int number)