diag_decentralizeddiagnosis.cpp
Go to the documentation of this file.
1 /** @file diag_decentralizeddiagnosis.cpp Functions to test decentralized diagnosability and compute diagnosers.
2 */
3 
4 /*
5 
6 Copyright Tobias Barthel, Klaus Schmidt, Thomas Moor
7 
8 */
9 
11 
12 
13 using namespace std;
14 
15 namespace faudes {
16 
17 ///////////////////////////////////////////////////////////////////////////////
18 // Functions for decentralized diagnosability (co-diagnosability)
19 ///////////////////////////////////////////////////////////////////////////////
20 
21 
22 
23 // IsCoDiagnosable()
24 bool IsCoDiagnosable(const System& rGen, const Generator& rSpec, const vector<const EventSet*>& rAlphabets, std::string& rReportString) {
25 
26  FD_DD("IsCoDiagnosable()");
27 
28  // clear report
29  rReportString.clear();
30  EventSet obsEvents = rGen.ObservableEvents();
31 #ifdef FAUDES_DEBUG_DIAGNOSIS
32  obsEvents.DWrite();
33 #endif
34  Generator verifier; // Graph for co-diagnosability verification
35  Idx nullEvent = verifier.InsEvent("nullEvent"); // event that corresponds to the value 0
36  Idx negEvent = verifier.InsEvent("negEvent"); // event that corresponds to the value -1
37  Generator verifierTest; // verifier with eeent information
38  verifierTest.InjectAlphabet(rGen.Alphabet() ); // FIXME remove this.
39  verifierTest.InsEvent(nullEvent);
40  map<Idx, CoVerifierState> stateToVerifierMap;
41  map<CoVerifierState, Idx> verifierToStateMap;
42  stack<pair<Idx, CoVerifierState> > waitingStates;
43  StateSet doneStates;
44  // initialize the algorithm
45  EventSet fullAlphabet = rGen.Alphabet();
46  EventSet::Iterator eIt, eEndIt;
47  eEndIt = fullAlphabet.End();
48  Idx newState = verifier.InsInitState();
49  verifierTest.InsInitState(newState);
50  CoVerifierState newVerifierState = CoVerifierState(rAlphabets.size(), rSpec.InitState(), rGen.InitState(),NORMAL);
51  for(Idx i = 0; i < rAlphabets.size(); i++) // all decentralized versions of the specification are initialized
52  newVerifierState.mSpec1State[i] = rSpec.InitState();
53 
54  stateToVerifierMap[newState] = newVerifierState;
55  verifierToStateMap[newVerifierState ] = newState;
56  waitingStates.push(make_pair(newState, newVerifierState) );
57  // extend the verifier graph until no new nodes can be added
58  pair<Idx, CoVerifierState> currentState;
59  Idx blockingState; // = verifier.InsMarkedState();
61  map<CoVerifierState, Idx>::const_iterator vsIt;
62  Idx X2;
63  bool block = false; // set to true if the BLOCK state is reachable
64  FD_DD("Main loop");
65  while(waitingStates.empty() == false){
66  // take the first element from the stack
67  currentState = waitingStates.top();
68  waitingStates.pop();
69  doneStates.Insert(currentState.first);
70  #ifdef FAUDES_DEBUG_DIAGNOSIS
71  std::cout << "currentState: " << ToStringInteger(currentState.first) << " VerifierState: (";
72  for(unsigned k = 0; k < currentState.second.mSpec1State.size(); k++)
73  cout << rSpec.StateName(currentState.second.mSpec1State.at(k)) << " ";
74  cout << rSpec.StateName(currentState.second.mSpec2State) << " " << rGen.StateName(currentState.second.mPlantState) << " " << currentState.second.mLabel << ")" << endl;
75  #endif
76  // go over all possible events
77  eIt = fullAlphabet.Begin();
78  for(; eIt != eEndIt; eIt++){
79  // if the event is not observable, the specifications and the plant can evolve independently
80  if(obsEvents.Exists(*eIt) == false){
81  for(Idx i = 0; i < rAlphabets.size(); i++){
82  tIt = rSpec.TransRelBegin(currentState.second.mSpec1State.at(i),*eIt);
83  // transition in decentralized version of Spec for component i exists
84  if(tIt != rSpec.TransRelEnd(currentState.second.mSpec1State.at(i),*eIt) ){
85  newVerifierState = CoVerifierState(rAlphabets.size(), currentState.second.mSpec2State, currentState.second.mPlantState, NORMAL);
86  for(Idx j = 0; j < rAlphabets.size(); j++){ // determine new verifier state
87  if(j == i)
88  newVerifierState.mSpec1State[j] = tIt->X2;
89  else
90  newVerifierState.mSpec1State[j] = currentState.second.mSpec1State.at(j);
91  }
92  if(currentState.second.mLabel == CONFUSED ) // transition in spec1 from normal state// transition in spec1 from confused state
93  newVerifierState.mLabel = CONFUSED;
94  // check if the new VerifierState already exist snd insert new transitions (rule 1 and 4)
95 
96  vsIt = verifierToStateMap.find(newVerifierState);
97  // a new state is inserted into the verifier
98  if(vsIt == verifierToStateMap.end() ){
99 
100  newState = verifier.InsState();
101  verifierTest.InsState(newState);
102  verifier.SetTransition(currentState.first,nullEvent,newState);
103  verifierTest.SetTransition(currentState.first,*eIt,newState);
104  verifierToStateMap[newVerifierState] = newState;
105  stateToVerifierMap[newState] = newVerifierState;
106  if(doneStates.Exists(newState) == false)
107  waitingStates.push(make_pair(newState,newVerifierState) );
108  }
109  // a transition to the existing state is added
110  else{
111  verifierTest.SetTransition(currentState.first,*eIt,vsIt->second);
112  verifier.SetTransition(currentState.first,nullEvent,vsIt->second);
113 
114  }
115  }
116  }// for(Idx i = 0...
117  tIt = rGen.TransRelBegin(currentState.second.mPlantState,*eIt);
118  // transition in plant exists
119  if(tIt != rGen.TransRelEnd(currentState.second.mPlantState,*eIt) ){
120  X2 = tIt->X2;
121  newVerifierState = CoVerifierState(rAlphabets.size(), currentState.second.mSpec2State, X2, NORMAL); // prepare the new verifier state
122  newVerifierState.mSpec1State = currentState.second.mSpec1State;
123  if(currentState.second.mLabel == CONFUSED)
124  newVerifierState.mLabel = CONFUSED;
125  else{ // current state is NORMAL
126  tIt = rSpec.TransRelBegin(currentState.second.mSpec2State,*eIt);
127  if(tIt == rSpec.TransRelEnd(currentState.second.mSpec2State,*eIt) ){ // violation of the specification
128  newVerifierState.mLabel = CONFUSED;
129  }
130  else{ // correct behavior
131  newVerifierState.mSpec2State = tIt->X2;
132  }
133  }
134  // check if a new state has to be inserted into the verifier
135  vsIt = verifierToStateMap.find(newVerifierState);
136  // a new state is inserted into the verifier
137  if(vsIt == verifierToStateMap.end() ){
138  newState = verifier.InsState();
139  verifierTest.InsState(newState);
140  verifierToStateMap[newVerifierState] = newState;
141  stateToVerifierMap[newState] = newVerifierState;
142  if(doneStates.Exists(newState) == false)
143  waitingStates.push(make_pair(newState,newVerifierState) );
144  }
145  else
146  newState = vsIt->second;
147  // new transition in the verifier
148  if(newVerifierState.mLabel == NORMAL || (currentState.second.mLabel == CONFUSED && newVerifierState.mPlantState == currentState.second.mPlantState) ){ // normal behavior or confused behavior extended in the specification (rule 3 or 4)
149  verifierTest.SetTransition(currentState.first,*eIt,newState);
150  verifier.SetTransition(currentState.first,nullEvent,newState);
151  }
152  else{ // faulty behavior extended in the plant (rule 5)
153  verifierTest.SetTransition(currentState.first,*eIt,newState);
154  verifier.SetTransition(currentState.first,negEvent,newState);
155  }
156  }
157  }// (obsEvents.Exists(*eIt) == false)
158  else{
159  CoVerifierState unobsVerifierState; // new verifier state in case of unobservable events
160  bool allSpecsParticipate = true; // indicates if the plant can proceed together with all specs that have the current event
161  TransSet::Iterator plantIt, specIt;
162  plantIt= rGen.TransRelBegin(currentState.second.mPlantState, *eIt);
163  specIt = rSpec.TransRelBegin(currentState.second.mSpec2State, *eIt);
164  if(plantIt != rGen.TransRelEnd(currentState.second.mPlantState, *eIt) ){// there plant has a transition with *eIt
165  // the new state is confused
166  if(specIt == rSpec.TransRelEnd(currentState.second.mSpec2State, *eIt) || currentState.second.mLabel == CONFUSED){
167  newVerifierState = CoVerifierState(rAlphabets.size(), currentState.second.mSpec2State, plantIt->X2, CONFUSED);
168  }
169  else{// the new state is normal (spec follows plant)
170  newVerifierState = CoVerifierState(rAlphabets.size(), specIt->X2, plantIt->X2, NORMAL);
171  }
172  // the state only exists if all specifications that observe *eIt can follow
173  for(unsigned int i = 0; i < rAlphabets.size(); i++){
174  if(rAlphabets.at(i)->Exists(*eIt) == true){ // check if transition exists
175  tIt = rSpec.TransRelBegin(currentState.second.mSpec1State.at(i), *eIt);
176  if(tIt == rSpec.TransRelEnd(currentState.second.mSpec1State.at(i), *eIt) ){
177  allSpecsParticipate = false; // this subsystem can detect that there is a deviationfrom the specification
178  break;
179  }
180  else{ // execute the transition in the respective specification
181  newVerifierState.mSpec1State[i] = tIt->X2;
182  }
183  }
184  else
185  newVerifierState.mSpec1State[i] = currentState.second.mSpec1State.at(i);
186  }
187  if(allSpecsParticipate == true){ // a new state has to be inserted in the verifier
188  // check if a new state has to be inserted into the verifier
189  vsIt = verifierToStateMap.find(newVerifierState);
190  // a new state is inserted into the verifier
191  if(vsIt == verifierToStateMap.end() ){
192  newState = verifier.InsState();
193  verifierTest.InsState(newState);
194  verifierToStateMap[newVerifierState] = newState;
195  stateToVerifierMap[newState] = newVerifierState;
196  if(doneStates.Exists(newState) == false)
197  waitingStates.push(make_pair(newState,newVerifierState) );
198  }
199  else
200  newState = vsIt->second;
201  // new transition in the verifier
202  if(newVerifierState.mLabel == NORMAL){ // normal behavior
203  verifierTest.SetTransition(currentState.first,*eIt,newState);
204  verifier.SetTransition(currentState.first,nullEvent,newState);
205  }
206  else{ // faulty behavior extended in the plant and unnoticed by the specification
207  verifierTest.SetTransition(currentState.first,*eIt,newState);
208  verifier.SetTransition(currentState.first,negEvent,newState);
209  }
210  }
211  }
212  // go through all specifications and execute locally unobservable transitions
213  for(unsigned int i = 0; i < rAlphabets.size(); i++){
214  if(rAlphabets.at(i)->Exists(*eIt) == false){
215  tIt = rSpec.TransRelBegin(currentState.second.mSpec1State.at(i), *eIt);
216  if(tIt != rSpec.TransRelEnd(currentState.second.mSpec1State.at(i), *eIt) ){
217  newVerifierState = currentState.second;
218  newVerifierState.mSpec1State[i] = tIt->X2;
219  // check if a new state has to be inserted into the verifier
220  vsIt = verifierToStateMap.find(newVerifierState);
221  // a new state is inserted into the verifier
222  if(vsIt == verifierToStateMap.end() ){
223  newState = verifier.InsState();
224  verifierTest.InsState(newState);
225  verifierToStateMap[newVerifierState] = newState;
226  stateToVerifierMap[newState] = newVerifierState;
227  if(doneStates.Exists(newState) == false)
228  waitingStates.push(make_pair(newState,newVerifierState) );
229  }
230  else
231  newState = vsIt->second;
232 
233  verifierTest.SetTransition(currentState.first,*eIt,newState);
234  verifier.SetTransition(currentState.first,nullEvent,newState);
235  }
236  }
237  }
238  }
239  }// for(; *eIt ...)
240  // check if the Block state is reachable
241  if(rGen.TransRelBegin(currentState.second.mPlantState) == rGen.TransRelEnd(currentState.second.mPlantState) && currentState.second.mLabel == CONFUSED){
242  blockingState = verifier.InsMarkedState();
243  verifier.SetTransition(currentState.first,nullEvent,blockingState);
244  verifierTest.InsMarkedState(blockingState);
245  verifierTest.SetTransition(currentState.first,nullEvent,blockingState);
246  FD_DD("Blocking State Reachable");
247  block = true;
248  }
249  } // while(waiting...)
250  #ifdef FAUDES_DEBUG_DIAGNOSIS
251  if(verifier.Size() < 200){
252  verifier.GraphWrite("data/verifier.png");
253  verifierTest.GraphWrite("data/verifierTest.png");
254  }
255  #endif
256  //verifierTest.GraphWrite("data/verifierTest.png");
257  // Seach for cycles with "-1"-transitions (negEvent) in the verifier
258  list<StateSet> sccList;
259  StateSet rootSet;
260  // compute the strongly connected components in the verifier
261  ComputeScc(verifier,sccList,rootSet);
262  // Check if there is a "-1"-transition in any of the SCCs
263  list<StateSet>::const_iterator sccIt, sccEndIt;
264  sccIt = sccList.begin();
265  sccEndIt = sccList.end();
266  StateSet::Iterator stIt, stEndIt;
267  bool existsCycle = false;
268  for( ; sccIt != sccEndIt; sccIt++){
269 #ifdef FAUDES_DEBUG_DIAGNOSIS
270  sccIt->Write();
271 #endif
272  stIt = sccIt->Begin();
273  stEndIt = sccIt->End();
274  for(; stIt != stEndIt; stIt++){// check all states in the SCC
275  tIt = verifier.TransRelBegin(*stIt, negEvent);
276  if(tIt != verifier.TransRelEnd(*stIt, negEvent) && sccIt->Exists(tIt->X2) ){ // there is a transition with negEvent within the SCC
277  FD_DD("Confused Cycle Found");
278  existsCycle = true;
279  break;
280  }
281  }
282  if(existsCycle == true)
283  break;
284  }
285  if(block == true || existsCycle == true)
286  return false;
287  else
288  return true;
289 }
290 
291 
292 // DecentralizedDiagnoser(rGsubs, rKsubs, rDiagsubs, rReportString)
293 bool DecentralizedDiagnoser(const System& rGen, const Generator& rSpec, const std::vector<const EventSet*>& rAlphabets, std::vector<Diagnoser*>& rDiags, std::string& rReportString){
294 
295  FD_DD("DecentralizedDiagnoser()");
296  System copyGen = rGen;
297  rDiags.clear();
298  Diagnoser *newGen;
299  // clear report
300  rReportString.clear();
301  // Verify Codiagnosability
302  bool diagnosable = IsCoDiagnosable(rGen,rSpec,rAlphabets,rReportString);
303  // Compute diagnoser for each local site
304  for(unsigned int i = 0; i < rAlphabets.size(); i++){
305  // modify observable events of copyGen according to the local observation
306  copyGen.ClrObservable(copyGen.Alphabet() );
307  copyGen.SetObservable(*rAlphabets.at(i) );
308  newGen = new Diagnoser;
309  rDiags.push_back(newGen );
310  LanguageDiagnoser(copyGen,rSpec,*rDiags[i]);
311  }
312 
313  return diagnosable;
314 }
315 
316 // DecentralizedDiagnoser(rGsubs, rKsubs, rDiagsubs, rReportString)
317 void DecentralizedModularDiagnoser(const std::vector<const System*>& rGens, const Generator& rSpec, std::vector<Diagnoser*>& rDiags, std::string& rReportString){
318  Generator projSpec;
319  Diagnoser *newGen;
320  // clear report
321  rReportString.clear();
322  // Compute diagnoser for each local site
323  for(unsigned int i = 0; i < rGens.size(); i++){
324  // generate local versioin of the specification
325  Project(rSpec,rGens.at(i)->Alphabet(),projSpec);
326  newGen = new Diagnoser;
327  rDiags.push_back(newGen);
328  LanguageDiagnoser(*rGens.at(i),projSpec,*rDiags[i]);
329  }
330 }
331 
332 ///////////////////////////////////////////////////////////////////////////////
333 // RTI wrapper
334 ///////////////////////////////////////////////////////////////////////////////
335 
336 // IsCoDiagnosable()
337 bool IsCoDiagnosable(const System& rGen, const Generator& rSpec, const EventSetVector& rAlphabets){
338  std::string ignore;
339  // reorganize as std vector
340  std::vector<const EventSet*> alphabets;
341  Idx i;
342 
343  for(i = 0; i < rAlphabets.Size(); ++i)
344  alphabets.push_back(&rAlphabets.At(i));
345  return IsCoDiagnosable(rGen, rSpec, alphabets, ignore);
346 }
347 
348 // DecentralizedDiagnoser()
349 bool DecentralizedDiagnoser(const System& rGen, const Generator& rSpec, const EventSetVector& rAlphabets, GeneratorVector& rDiags){
350  std::string ignore;
351  // reorganize as std vector
352  std::vector<const EventSet*> alphabets;
353  std::vector<Diagnoser*> diags;
354  Idx i;
355 
356  for(i = 0; i < rAlphabets.Size(); ++i)
357  alphabets.push_back(&rAlphabets.At(i));
358 
359  bool ok = DecentralizedDiagnoser(rGen,rSpec,alphabets,diags,ignore);
360  for(i = 0; i < rAlphabets.Size(); ++i)
361  rDiags.Append(diags.at(i) );
362  rDiags.TakeOwnership();
363 
364  return ok;
365 }
366 
367 void DecentralizedModularDiagnoser(const SystemVector& rGens, const Generator& rSpec, GeneratorVector& rDiags){
368  std::string ignore;
369  // reorganize as std vector
370  std::vector<const System*> generators;
371  std::vector<Diagnoser*> diags;
372  Idx i;
373 
374  for(i = 0; i < rGens.Size(); ++i)
375  generators.push_back(&rGens.At(i));
376 
377  DecentralizedModularDiagnoser(generators,rSpec,diags,ignore);
378  for(i = 0; i < rGens.Size(); ++i)
379  rDiags.Append(diags.at(i) );
380  rDiags.TakeOwnership();
381 }
382 
383 
384 
385 } // namespace faudes
bool Exists(const Idx &rIndex) const
virtual const T & At(const Position &pos) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
const TaEventSet< EventAttr > & Alphabet(void) const
void ClrObservable(Idx index)
void SetObservable(Idx index)
EventSet ObservableEvents(void) const
void DWrite(const Type *pContext=0) const
Definition: cfl_types.cpp:226
virtual void Append(const Type &rElem)
Idx Size(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const EventSet & Alphabet(void) const
TransSet::Iterator TransRelBegin(void) const
std::string StateName(Idx index) const
TransSet::Iterator TransRelEnd(void) const
Idx InitState(void) const
bool InsEvent(Idx index)
void GraphWrite(const std::string &rFileName, const std::string &rOutFormat="", const std::string &rDotExec="dot") const
Idx Size(void) const
void InjectAlphabet(const EventSet &rNewalphabet)
#define FD_DD(message)
Definition: diag_debug.h:13
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2132
Iterator End(void) const
Definition: cfl_baseset.h:1913
Iterator Begin(void) const
Definition: cfl_baseset.h:1908
void LanguageDiagnoser(const System &rGen, const System &rSpec, Diagnoser &rDiagGen)
bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
uint32_t Idx
TdiagGenerator< AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoid > Diagnoser
bool DecentralizedDiagnoser(const System &rGen, const Generator &rSpec, const EventSetVector &rAlphabets, GeneratorVector &rDiags)
bool IsCoDiagnosable(const System &rGen, const Generator &rSpec, const EventSetVector &rAlphabets)
std::string ToStringInteger(Int number)
Definition: cfl_utils.cpp:43
void DecentralizedModularDiagnoser(const SystemVector &rGens, const Generator &rSpec, GeneratorVector &rDiags)

libFAUDES 2.33c --- 2025.05.15 --- c++ api documentaion by doxygen