op_obserververification.cpp
Go to the documentation of this file.
1 /** @file op_obserververification.cpp
2 
3 Methods to verify the obsrver condition for natural projections.
4 The observer condition is, e.g., defined in
5 K. C. Wong and W. M. Wonham, “Hierarchical control of discrete-event
6 systems,” Discrete Event Dynamic Systems: Theory and Applications, 1996.
7 In addition, methods to verify output control consistency (OCC) and
8 local control consistency (LCC) are provided. See for example
9 K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory
10 Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.
11 */
12 
13 /* FAU Discrete Event Systems Library (libfaudes)
14 
15  Copyright (C) 2006 Bernd Opitz
16  Exclusive copyright is granted to Klaus Schmidt
17 
18  This library is free software; you can redistribute it and/or
19  modify it under the terms of the GNU Lesser General Public
20  License as published by the Free Software Foundation; either
21  version 2.1 of the License, or (at your option) any later version.
22 
23  This library is distributed in the hope that it will be useful,
24  but WITHOUT ANY WARRANTY; without even the implied warranty of
25  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
26  Lesser General Public License for more details.
27 
28  You should have received a copy of the GNU Lesser General Public
29  License along with this library; if not, write to the Free Software
30  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
32 
33 
34 using namespace std;
35 
36 namespace faudes {
37 
38 bool IsObs(const Generator& rLowGen, const EventSet& rHighAlph){
39  OP_DF("IsObs(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
40  // Initialization of variables
41  EventSet newHighAlph = rHighAlph;
42  EventSet controllableEvents;
43  map<Transition,Idx> mapChangedTrans;
44  Generator genDyn(rLowGen);
45  map<Transition,Transition> mapChangedTransReverse;
46  map<Idx,Idx> mapStateToPartition;
47  map<Idx, EventSet> mapRelabeledEvents;
48  // One step of the observer algorithm: A dynamic system is computed that fulfills the one-step observer condition.
49  // if the result is equal to the original generator, then the natural projection on the high-level alphabet fulfills the observer property
50  calculateDynamicSystemClosedObs(rLowGen, newHighAlph, genDyn);
51  calculateDynamicSystemObs(rLowGen, newHighAlph, genDyn);
52  Generator genPart;
53  // compute coarsest quasi-congruence on the dynamic system
54  ComputeBisimulation(genDyn, mapStateToPartition, genPart);
55  // Extend the high-level alphabet according to the algorithm of Lei
56  ExtendHighAlphabet(rLowGen, newHighAlph, mapStateToPartition);
57  // return the result of the event extension
58  return newHighAlph == rHighAlph;
59 
60 }
61 
62 bool IsMSA(const Generator& rLowGen, const EventSet& rHighAlph){
63  OP_DF("IsMSA(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
64  // Initialization of variables
65  EventSet newHighAlph = rHighAlph;
66  EventSet controllableEvents;
67  map<Transition,Idx> mapChangedTrans;
68  Generator genDyn(rLowGen);
69  map<Transition,Transition> mapChangedTransReverse;
70  map<Idx,Idx> mapStateToPartition;
71  map<Idx, EventSet> mapRelabeledEvents;
72  // One step of the observer algorithm: A dynamic system is computed that fulfills the one-step observer condition.
73  // if the result is equal to the original generator, then the natural projection on the high-level alphabet fulfills the observer property
74  calculateDynamicSystemClosedObs(rLowGen, newHighAlph, genDyn);
75  calculateDynamicSystemMSA(rLowGen, newHighAlph, genDyn);
76  Generator genPart;
77  // compute coarsest quasi-congruence on the dynamic system
78  ComputeBisimulation(genDyn, mapStateToPartition, genPart);
79  // Extend the high-level alphabet according to the algorithm of Lei
80  ExtendHighAlphabet(rLowGen, newHighAlph, mapStateToPartition);
81  // return the result of the event extension
82  return newHighAlph == rHighAlph;
83 
84 }
85 
86 bool IsOCC(const System& rLowGen, const EventSet& rHighAlph){
87  OP_DF("IsOCC(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
88  EventSet controllableEvents = rLowGen.ControllableEvents();
89  // call the function that implements the algorithm
90  return IsOCC(rLowGen, controllableEvents, rHighAlph);
91 }
92 
93 bool IsOCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
94  OP_DF("IsOCC(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
95  //helpers:
96  StateSet::Iterator stIt, stEndIt;
97  stIt = rLowGen.StatesBegin();
98  stEndIt = rLowGen.StatesEnd();
99  TransSet::Iterator tIt, tEndIt;
100  // iteration over all states of rLowGen. If there is an uncontrollable feasible high-level event, backward reachability is conducted to determine if OCC holds.
101  for( ; stIt != stEndIt; stIt++){
102  tIt = rLowGen.TransRelBegin(*stIt);
103  tEndIt = rLowGen.TransRelEnd(*stIt);
104  for( ; tIt != tEndIt; tIt++){
105  if(rHighAlph.Exists(tIt->Ev) && !rControllableEvents.Exists(tIt->Ev) ){
106  // check if all local backward paths are uncontrollable
107  bool uncontrollable = backwardVerificationOCC(rLowGen, rControllableEvents, rHighAlph, *stIt);
108  // if not all paths are uncontrollable, OCC is violated
109  if(uncontrollable == false)
110  return false;
111  // otherwise, go to the next state
112  else
113  break;
114  }
115  }
116  }
117  return true;
118 }
119 
120 bool backwardVerificationOCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph, Idx currentState){
121  OP_DF("backwardVerificationOCC(" << rLowGen.Name() << "," << rControllableEvents.Name() << "," << rHighAlph.Name() << "," << currentState << ")");
122  // reverse transition relation
123  TransSetX2EvX1 tset_X2EvX1;
124  rLowGen.TransRel(tset_X2EvX1);
125  TransSetX2EvX1::Iterator tsIt, tsEndIt;
126  // todo list
127  std::stack<Idx> todo;
128  // algorithm: the locally backwards reachable states from current staet are
129  // evaluated. If a controllable event is found, OCC is violated.
130  StateSet doneStates;
131  doneStates.Insert(currentState);
132  todo.push(currentState);
133  // the local reachability is evaluated until no new state is found
134  while( !todo.empty() ){
135  const Idx current = todo.top();
136  todo.pop();
137  tsIt = tset_X2EvX1.BeginByX2(current);
138  tsEndIt = tset_X2EvX1.EndByX2(current);
139  for(; tsIt != tsEndIt; tsIt++){
140  // if the current transition is labeled with a high-level evnet
141  // it is skipped
142  if(rHighAlph.Exists(tsIt->Ev) )
143  continue;
144  // if the current transition is controllable, OCC is violated
145  else if( rControllableEvents.Exists(tsIt->Ev) )
146  return false;
147  else if( !doneStates.Exists(tsIt->X1) ){
148  todo.push(tsIt->X1);
149  doneStates.Insert(tsIt->X1);
150  }
151  }
152  }
153  return true;
154 }
155 
156 
157 bool IsLCC(const System& rLowGen, const EventSet& rHighAlph){
158  OP_DF("IsLCC(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
159  EventSet controllableEvents = rLowGen.ControllableEvents();
160  // call the function that implements the algorithm
161  return IsLCC(rLowGen, controllableEvents, rHighAlph);
162 }
163 
164 
165 /*
166 
167 In my opinion, the below algorithm to test LCC is incorrect.
168 It gives false negatives; e.g. stackfeeder example from
169 LRT "Uebung 12", data given below. I've
170 temporarily replaced IsLCC by a naive algorithm
171 which should be correct. This topic needs further
172 attentio .. tmoor, 07/20012
173 
174 
175 <Generator>
176 "Generator"
177 <Alphabet>
178 "wpar" "mv" +C+ "wplv" "r" "nr"
179 "stp" +C+
180 </Alphabet>
181 
182 <States>
183 <Consecutive>
184 1 8
185 </Consecutive>
186 </States>
187 
188 <TransRel>
189 1 "wpar" 2
190 2 "mv" 3
191 3 "nr" 4
192 4 "wplv" 5
193 5 "wpar" 8
194 5 "r" 6
195 6 "wpar" 7
196 6 "stp" 1
197 7 "stp" 2
198 8 "r" 7
199 </TransRel>
200 
201 <InitStates> 1 </InitStates>
202 <MarkedStates> 1 </MarkedStates>
203 </Generator>
204 
205 with high-level alphabet wpar and mv
206 */
207 
208 /*
209 bool IsLCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
210  OP_DF("IsLCC(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
211  // reverse transition relation
212  TransSetX2EvX1 tset_X2EvX1;
213  rLowGen.TransRel(tset_X2EvX1);
214  //helpers:
215  StateSet::Iterator stIt, stEndIt;
216  stIt = rLowGen.StatesBegin();
217  stEndIt = rLowGen.StatesEnd();
218  TransSet::Iterator tIt, tEndIt;
219  StateSet doneStates;
220  map<Idx, bool> localStatesMap;
221  map<Idx, bool>::const_iterator lsIt, lsEndIt;
222  // iteration over all states of rLowGen. If there is an uncontrollable feasible high-level event,
223  // backward reachability is conducted to determine if LCC holds.
224  for( ; stIt != stEndIt; stIt++){
225  tIt = rLowGen.TransRelBegin(*stIt);
226  tEndIt = rLowGen.TransRelEnd(*stIt);
227  for( ; tIt != tEndIt; tIt++){
228  if(rHighAlph.Exists(tIt->Ev) && !rControllableEvents.Exists(tIt->Ev) ){
229  doneStates.Clear();
230  localStatesMap.clear();
231  localStatesMap[*stIt] = false;
232  doneStates.Insert(*stIt);
233  // check if for all backward reachable states, a local uncontrollable backward paths exists
234  FD_WARN("IsLCC(): analyse state " << rLowGen.SStr(*stIt));
235  backwardVerificationLCC(tset_X2EvX1, rControllableEvents, rHighAlph, *stIt, *stIt, false, localStatesMap, doneStates);
236  // if for some state, all paths are controllable, LCC is violated
237  lsIt = localStatesMap.begin();
238  lsEndIt = localStatesMap.end();
239  for( ; lsIt != lsEndIt; lsIt++){
240  // if there is a state with only controllable paths, LCC is violated
241  if(lsIt->second == true) {
242  FD_WARN("IsLCC(): fail for state " << lsIt->first);
243  return false;
244  }
245  }
246  // the evaluation for the current state is finished
247  break;
248  }
249  }
250  }
251  FD_WARN("IsLCC(): pass");
252  return true;
253 }
254 
255 
256 void backwardVerificationLCC(
257  const TransSetX2EvX1& rTransSetX2EvX1,
258  const EventSet& rControllableEvents,
259  const EventSet& rHighAlph,
260  Idx exitState,
261  Idx currentState,
262  bool controllablePath,
263  map<Idx, bool>& rLocalStatesMap,
264  StateSet& rDoneStates)
265 {
266  OP_DF("backwardVerificationLCC(rTransSetX2EvX1," <<
267  rControllableEvents.Name() << "," << rHighAlph.Name() << "," << exitState << ","
268  << currentState << "," << controllablePath << ",rExitLocalStatesMap, rDoneStates)");
269  FD_WARN("IsLCC(): b-reach at state " << currentState);
270  // go along all backward transitions. Discard the goal state if it is reached via a high-level event or if it is in the rDoneStates and
271  // the controllability properties of the state do not change on the current path
272 
273  // helpers
274  TransSetX2EvX1::Iterator tsIt, tsEndIt;
275  tsIt = rTransSetX2EvX1.BeginByX2(currentState);
276  tsEndIt = rTransSetX2EvX1.EndByX2(currentState);
277  bool currentControllablePath;
278  // we iterate over all backward transitions of the currentState to establish backward reachability
279  for( ;tsIt != tsEndIt; tsIt++){
280  // states reachable via a high-level event
281  // are not in the local backward reach and the controllability property of the current exitState does not change
282  if( !rHighAlph.Exists(tsIt->Ev) && tsIt->X1 != exitState){
283  // if the state has not been visited, yet, the controllability of the current path are set in the rExitLocalStatesMap
284  if( !rDoneStates.Exists(tsIt->X1) ){
285  rDoneStates.Insert(tsIt->X1);
286  // the path is uncontrollable if the current transition has an uncontrollable event or the path was already uncontrollable
287  currentControllablePath = rControllableEvents.Exists(tsIt->Ev) || controllablePath;
288  FD_WARN("IsLCC(): record new state " << tsIt->X1 << " cntr=" << currentControllablePath);
289  rLocalStatesMap[tsIt->X1] = currentControllablePath;
290  // as the state has not been visited, yet, it is subject to a new backward reachability
291  backwardVerificationLCC(rTransSetX2EvX1, rControllableEvents, rHighAlph, exitState, tsIt->X1, currentControllablePath, rLocalStatesMap, rDoneStates);
292  }
293  else{ // for an existing state, the controllability value can change from controllable to uncontrollable (if
294  // a new uncontrollable path has been found). It is important to note, that the LCC condition implies that
295  // if there is one uncontrollable path, then the state is flagged uncontrollable except for the case of the
296  // given exitState that is always uncontrollable
297  currentControllablePath = rControllableEvents.Exists(tsIt->Ev) || controllablePath;
298  if(rLocalStatesMap[tsIt->X1] != currentControllablePath && currentControllablePath == false){
299  rLocalStatesMap[tsIt->X1] = false;
300  // as the controllabiity attribute of the current state changed it is subject to a new backward reachability
301  backwardVerificationLCC(rTransSetX2EvX1, rControllableEvents, rHighAlph, exitState, tsIt->X1, false, rLocalStatesMap, rDoneStates);
302  }
303  }
304  }
305  }
306 }
307 
308 */
309 
310 
311 // Naive replacement to test LCC with std. forward search for each state
312 // (complexity is quadratic in the number of states and
313 // linear in the number of events; actual performance is suboptimal,
314 // but I don't see how to get lower complexity)
315 
316 bool IsLCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
317  OP_DF("IsLCC(" << rLowGen.Name() << "," << rHighAlph.Name() << ")");
318  // iteration over all states of rLowGen.
319  StateSet::Iterator sit=rLowGen.StatesBegin();
320  for( ; sit != rLowGen.StatesEnd(); sit++){
321  // forward reachablity to figure all next high-level events
322  StateSet freach;
323  StateSet todo;
324  EventSet hievs;
325  todo.Insert(*sit);
326  while(!todo.Empty()) {
327  // take from todo stack
328  Idx cs = *todo.Begin();
329  todo.Erase(todo.Begin());
330  freach.Insert(cs);
331  // figure next states
332  TransSet::Iterator tit = rLowGen.TransRelBegin(cs);
333  TransSet::Iterator tit_end=rLowGen.TransRelEnd(cs);
334  for( ; tit != tit_end; tit++){
335  if(rHighAlph.Exists(tit->Ev)) {
336  hievs.Insert(tit->Ev);
337  continue;
338  }
339  if(!freach.Exists(tit->X2)) {
340  todo.Insert(tit->X2);
341  }
342  }
343  }
344  // forward reachablity to figure next high-level events by uncontr. paths
345  EventSet hievs_ucpath;
346  todo.Clear();
347  freach.Clear();
348  todo.Insert(*sit);
349  while(!todo.Empty()) {
350  // take from todo stack
351  Idx cs = *todo.Begin();
352  todo.Erase(todo.Begin());
353  freach.Insert(cs);
354  // figure next states
355  TransSet::Iterator tit = rLowGen.TransRelBegin(cs);
356  TransSet::Iterator tit_end=rLowGen.TransRelEnd(cs);
357  for( ; tit != tit_end; tit++){
358  if(rControllableEvents.Exists(tit->Ev)) {
359  continue;
360  }
361  if(rHighAlph.Exists(tit->Ev)) {
362  hievs_ucpath.Insert(tit->Ev);
363  continue;
364  }
365  if(!freach.Exists(tit->X2)) {
366  todo.Insert(tit->X2);
367  }
368  }
369  }
370  // test lcc
371  hievs = hievs - rControllableEvents;
372  hievs_ucpath = hievs_ucpath - rControllableEvents;
373  if(hievs_ucpath != hievs) {
374  OP_DF("IsLCC: failed at state " << rLowGen.SStr(*sit))
375  return false;
376  }
377  }
378  // no issues found
379  OP_DF(y"IsLCC: passed");
380  return true;
381 }
382 
383 
384 }// namespace faudes
bool Exists(const Idx &rIndex) const
bool Insert(const Idx &rIndex)
Iterator BeginByX2(Idx x2) const
Iterator EndByX2(Idx x2) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
EventSet ControllableEvents(void) const
StateSet::Iterator StatesBegin(void) const
const TransSet & TransRel(void) const
TransSet::Iterator TransRelBegin(void) const
void Name(const std::string &rName)
StateSet::Iterator StatesEnd(void) const
TransSet::Iterator TransRelEnd(void) const
std::string SStr(Idx index) const
bool Empty(void) const
Definition: cfl_baseset.h:1841
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2132
virtual void Clear(void)
Definition: cfl_baseset.h:1919
Iterator Begin(void) const
Definition: cfl_baseset.h:1908
virtual bool Erase(const T &rElem)
Definition: cfl_baseset.h:2036
const std::string & Name(void) const
Definition: cfl_baseset.h:1772
void ComputeBisimulation(const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition)
bool IsMSA(const Generator &rLowGen, const EventSet &rHighAlph)
void ExtendHighAlphabet(const Generator &rGen, EventSet &rHighAlph, map< Idx, Idx > &rMapStateToPartition)
bool IsObs(const Generator &rLowGen, const EventSet &rHighAlph)
uint32_t Idx
bool backwardVerificationOCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx currentState)
void calculateDynamicSystemMSA(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
void calculateDynamicSystemClosedObs(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
bool IsLCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
bool IsOCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
void calculateDynamicSystemObs(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
#define OP_DF(expr)
Definition: op_debug.h:31

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