|
|
||||||
|
op_obserververification.cpp
Go to the documentation of this file.
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
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
93 bool IsOCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
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.
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 << ")");
209 bool IsLCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
222 // iteration over all states of rLowGen. If there is an uncontrollable feasible high-level event,
235 backwardVerificationLCC(tset_X2EvX1, rControllableEvents, rHighAlph, *stIt, *stIt, false, localStatesMap, doneStates);
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
278 // we iterate over all backward transitions of the currentState to establish backward reachability
281 // are not in the local backward reach and the controllability property of the current exitState does not change
283 // if the state has not been visited, yet, the controllability of the current path are set in the rExitLocalStatesMap
286 // the path is uncontrollable if the current transition has an uncontrollable event or the path was already uncontrollable
291 backwardVerificationLCC(rTransSetX2EvX1, rControllableEvents, rHighAlph, exitState, tsIt->X1, currentControllablePath, rLocalStatesMap, rDoneStates);
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
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);
316 bool IsLCC(const Generator& rLowGen, const EventSet& rControllableEvents, const EventSet& rHighAlph){
Definition: cfl_indexset.h:78 Definition: cfl_nameset.h:69 Definition: cfl_baseset.h:396 Definition: cfl_transset.h:242 TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator Definition: cfl_transset.h:273 Definition: cfl_cgenerator.h:278 EventSet ControllableEvents(void) const Definition: cfl_cgenerator.h:1132 Definition: cfl_generator.h:213 StateSet::Iterator StatesBegin(void) const Definition: cfl_generator.cpp:1057 TransSet::Iterator TransRelBegin(void) const Definition: cfl_generator.cpp:1067 StateSet::Iterator StatesEnd(void) const Definition: cfl_generator.cpp:1062 TransSet::Iterator TransRelEnd(void) const Definition: cfl_generator.cpp:1072 void ComputeBisimulation(const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition) Definition: cfl_bisimulation.cpp:1272 bool IsMSA(const Generator &rLowGen, const EventSet &rHighAlph) Definition: op_obserververification.cpp:62 void ExtendHighAlphabet(const Generator &rGen, EventSet &rHighAlph, map< Idx, Idx > &rMapStateToPartition) Definition: op_observercomputation.cpp:520 bool IsObs(const Generator &rLowGen, const EventSet &rHighAlph) Definition: op_obserververification.cpp:38 Definition: cfl_agenerator.h:43 bool backwardVerificationOCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx currentState) Definition: op_obserververification.cpp:120 void calculateDynamicSystemMSA(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn) Definition: op_observercomputation.cpp:195 void calculateDynamicSystemClosedObs(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn) Definition: op_observercomputation.cpp:46 bool IsLCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph) Definition: op_obserververification.cpp:316 bool IsOCC(const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph) Definition: op_obserververification.cpp:93 void calculateDynamicSystemObs(const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn) Definition: op_observercomputation.cpp:159 libFAUDES 2.33c --- 2025.05.15 --- c++ api documentaion by doxygen |