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)
#define FD_WARN(message)
Debug: always report warnings.
#define FD_DF(message)
Debug: optional report on user functions.
Helper functions for projected generators.
Container for colors: this is a NameSet with its own static symboltable.
Idx Signature(void) const
Compute an Idx type signature for a Set.
Idx Insert(void)
Insert new index to set.
Set of indices with symbolic names.
bool Exists(const Idx &rIndex) const
Test existence of index.
void ClrEntry(Idx index)
Delete entry by index.
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Idx InsState(void)
Add new anonymous state to generator.
virtual void Clear(void)
Clear generator data.
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
const ATransSet & TransRel(void) const
Return reference to transition relation.
void InjectAlphabet(const EventSet &rNewalphabet)
Set mpAlphabet without consistency check.
void ClrObservable(Idx index)
Mark event unobservable (by index)
EventSet ControllableEvents(void) const
Get EventSet with controllable events.
void SetControllable(Idx index)
Mark event controllable (by index)
EventSet ForcibleEvents(void) const
Get EventSet with forcible events.
void SetForcible(Idx index)
Mark event forcible (by index)
EventSet UnobservableEvents(void) const
Get EventSet with unobservable events.
Allows to create colored marking generators (CMGs) as the common five tupel consisting of alphabet,...
void InsColors(Idx stateIndex, const ColorSet &rColors)
Insert multiple colors from a color set into an existing state.
void Colors(ColorSet &rColors) const
Insert all colors used in the generator to a given ColorSet.
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Write configuration data to a string.
void Write(const Type *pContext=0) const
Write configuration data to console.
StateSet::Iterator StatesBegin(void) const
Iterator to Begin() of state set.
StateSet::Iterator InitStatesBegin(void) const
Iterator to Begin() of mInitStates.
void ClearInitStates(void)
Clear all mInitStates.
bool InitStatesEmpty(void) const
Check if set of initial states are empty.
void DelEvents(const EventSet &rEvents)
Delete a set of events from generator.
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
void ClrTransition(Idx x1, Idx ev, Idx x2)
Remove a transition by indices.
SymbolTable * EventSymbolTablep(void) const
Get Pointer to EventSymbolTable currently used by this vGenerator.
bool DelEvent(Idx index)
Delete event from generator by index.
Idx InitStatesSize(void) const
Get number of initial states.
void InsEvents(const EventSet &events)
Add new named events to generator.
bool MarkedStatesEmpty(void) const
Check if set of marked states are empty.
void SetInitState(Idx index)
Set an existing state as initial state by index.
std::string TStr(const Transition &rTrans) const
Return pretty printable transition (eg for debugging)
std::string StateName(Idx index) const
State name lookup.
void Name(const std::string &rName)
Set the generator's name.
StateSet::Iterator StatesEnd(void) const
Iterator to End() of state set.
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
std::string EStr(Idx index) const
Pretty printable event name for index (eg for debugging).
void SetMarkedState(Idx index)
Set an existing state as marked state by index.
Idx InsInitState(void)
Create new anonymous state and set as initial state.
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
StateSet::Iterator InitStatesEnd(void) const
Iterator to End() of mInitStates.
EventSet UsedEvents(void) const
Return used events (executed in transitions)
EventSet UnusedEvents(void) const
Return unused events.
virtual void ClrEventAttribute(Idx index)
Clear attribute for existing event.
std::string SStr(Idx index) const
Return pretty printable state name for index (eg for debugging)
std::string UniqueStateName(const std::string &rName) const
Create a new unique symbolic state name.
bool Empty(void) const
Test whether if the TBaseSet is Empty.
bool Exists(const T &rElem) const
Test existence of element.
virtual void Clear(void)
Clear all set.
Iterator End(void) const
Iterator to the end of set.
virtual void InsertSet(const TBaseSet &rOtherSet)
Insert elements given by rOtherSet.
Iterator Begin(void) const
Iterator to the begin of set.
void mtcProject(const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
Minimized Deterministic projection.
void mtcInvProject(MtcSystem &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
void mtcProjectNonDet(MtcSystem &rGen, const EventSet &rProjectAlphabet)
Project generator to alphabet rProjectAlphabet.
void mtcDeterministic(const MtcSystem &rGen, MtcSystem &rResGen)
Make generator deterministic.
Methods for computing the natural projection of multitasking generators.
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
void mtcStateMin(MtcSystem &rGen, MtcSystem &rResGen)
State Minimization This function implements the (n*log n) set partitioning algorithm by John E.
void mtcUniqueInit(MtcSystem &rGen)
TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid > MtcSystem
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
Compute the accessible reach for a local automaton.
std::string ToStringInteger(Int number)
integer to string