106 cout <<
"Writing info-map for event " <<
event << endl;
107 const std::map<Idx,Idx> & pMap = infoMap[event];
108 std::map<Idx,Idx>::const_iterator mIt;
109 std::map<Idx,Idx>::const_iterator mItBegin = pMap.begin();
110 std::map<Idx,Idx>::const_iterator mItEnd = pMap.end();
111 if(mItBegin == mItEnd)
112 cout <<
"no entries for this event" << endl;
113 for(mIt=mItBegin; mIt != mItEnd; ++mIt)
114 cout <<
"state: " << (*mIt).first <<
" : occurrences: " << (*mIt).second << endl;
176 void partition(std::map<Idx,Idx>& rMapStateToPartition,
Generator& rGenPart);
186 void partition(std::map<Idx,Idx>& rMapStateToPartition);
195 void partition(std::list< StateSet >& rPartition);
208 vector< vector<Idx> >
suc;
209 vector< vector<Idx> >
pre;
230 std::vector<Pnode*>
W;
281 void computeInfoMap(
Pnode& B,
Pnode& Bstates,
Idx ev, vector<Idx>& tb);
289 void invImage(
Pnode& B,
Pnode& Bstates,
Idx ev, vector<Idx>& tb);
301 bool stateLeadsToPartition(
Idx state,
Pnode& node,
Idx ev);
310 void partitionClass(
Pnode& B);
319 void partitionSplitter(
Pnode& B);
328 void writeNode(
Pnode& node);
337 FD_DF(
"Bisimulation::Bisimulation(" << g.
Name() <<
")");
345 events.resize(gen->Alphabet().Size()+1);
347 for(; eit != gen->AlphabetEnd(); ++eit) {
352 states.resize(gen->States().Size()+1);
353 StateSet::Iterator sit=gen->StatesBegin();
354 for(; sit != gen->StatesEnd(); ++sit) {
356 states[max].idx=*sit;
357 states[max].suc.resize(events.size());
358 states[max].pre.resize(events.size());
361 for(; tit != gen->TransRelEnd(); ++tit) {
362 states[smap[tit->X1]].suc[emap[tit->Ev]].push_back(smap[tit->X2]);
363 states[smap[tit->X2]].pre[emap[tit->Ev]].push_back(smap[tit->X1]);
367 Pnode* universe = newnode();
371 for(;st<states.size();++st) universe->
states.push_back(st);
376 roDividers.insert(universe);
379 FD_DF(
"Bisimulation::Bisimulation: leaving function");
383 Bisimulation::~Bisimulation(
void)
385 vector<Pnode*>::iterator wit=W.begin();
386 vector<Pnode*>::iterator wit_end=W.end();
387 for(;wit!=wit_end;++wit)
delete *wit;
392 Pnode* Bisimulation::newnode(
void) {
399 nn->
infoMap.resize(events.size());
412 void Bisimulation::partitionSplitter(
Pnode& B) {
414 FD_DF(
"Bisimulation::partitionSplitter(B)");
415 FD_DF(
"Bisimulation::partitionSplitter: index of current coset is " << B.
index);
426 if(BSmallerPart->
nsize > BLargerPart->
nsize) {
431 FD_DF(
"Bisimulation::partitionSplitter: the smaller coset (chosen) has index: " << BSmallerPart->
index);
432 FD_DF(
"Bisimulation::partitionSplitter: the larger coset has index: " << BLargerPart->
index);
435 vector<Idx>::iterator sit;
436 vector<Idx>::iterator sit_end;
443 for(; ev < events.size(); ++ev){
447 if(!BParent->
activeEv[ev])
continue;
448 FD_DF(
"Bisimulation::partitionSplitter: partitioning for event " << gen->EventName(events[ev]));
454 BSmallerPart->
infoMap[ev].clear();
456 computeInfoMaps(*(BSmallerPart), BSmallerPart, BLargerPart, ev);
473 FD_DF(
"Bisimulation::partitionSplitter: computing predecessor cosets of parent coset with index " << BParent->
index);
474 set<Pnode*>::iterator rit;
475 for(rit=ro.begin(); rit!=ro.end(); ++rit) {
477 if((*rit)->nsize==1)
continue;
479 Idx testState = *((*rit)->states.begin());
480 FD_DF(
"Bisimulation::partitionSplitter: candidate coset index " << (*rit)->index <<
" and test state " << gen->SStr(testState));
481 if(stateLeadsToPartition(testState, *BParent, ev)) {
483 FD_DF(
"Bisimulation::partitionSplitter: coset index " << (*rit)->index <<
" is predecessor for parent coset with index " << (*BParent).index <<
" and event = " << gen->EStr(events[ev]) <<
" and was pushed on toDo-stack");
488 map<Idx, Idx> & imapParentEv = BParent->
infoMap[ev];
489 map<Idx, Idx> & imapSmallerEv = BSmallerPart->
infoMap[ev];
490 map<Idx, Idx>::const_iterator imapParentEvX1;
491 map<Idx, Idx>::const_iterator imapSmallerEvX1;
499 while(!toDo.empty()){
501 Pnode* rop=toDo.top();
503 FD_DF(
"Bisimulation::partitionSplitter: current coset taken from todo-stack has index " << rop->
index);
512 sit_end = rop->
states.end();
513 for(sit=rop->
states.begin(); sit!=sit_end; ++sit) {
514 if(imapSmallerEv.empty()){
517 imapSmallerEvX1=imapSmallerEv.find(*sit);
518 if(imapSmallerEvX1==imapSmallerEv.end()) {
521 imapParentEvX1=imapParentEv.find(*sit);
522 if(imapParentEvX1->second==imapSmallerEvX1->second)
543 sort(sX1.begin(), sX1.end());
544 sort(sX2.begin(), sX2.end());
545 sort(sX3.begin(), sX3.end());
551 if(!sX1.empty()) { nX1=newnode(); nX1->
nsize=sX1.size(); nX1->
states.swap(sX1); };
552 if(!sX2.empty()) { nX2=newnode(); nX2->
nsize=sX2.size(); nX2->
states.swap(sX2); };
553 if(!sX3.empty()) { nX3=newnode(); nX3->
nsize=sX3.size(); nX3->
states.swap(sX3); };
556 if((nX1!=NULL ? 1 : 0) + (nX2!=NULL ? 1 : 0) + (nX3!=NULL ? 1 : 0) <2)
continue;
559 if(nX1!=NULL) {ro.insert(nX1); roDividers.insert(nX1);};
560 if(nX2!=NULL) {ro.insert(nX2); roDividers.insert(nX2);};
561 if(nX3!=NULL) {ro.insert(nX3); roDividers.insert(nX3);};
565 roDividers.erase(rop);
578 switch( (nX1!=NULL ? 1 : 0) + (nX2!=NULL ? 2 : 0) + (nX3!=NULL ? 4 : 0) ) {
586 FD_DF(
"Bisimulation::partitionSplitter: coset " << rop->
index <<
" has been split into cosets X1 and X2");
594 FD_DF(
"Bisimulation::partitionSplitter: coset " << rop->
index <<
" has been split into cosets X1 and X3");
602 FD_DF(
"Bisimulation::partitionSplitter: coset " << rop->
index <<
" has been split into cosets X2 and X3");
610 FD_DF(
"Bisimulation::partitionSplitter: coset " << rop->
index <<
" has been split into cosets X1, X2 and X3");
612 Pnode* nX23=newnode();
634 BParent->
states=vector<Idx>();
645 roDividers.erase(BSmallerPart);
646 roDividers.erase(BLargerPart);
648 FD_DF(
"Bisimulation::partitionSplitter: leaving function");
656 FD_DF(
"Bisimulation::computeInfoMaps(" << node.
index <<
"," << pSmallerPart->
index <<
"," << pLargerPart->
index <<
"," << gen->EventName(ev) <<
")");
661 computeInfoMaps(*(node.
pFirstChild), pSmallerPart, pLargerPart, ev);
663 computeInfoMaps(*(node.
pSecondChild),pSmallerPart, pLargerPart, ev);
668 vector<Idx>::iterator tit;
669 vector<Idx>::iterator tit_end;
672 map<Idx,Idx>& imapLEv = pLargerPart->
infoMap[ev];
673 map<Idx,Idx>& imapSEv = pSmallerPart->
infoMap[ev];
674 map<Idx,Idx>::iterator imapLEvX1;
675 map<Idx,Idx>::iterator imapSEvX1;
678 vector<Idx>::iterator xit2=node.
states.begin();
679 vector<Idx>::iterator xit2_end=node.
states.end();
680 for(; xit2!=xit2_end; ++xit2) {
683 tit = states[*xit2].pre[ev].begin();
684 tit_end = states[*xit2].pre[ev].end();
685 for(; tit!=tit_end; ++tit) {
689 imapSEvX1=imapSEv.find(x1);
690 if(imapSEvX1!=imapSEv.end())
695 imapLEvX1=imapLEv.find(x1);
697 if(imapLEvX1->second==0) imapLEv.erase(imapLEvX1);
717 FD_DF(
"Bisimulation::computeInfoMaps: leaving function");
724 bool Bisimulation::stateLeadsToPartition(
Idx state,
Pnode& node,
Idx ev) {
725 FD_DF(
"Bisimulation::stateLeadsToPartition(" << state <<
"," << node.
index <<
"," << gen->EventName(ev) <<
")");
730 if(stateLeadsToPartition(state,*node.
pFirstChild,ev))
return true;
732 if(stateLeadsToPartition(state,*node.
pSecondChild,ev))
return true;
737 vector<Idx>::iterator tit = states[state].suc[ev].begin();
738 vector<Idx>::iterator tit_end = states[state].suc[ev].end();
739 for(;tit!=tit_end; ++tit) {
740 if(binary_search(node.
states.begin(),node.
states.end(),*tit))
return true;
785 void Bisimulation::partitionClass(
Pnode& B) {
787 FD_DF(
"Bisimulation::partitionClass(" << B.
index <<
")");
788 FD_DF(
"Bisimulation::partitionClass: index of passed coset is " << B.
index);
791 vector<Pnode*> addSet;
792 vector<Pnode*>::iterator addIt;
793 vector<Pnode*> removeSet;
794 vector<Pnode*>::iterator remIt;
796 FD_DV(
"Bisimulation::partitionClass: loop over events");
800 for(; ev<events.size(); ++ev) {
802 FD_DF(
"Bisimulation::partitionClass: partitioning for event " << gen->EventName(events[ev]));
805 computeInfoMap(B, B, ev, tb);
813 set<Pnode*>::iterator rit;
814 for(rit = ro.begin(); rit != ro.end(); ++rit) {
815 FD_DF(
"Bisimulation::partitionClass: candidate coset to be split has index " << (*rit)->index);
818 if((*rit)->nsize==1)
continue;
822 std::set_intersection((*rit)->states.begin(), (*rit)->states.end(), tb.begin(), tb.end(),
823 std::inserter(sXinter, sXinter.begin()));
826 if(sXinter.empty() || sXinter.size()==(*rit)->states.size())
continue;
827 FD_DF(
"Bisimulation::partitionClass: current coset with index " << (*rit)->index <<
" will be split");
830 roDividers.erase(*rit);
831 removeSet.push_back(*rit);
834 Pnode* nXinter= newnode();
835 nXinter->
nsize=sXinter.size();
836 nXinter->
states.swap(sXinter);
837 (*rit)->pFirstChild=nXinter;
841 Pnode* nXdiff = newnode();
842 std::set_difference((*rit)->states.begin(), (*rit)->states.end(), nXinter->
states.begin(), nXinter->
states.end(),
844 (*rit)->pSecondChild=nXdiff;
849 addSet.push_back(nXinter);
850 addSet.push_back(nXdiff);
851 roDividers.insert(nXinter);
852 roDividers.insert(nXdiff);
855 FD_DF(
"Bisimulation::partitionClass: the coset with index " << nXinter->
index <<
" has been added to addSet and to roDividers");
856 FD_DF(
"Bisimulation::partitionClass: the coset with index " << nXdiff->
index <<
" has been added to addSet and to roDividers");
857 FD_DF(
"Bisimulation::partitionClass: the candidate coset has been split");
860 if((*rit)->pParent!=NULL) {
861 FD_DF(
"Bisimulation::partitionClass: split coset has parent coset with index " << (*rit)->pParent->index);
862 if((*rit)->pParent->pFirstChild->pFirstChild!=NULL && (*rit)->pParent->pSecondChild->pSecondChild!=NULL && (*rit)->pParent->rostable) {
863 (*rit)->pParent->infoMap.clear();
864 (*rit)->pParent->states=vector<Idx>();
865 FD_DF(
"Bisimulation::partitionClass: info map of parent coset deleted");
871 FD_DF(
"Bisimulation::partitionClass: states of split coset " << (*rit)->index <<
" have been deleted");
876 FD_DF(
"Bisimulation::partitionClass: deleting split cosets from ro");
877 for(remIt=removeSet.begin(); remIt!=removeSet.end();++remIt)
882 FD_DF(
"Bisimulation::partitionClass: inserting #" << addSet.size() <<
" new cosets into ro");
883 for(addIt=addSet.begin();addIt!=addSet.end();++addIt)
894 roDividers.erase(&B);
899 FD_DF(
"Bisimulation::partitionClass(): done");
904 void Bisimulation::computeInfoMap(
Pnode& B,
Pnode& Bstates,
Idx ev, vector<Idx>& tb) {
906 FD_DF(
"Bisimulation::computeInfoMap(" << B.
index <<
"," << Bstates.
index <<
"," << gen->EventName(ev) <<
", Stateset&)");
907 FD_DF(
"Bisimulation::computeInfoMap: consider stateSet of coset " << Bstates.
index);
910 if(Bstates.
states.empty()) {
919 vector< Idx >::iterator tit;
920 vector< Idx >::iterator tit_end;
923 map<Idx, Idx>& imapBEv = B.
infoMap[ev];
924 map<Idx, Idx>::iterator imapBEvX1;
927 vector<Idx>::iterator xit2 = Bstates.
states.begin();
928 vector<Idx>::iterator xit2_end = Bstates.
states.end();
929 for(; xit2 != xit2_end; ++ xit2){
931 tit=states[*xit2].pre[ev].begin();
932 tit_end=states[*xit2].pre[ev].end();
933 for(; tit < tit_end; ++tit) {
938 imapBEvX1=imapBEv.find(x1);
939 if(imapBEvX1!=imapBEv.end()) ++imapBEvX1->second;
944 sort(tb.begin(),tb.end());
948 FD_DF(
"Bisimulation::computeInfoMap: leaving function");
962 vector<State>::iterator sit=states.begin();
963 if(sit!=states.end()) ++sit;
964 for(;sit!=states.end();++sit) {
970 vector< Idx >::iterator tit;
971 vector< Idx >::iterator tit_end;
972 vector<Idx>::iterator xit2;
977 xit2 = BSmaller.
states.begin();
978 for(; xit2 != BSmaller.
states.end(); ++xit2) {
980 tit=states[*xit2].pre[ev].begin();
981 tit_end=states[*xit2].pre[ev].end();
982 for(; tit < tit_end; ++tit) {
985 ++(states[x1].iscnt);
989 if(found) BSmaller.
activeEv[ev]=
true;
994 xit2 = BLarger.
states.begin();
995 for(; xit2 != BLarger.
states.end(); ++xit2) {
997 tit=states[*xit2].pre[ev].begin();
998 tit_end=states[*xit2].pre[ev].end();
999 for(; tit < tit_end; ++tit) {
1002 ++(states[x1].ilcnt);
1006 if(found) BLarger.
activeEv[ev]=
true;
1008 FD_DF(
"Bisimulation::setInfoMap: leaving function");
1013 void Bisimulation::invImage(
Pnode& B,
Pnode& Bstates,
Idx ev, vector<Idx>& tb) {
1016 if(Bstates.
states.empty()) {
1025 vector< Idx >::iterator tit;
1026 vector< Idx >::iterator tit_end;
1029 vector<Idx>::iterator xit2 = Bstates.
states.begin();
1030 for(; xit2 != Bstates.
states.end(); ++xit2) {
1032 tit=states[*xit2].pre[ev].begin();
1033 tit_end=states[*xit2].pre[ev].end();
1034 for(; tit < tit_end; ++tit) {
1041 sort(tb.begin(),tb.end());
1048 void Bisimulation::refine() {
1049 FD_DF(
"Bisimulation::refine()");
1051 set<Pnode*>::iterator roDivIt;
1055 while(!roDividers.empty()) {
1057 FD_WPC(ro.size()-roDividers.size(), ro.size(),
"Bisimulation: blocks/dividers: " << ro.size() <<
" / " << roDividers.size());
1060 roDivIt=roDividers.begin();
1061 while(roDivIt != roDividers.end()) {
1063 if(pParent == NULL) { roDivIt++;
continue; };
1064 if(pParent->
rostable !=
true) { roDivIt++;
continue; };
1068 if(roDivIt != roDividers.end()) {
1069 partitionSplitter(**roDivIt);
1073 roDivIt=roDividers.begin();
1074 partitionClass(**roDivIt);
1081 void Bisimulation::partition(std::map<Idx,Idx>& rMapStateToPartition,
Generator& rGenPart) {
1083 FD_DF(
"Bisimulation::partition(rMapStateToPartition," << rGenPart.
Name() <<
")");
1087 rMapStateToPartition.clear();
1090 set<Pnode*>::const_iterator cRoIt = ro.begin();
1091 set<Pnode*>::const_iterator cRoItEnd = ro.end();
1092 vector<Idx>::iterator cSIt;
1093 vector<Idx>::iterator cSItEnd;
1094 for(; cRoIt != cRoItEnd; ++cRoIt) {
1096 std::ostringstream ostr;
1098 FD_DF(
"Bisimulation::partition: new state " << newstate <<
" for coset "
1099 << (*cRoIt)->index );
1102 cSIt=(*cRoIt)->states.begin();
1103 cSItEnd=(*cRoIt)->states.end();
1104 for(; cSIt != cSItEnd; ++cSIt) {
1106 Idx st=states[*cSIt].idx;
1109 rMapStateToPartition[st] = newstate;
1112 if(gen->StateName(st)!=
"") ostr << gen->StateName(st) <<
",";
1113 else ostr << st <<
",";
1116 if(gen->ExistsInitState(st))
1119 if(gen->ExistsMarkedState(st))
1125 std::string statename = ostr.str();
1126 if(statename.length()>=1) statename.erase(statename.length()-1);
1127 statename =
"{" + statename +
"}";
1128 rGenPart.
StateName(newstate, statename);
1129 FD_DF(
"Bisimulation::partition: new state " << statename);
1138 for(; tIt != tItEnd; ++tIt) {
1140 rGenPart.
SetTransition(rMapStateToPartition[tIt->X1], tIt->Ev, rMapStateToPartition[tIt->X2]);
1141 FD_DF(
"Bisimulation::partition: adding transition: X1=" << rGenPart.
TStr(*tIt) );
1143 FD_DF(
"Bisimulation::partition: leaving function");
1149 void Bisimulation::partition(std::map<Idx,Idx>& rMapStateToPartition) {
1150 FD_DF(
"Bisimulation::partition(rMapStateToPartition)");
1154 rMapStateToPartition.clear();
1157 set<Pnode*>::const_iterator cRoIt = ro.begin();
1158 set<Pnode*>::const_iterator cRoItEnd = ro.end();
1159 vector<Idx>::iterator cSIt;
1160 vector<Idx>::iterator cSItEnd;
1161 for (; cRoIt != cRoItEnd; ++cRoIt) {
1162 cSIt=(*cRoIt)->states.begin();
1163 cSItEnd=(*cRoIt)->states.end();
1164 for(; cSIt!=cSItEnd; ++ cSIt) {
1166 Idx st=states[*cSIt].idx;
1167 rMapStateToPartition[st] = (*cRoIt)->index;
1170 FD_DF(
"Bisimulation::partition: leaving function");
1175 void Bisimulation::partition(std::list< StateSet >& rPartition) {
1176 FD_DF(
"Bisimulation::partition(rPartition)");
1182 set<Pnode*>::const_iterator cRoIt = ro.begin();
1183 for(; cRoIt != ro.end(); ++cRoIt) {
1184 if((*cRoIt)->states.size()<=1)
continue;
1186 vector<Idx>::iterator cSIt=(*cRoIt)->states.begin();
1187 for(; cSIt!=(*cRoIt)->states.end(); ++ cSIt) tb.
Insert(states[*cSIt].idx);
1188 rPartition.push_back(tb);
1190 FD_DF(
"Bisimulation::partition: leaving function");
1195 void Bisimulation::writeW(
void)
1197 FD_DF(
"Bisimulation:writeW()");
1198 cout <<
"Plotting the W-tree:" << endl;
1199 writeNode(**W.begin());
1203 void Bisimulation::writeNode(
Pnode& node)
1205 FD_DF(
"Bisimulation::writeNode(" << node.
index <<
")");
1206 cout <<
"Coset with index " << node.
index <<
" has the following states:" << endl;
1207 vector<Idx>::iterator cSIt;
1208 vector<Idx>::iterator cSItEnd;
1209 cSIt=node.
states.begin();
1210 cSItEnd=node.
states.end();
1211 for(; cSIt!=cSItEnd; ++ cSIt) cout << *cSIt <<
" ";
1214 cout <<
"Parent coset has index: " << node.
pParent->
index << endl;
1216 cout <<
"Coset is the root of the tree" << endl;
1230 cout <<
"Coset has no children" << endl;
1231 cout <<
"ro is stable with respect to this coset (1=yes; 0=no): " << node.
rostable << endl;
1246 void Bisimulation::writeRo(
void)
1248 FD_DF(
"Bisimulation::writeRo()");
1249 cout <<
"The Cosets with the following indices are in ro: " << endl;
1250 set<Pnode*>::iterator roIt;
1251 set<Pnode*>::iterator roItBegin =ro.begin();
1252 set<Pnode*>::iterator roItEnd = ro.end();
1253 for(roIt=roItBegin; roIt!=roItEnd; roIt++)
1254 cout << (*roIt)->index << endl;
1274 FD_DF(
"ComputeBisimulation(" << rGenOrig.
Name() <<
", rMapStateToPartition)");
1280 #ifdef FAUDES_DEBUG_FUNCTION
1281 cout <<
"The result of the partition refinement is:" << endl;
1285 FD_DF(
"ComputeBisimulation: leaving function");
1291 FD_DF(
"ComputeBisimulation(" << rGenOrig.
Name() <<
", rMapStateToPartition, " << rGenPart.
Name() <<
")");
1296 bisim.
partition(rMapStateToPartition, rGenPart);
1298 cout <<
"The result of the partition refinement is:" << endl;
1302 FD_DF(
"ComputeBisimulation: leaving function");
1308 FD_DF(
"ComputeBisimulation(" << rGenOrig.
Name() <<
", rPartition)");
1315 cout <<
"The result of the partition refinement is:" << endl;
1319 FD_DF(
"ComputeBisimulation: leaving function");
#define FD_WPC(cntnow, contdone, message)
std::set< Pnode * > roDividers
void partition(std::map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
bool SetTransition(Idx x1, Idx ev, Idx x2)
EventSet::Iterator AlphabetBegin(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)
void SetMarkedState(Idx index)
bool StateNamesEnabled(void) const
void ComputeBisimulation(const Generator &rGenOrig, std::list< StateSet > &rPartition)
vector< vector< Idx > > pre
vector< vector< Idx > > suc
void writeInfoMap(Idx event) const
std::vector< bool > activeEv
std::vector< std::map< Idx, Idx > > infoMap
std::vector< Idx > states