48 std::stringstream errstr;
49 errstr <<
"Alphabets of generators do not match.";
50 throw Exception(
"IsRelativelyMarked", errstr.str(), 100);
56 std::stringstream errstr;
57 errstr <<
"Arguments are expected to be nonblocking.";
58 throw Exception(
"IsRelativelyMarked", errstr.str(), 201);
65 std::stringstream errstr;
66 errstr <<
"Arguments are expected to be deterministic.";
67 throw Exception(
"IsRelativelyMarked", errstr.str(), 202);
72 std::map< std::pair<Idx,Idx> ,
Idx> revmap;
75 Product(rGenPlant,rGenCand,revmap,product);
78 std::map< std::pair<Idx,Idx> ,
Idx>::iterator rit;
79 for(rit=revmap.begin(); rit!=revmap.end(); ++rit) {
91 return rit==revmap.end();
100 FD_DF(
"IsRelativelyClosed(\"" << rGenPlant.
Name() <<
"\", \"" << rGenCand.
Name() <<
"\")");
104 std::stringstream errstr;
105 errstr <<
"Alphabets of generators do not match.";
106 throw Exception(
"IsRelativelyClosed", errstr.str(), 100);
109 #ifdef FAUDES_CHECKED
112 std::stringstream errstr;
113 errstr <<
"Arguments are expected to be nonblocking.";
114 throw Exception(
"IsRelativelyClosed", errstr.str(), 201);
118 #ifdef FAUDES_CHECKED
121 std::stringstream errstr;
122 errstr <<
"Arguments are expected to be deterministic.";
123 throw Exception(
"IsRelativelyClosed", errstr.str(), 202);
128 FD_DF(
"IsRelativelyClosed(..): perform product");
131 std::stack< std::pair<Idx,Idx> > todo;
133 std::pair<Idx,Idx> currentstates, newstates;
135 std::set< std::pair<Idx,Idx> > productstates;
137 StateSet::Iterator lit1, lit2;
139 std::set< std::pair<Idx,Idx> >::iterator rcit;
141 bool inclusion12=
true;
144 FD_DF(
"IsRelativelyClosed(..): perform product: adding all combinations of initial states to todo");
149 currentstates = std::make_pair(*lit1, *lit2);
150 todo.push(currentstates);
151 productstates.insert(currentstates);
152 FD_DF(
"IsRelativelyClosed(..): perform product: (" <<
153 *lit1 <<
"|" << *lit2 <<
")");
158 FD_DF(
"IsRelativelyClosed(..): perform product: Product: processing reachable states:");
159 while (! todo.empty() && inclusion12) {
163 currentstates = todo.top();
165 FD_DF(
"Processing (" << currentstates.first <<
"|"
166 << currentstates.second <<
")");
169 tit1_end = rGenCand.
TransRelEnd(currentstates.first);
171 tit2_end = rGenPlant.
TransRelEnd(currentstates.second);
173 bool resolved12=
true;
174 while((tit1 != tit1_end) && (tit2 != tit2_end)) {
176 if(tit1->Ev != curev1) {
177 if(!resolved12) inclusion12=
false;
182 if(tit1->Ev == tit2->Ev) {
184 newstates = std::make_pair(tit1->X2, tit2->X2);
186 rcit = productstates.find(newstates);
187 if(rcit == productstates.end()) {
188 todo.push(newstates);
189 productstates.insert(newstates);
190 FD_DF(
"Product: todo push: (" << newstates.first <<
"|"
191 << newstates.second <<
")");
197 else if (tit1->Ev < tit2->Ev) {
201 else if (tit1->Ev > tit2->Ev) {
206 if(!resolved12) inclusion12=
false;
209 #ifdef FAUDES_DEBUG_FUNCTION
210 FD_DF(
"IsRelativelyClosed(): Product: done");
212 FD_DF(
"IsRelativelyClosed(): Product: inclusion L(G1) <= L(G2) not satisfied");
217 if(!inclusion12)
return false;
220 std::set< std::pair<Idx,Idx> >::iterator rit;
221 for(rit=productstates.begin(); rit!=productstates.end(); ++rit) {
235 return rit==productstates.end();
251 only_in_plant.
Name(
"Only_In_Plant");
252 only_in_spec.
Name(
"Only_In_Specification");
253 std::stringstream errstr;
254 errstr <<
"Alphabets of generators do not match.";
255 if(!only_in_plant.
Empty())
256 errstr <<
" " << only_in_plant.
ToString() <<
".";
257 if(!only_in_spec.
Empty())
258 errstr <<
" " << only_in_spec.
ToString() <<
".";
259 throw Exception(
"SupCon/SupCon", errstr.str(), 100);
265 if ((plant_det ==
false) && (spec_det ==
true)) {
266 std::stringstream errstr;
267 errstr <<
"Plant generator must be deterministic, "
268 <<
"but is nondeterministic";
269 throw Exception(
"ControllableConsistencyCheck", errstr.str(), 201);
271 else if ((plant_det ==
true) && (spec_det ==
false)) {
272 std::stringstream errstr;
273 errstr <<
"Spec generator must be deterministic, "
274 <<
"but is nondeterministic";
275 throw Exception(
"ControllableConsistencyCheck", errstr.str(), 203);
277 else if ((plant_det ==
false) && (spec_det ==
false)) {
278 std::stringstream errstr;
279 errstr <<
"Plant and spec generator must be deterministic, "
280 <<
"but both are nondeterministic";
281 throw Exception(
"ControllableConsistencyCheck", errstr.str(), 204);
285 std::map< std::pair<Idx,Idx>,
Idx> rcmap;
296 std::map< std::pair<Idx,Idx>,
Idx>& rCompositionMap,
299 FD_DF(
"SupRelativelyClosed(" << &rPlantGen <<
"," << &rSpecGen <<
")");
303 if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
304 pResGen= rResGen.
New();
313 Product(rPlantGen, rSpecGen, rCompositionMap, pmarked, smarked, *pResGen);
319 if(!pmarked.
Exists(s))
continue;
320 if(smarked.
Exists(s))
continue;
326 if(pResGen != &rResGen) {
327 pResGen->
Move(rResGen);
336 FD_WARN(
"SupRelativelyPrefixClosed(): API depreciated; use SupRelativelyClosed()");
341 FD_WARN(
"SupRelativelyPrefixClosed(): API depreciated; use SupRelativelyClosed()");
const std::string & Name(void) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
const EventSet & Alphabet(void) const
virtual void Move(vGenerator &rGen)
TransSet::Iterator TransRelBegin(void) const
virtual vGenerator * New(void) const
StateSet::Iterator StatesEnd(void) const
TransSet::Iterator TransRelEnd(void) const
bool IsDeterministic(void) const
bool StateNamesEnabled(void) const
StateSet::Iterator InitStatesEnd(void) const
bool ExistsMarkedState(Idx index) const
void InjectAlphabet(const EventSet &rNewalphabet)
bool Exists(const T &rElem) const
void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
bool IsDeterministic(const vGenerator &rGen)
bool IsRelativelyMarked(const Generator &rGenPlant, const Generator &rGenCand)
void SupRelativelyClosed(const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
bool IsRelativelyClosed(const Generator &rGenPlant, const Generator &rGenCand)
void LoopCallback(bool pBreak(void))
void SupRelativelyClosedUnchecked(const Generator &rPlantGen, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
bool IsNonblocking(const GeneratorVector &rGvec)
bool IsRelativelyPrefixClosed(const Generator &rGenPlant, const Generator &rGenCand)
void SupRelativelyPrefixClosed(const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
std::string CollapsString(const std::string &rString, unsigned int len)