DiaDes  0.1
DIAgnosis of Discrete-Event System
Explanation.hh
Go to the documentation of this file.
1 
9 #ifndef __DIADES__AUTOMATA__EXPERIMENTAL__EXPLANATION__HH
10 #define __DIADES__AUTOMATA__EXPERIMENTAL__EXPLANATION__HH
11 
12 #include<unordered_map>
13 #include<unordered_set>
14 #include<list>
24 
25 
26 namespace Diades {
27  namespace Automata {
28  namespace Experimental {
29 
31 
33 
46  template<typename _SPId,typename _ISId,typename _NSPId = NullValue<_SPId>,typename _NISId = NullValue< _ISId>>
49  const LocStateMap & levels)
50  {
51  auto it = fsa.outputTransitionBegin(state);
52  bool result = it != fsa.outputTransitionEnd(state);
53  int commonLevel = -1;
54  while(result && it != fsa.outputTransitionEnd(state))
55  {
56  result = (levels[it->target()] != -1);
57  if(result)
58  {
59  if(commonLevel == -1)
60  {
61  commonLevel = levels[it->target()];
62  }
63  result = (commonLevel == levels[it->target()]);
64  }
65  ++it;
66  }
67  LP(Msg("\\item The state %1% is %2% considered as a no-choice state.\n")
68  % fsa.getStatePropertyId(state)
69  % (result?"definitely":"not yet"));
70  return result;
71  }
72 
73 
92  template<typename _SPId,
93  typename _ISId,
94  typename _NSPId = NullValue<_SPId>,
95  typename _NISId = NullValue< _ISId>>
98  int currentLevel,
99  LocStateMap & levels,
101  std::unordered_set<typename FiniteAutomaton<_SPId,_ISId,_NSPId,_NISId>::State> & tagged,
102  std::unordered_set<typename FiniteAutomaton<_SPId,_ISId,_NSPId,_NISId>::State> & visited)
103  {
105  LP(Msg("\\item State %1% is tagged at level %2%.\n") % fsa.getStatePropertyId(state) % currentLevel);
106  levels[state] = currentLevel;
107  tagged.insert(state);
108  visited.insert(state);
109  if(!fsa.isInitial(state))
110  {
111  std::for_each(fsa.inputTransitionBegin(state),
112  fsa.inputTransitionEnd(state),
113  [&](Transition t)
114  {
115  if((levels[t.source()]== -1) && (visited.find(t.source()) == visited.end()))
116  {
117  LP(Msg("\\item State %1% is a non-visited predecessor of State %2% and is inserted.\n")
118  % fsa.getStatePropertyId(t.source())
119  % fsa.getStatePropertyId(state));
120  states.insert(states.end(),t.source());
121  visited.insert(t.source());
122  }
123  });
124  }
125  }
126 
127 
128  template<typename _SPId,
129  typename _ISId,
130  typename _NSPId = NullValue<_SPId>,
131  typename _NISId = NullValue< _ISId>>
134  int currentLevel,
135  LocStateMap & levels)
136  {
137  bool result = !states.empty();
138  if(result)
139  {
140  LP(Msg("\\item The number of states to initially assign is %1%.\n") % states.size());
142  using ListStates = std::list<State>;
143  using ListStatesIterator = typename ListStates::const_iterator;
144  // first, any states that are currently in 'states' must be tagged with
145  // the current level 'currentLevel'
146  // then any predecessor must be inserted in 'states'. (see setLevelAndPropagate)
147  // they are inserted after the state '*last' that is the last state initially
148  // present in 'states'.
149  std::unordered_set<State> tagged;
150  std::unordered_set<State> visited;
151  auto it = states.begin();
152  auto last = --states.end();
153  while(it!= last)
154  {
155  setLevelStateAndPropagate(fsa,states,currentLevel,levels,*it,tagged,visited);
156  it = states.erase(it);
157  }
158  if(it==last)
159  {
160  setLevelStateAndPropagate(fsa,states,currentLevel,levels,*it,tagged,visited);
161  states.erase(it);
162  }
163 
164 
165  // this iterator is a reference to the first element of the list of postponed states present
166  // at the end of the list 'states'
167  // for now, none is postponed, the list of postponed states is empty at the end of the 'states' list
168  ListStatesIterator firstPostponedStateIt = states.end();
169 
170 
171  while(firstPostponedStateIt != states.begin())
172  {
173  if(levels[states.front()]==-1)
174  {
175  if(isNotChoiceState(fsa,states.front(),levels))
176  {
177  setLevelStateAndPropagate(fsa,states,currentLevel,levels,states.front(),tagged,visited);
178  // this state is definitely not a choice state
179  // it has definitely the current level
180  firstPostponedStateIt = states.end();
181  }
182  else
183  {
184  // this state might be a choice state or not (I postpone the decision)
185  if(firstPostponedStateIt == states.end())
186  {
187  firstPostponedStateIt = states.insert(states.end(),states.front());
188  }
189  else
190  {
191  states.insert(states.end(),states.front());
192  }
193  }
194  }
195  states.pop_front();
196  }
197  }
198  // so here 'states' contains the set of predecessors that are definitely choice state at a upper level
199  // I simply return them. It might be empty.
200  return result;
201  }
202 
203 
204 
205  template<typename _SPId,
206  typename _ISId,
207  typename _NSPId = NullValue<_SPId>,
208  typename _NISId = NullValue< _ISId>>
209  bool levelOfChoice(const FiniteAutomaton<_SPId,
210  _ISId,
211  _NSPId,
212  _NISId> & fsa,
213  LocStateMap & result)
214  {
215  using FA = FiniteAutomaton<_SPId,
216  _ISId,
217  _NSPId,
218  _NISId>;
219  result.clear();
220  result.init(fsa.behaviour(),fsa.numberOfStates(),-1);
221  int currentLevel = 0;
222  std::list<typename FA::State> states;
223  states.insert(states.end(),fsa.acceptingStateBegin(),fsa.acceptingStateEnd());
224  auto ok = !states.empty();
225  while(ok && !states.empty())
226  {
227  LP(R"(\paragraph{Computing level )");
228  LP(Msg("%1%}\n")%currentLevel);
229  LP("\\begin{itemize}\n");
230  ok = setLevel(fsa, states, currentLevel++,result);
231  LP("\\end{itemize}\n");
232  }
233  return ok;
234  }
235 
236  using Observation = std::string;
237  using Observations = std::vector<Observation>;
238  using Observables = std::set<DdAutFA::EventPropertyId>;
239  using Matcher = std::unordered_map<Observation,Observables>;
240 
241 
252  template<typename Fsm>
254  unordered_set<typename Fsm::Transition> & solutions)
255  {
256 
257  using State = typename Fsm::State;
258  using Transition = typename Fsm::Transition;
259  using MinMaxPathEdgeMap = Diades::Graph::EdgeMap< pair<int,bool> >;
260 
261  stack<Transition> visitingTransitions;
262  // minMaxPath[s] = (minMaxPathLoc, updated)
263  // the current minMaxPathLoc is either -1 or the current level of choice
264  // that is the current minimal level of choice among the set of maximal
265  // level of choice found in the current set of visited paths.
266  MinMaxPathEdgeMap minMaxPath(traces.behaviour(),
267  traces.numberOfTransitions(),
268  std::make_pair(-1,false));
269  // any acceptor states should have a level of Choice set to 0
270  // I initialise a DFS from the range of the acceptor states to move backward
271  // and set up the information minmaxpath: for every state s minmaxpath[s] is
272  // the minimal level of choice we can find among the maximal level of choices
273  // we can find in a path from the state s (level of choice of s not included)
274  // to an acceptor state. minmaxpath[acceptor] = 0: by construction there is
275  // no path from an acceptor state so maxpaths[acceptor] = 0 , so is
276  // minmaxpath[acceptor] =0
277  // I maintained a set of potential solutions. At the end, solutions
278  // will only keep the effective choice transitions
279  std::for_each(traces.acceptingStateBegin(),
280  traces.acceptingStateEnd(),
281  [&](State s){
282  std::for_each(traces.inputTransitionBegin(s), traces.inputTransitionEnd(s),
283  [&](Transition t)
284  {
285  minMaxPath[t] = std::make_pair(levelOfChoice[t.target()],true);
286  visitingTransitions.push(t);
287  });
288  });
289 
290  solutions.clear();
291 
292  while(!visitingTransitions.empty())
293  {
294  auto currentTransition = visitingTransitions.top();
295  if(levelOfChoice[currentTransition.source()] > minMaxPath[currentTransition].first)
296  {
297  solutions.insert(currentTransition);
298  }
299  else
300  {
301  solutions.erase(currentTransition);
302  }
303  visitingTransitions.pop();
304  minMaxPath[currentTransition].second = false;
305 
306 
307  // search backwards
308  auto currentState = currentTransition.source();
309  std::for_each(traces.inputTransitionBegin(currentState),
310  traces.inputTransitionEnd(currentState),
311  [&](Transition t){
312  bool mustBeVisited = false;
313  if(minMaxPath[t].first == -1)
314  {
315  minMaxPath[t].first = std::max(levelOfChoice[t.target()],minMaxPath[currentTransition].first);
316  mustBeVisited = true;
317  }
318  else
319  {
320  int locPathMax = std::max(levelOfChoice[t.target()],minMaxPath[currentTransition].first);
321  if(minMaxPath[t].first > locPathMax)
322  {
323  minMaxPath[t].first = locPathMax;
324  mustBeVisited = true;
325  }
326  }
327  if(mustBeVisited)
328  {
329 
330 
331  if(!minMaxPath[t].second)
332  {
333  visitingTransitions.push(t);
334  minMaxPath[t].second = true;
335  }
336  }
337  });
338 
339  }
340 
341 
342  }
343 
344  std::unordered_set<DdAutFA::Transition> getSafeAlternatives(const DdAutFA & traces,
345  DdAutFA::State state,
346  const ExplLocStateMap & levelOfChoiceInTraces,
348  const DdAutFA & fsa,
349  const LocStateMap & levelOfChoiceInFsa,
350  const DdAutStateManager & sManager,
351  const DdAutEventManager & eManager)
352  {
353 
354  std::unordered_set<DdAutFA::Transition> result;
355  auto source = mapping[state]; // 'source' is state s_A||P in DX
356  for(auto it = fsa.outputTransitionBegin(source);
357  it != fsa.outputTransitionEnd(source);
358  ++it)
359  {
360  auto targetLevel = levelOfChoiceInFsa[it->target()]; // this is \Ksi(q')
361  auto it2 = traces.outputTransitionBegin(state); // 'state' is state s in DX so it2 iterates over s^{\bullet}
362  bool isGreater = true;
363  while(isGreater && it2 != traces.outputTransitionEnd(state))
364  {
365  isGreater = targetLevel > levelOfChoiceInTraces[it2->target()]; // it2->target is s''
366  ++it2;
367  }
368  if(isGreater)
369  {
370  result.insert(*it);
371  }
372  }
373  return result;
374  }
375 
376  template<typename Fsm>
377  using SafeAlt = std::unordered_map<typename Fsm::State, std::unordered_set<typename Fsm::Transition> >;
378 
379 
380 
381  template<typename StateIterator>
382  bool explainFromStates(StateIterator begin,
383  StateIterator end,
384  const DdAutFA & fsa,
385  const DdAutStateManager & sManager,
386  const DdAutEventManager & eManager,
387  const Observations & observations,
388  Observables & observables,
389  DdAutFA & explanations,
390  DdAutFA & traces,
391  DdAutStateManager & sManagerExplanation,
392  const Matcher & matcher,
393  const LocStateMap & levelOfChoice,
394  SafeAlt<DdAutFA> & safeAlternatives)
395  {
396  using Fsa = DdAutFA;
397  using Transition = Fsa::Transition;
398  using State = Fsa::State;
399  using TransList = std::list<Transition>;
400  ExplLocStateMap levelOfChoiceInExplanation(traces.behaviour() ,10000,-1);
401  StMap<State> mapping(traces.behaviour());
402  auto currentStates = std::make_shared<BeliefState<Fsa>>(fsa);
403  currentStates->insertStates(begin,end);
404  TransList transitions;
405  TransList targetTransitions;
406  for(size_t i = 0; i < observations.size(); ++i)
407  {
408  Observables forbidden;
409  auto & observableCandidates = matcher.find(observations[i])->second;
410  std::set_difference(observables.begin(), observables.end(),
411  observableCandidates.begin(), observableCandidates.end(),
412  std::inserter(forbidden, forbidden.begin()));
413  currentStates = currentStates->nextReachableBeliefState([&](Transition t) { return observableCandidates.find(fsa.getEvent(t)) != observableCandidates.end(); },
414  [&](Transition t) { return forbidden.find(fsa.getEvent(t))!= forbidden.end(); },
415 
416  std::inserter(transitions,transitions.begin()),
417  std::inserter(targetTransitions,targetTransitions.begin()));
418  // isGoal and isForbidden -> find a way to make them time constant
419  for(auto transition: transitions)
420  {
421  std::stringstream streamSource;
422  streamSource << levelOfChoice[transition.source()] << "_"
423  << sManager.getStateProperty(fsa.getStatePropertyId(transition.source()))
424  << "_" << i;
425  std::stringstream streamTarget;
426  streamTarget << levelOfChoice[transition.target()] << "_"
427  << sManager.getStateProperty(fsa.getStatePropertyId(transition.target()))
428  << "_" << i;
429  auto sourceId = sManagerExplanation.statePropertyId(streamSource.str());
430  auto targetId = sManagerExplanation.statePropertyId(streamTarget.str());
431  traces.newTransition(sourceId, targetId, fsa.getEvent(transition));
432  mapping[traces.getState(sourceId)] = transition.source();
433  mapping[traces.getState(targetId)] = transition.target();
434  if(i == 0)
435  {
436  if(fsa.isInitial(transition.source()))
437  {
438  traces.setInitial(traces.getState(sourceId));
439  }
440  if(fsa.isInitial(transition.target()))
441  {
442  traces.setInitial(traces.getState(targetId));
443  }
444  }
445  levelOfChoiceInExplanation[traces.getState(sourceId)] = levelOfChoice[transition.source()];
446  levelOfChoiceInExplanation[traces.getState(targetId)] = levelOfChoice[transition.target()];
447 
448  }
449  for(auto transition: targetTransitions)
450  {
451  std::stringstream streamSource;
452  streamSource << levelOfChoice[transition.source()] << "_"
453  << sManager.getStateProperty(fsa.getStatePropertyId(transition.source()))
454  << "_" << i;
455  std::stringstream streamTarget;
456  streamTarget << levelOfChoice[transition.target()] << "_"
457  << sManager.getStateProperty(fsa.getStatePropertyId(transition.target()))
458  << "_" << i+1;
459  auto sourceId = sManagerExplanation.statePropertyId(streamSource.str());
460  auto targetId = sManagerExplanation.statePropertyId(streamTarget.str());
461  traces.newTransition(sourceId, targetId, fsa.getEvent(transition));
462  if(i == observations.size()-1)
463  {
464  traces.setAcceptingState(traces.getState(targetId));
465  }
466  levelOfChoiceInExplanation[traces.getState(sourceId)] = levelOfChoice[transition.source()];
467  levelOfChoiceInExplanation[traces.getState(targetId)] = levelOfChoice[transition.target()];
468  }
469  transitions.clear();
470  targetTransitions.clear();
471  }
472 
473  std::unordered_set<Transition> effectiveChoiceTransitions;
474  extractEffectiveChoiceTransitions(traces, levelOfChoiceInExplanation,
475  effectiveChoiceTransitions);
476 
477 
478  BsMap<Fsa> bsMap;
479  CstStMap<State> stMap;
480  bool result = project(traces, explanations,
481  [&](Transition t)
482  {
483  return effectiveChoiceTransitions.find(t) != effectiveChoiceTransitions.end();
484  },
485  bsMap,
486  stMap);
487  if(result)
488  {
489  std::for_each(effectiveChoiceTransitions.begin(),
490  effectiveChoiceTransitions.end(),
491  [&](Transition t)
492  {
493  auto safeAlternativeTransitions = getSafeAlternatives(traces,
494  t.source(),
495  levelOfChoiceInExplanation,
496  mapping,
497  fsa,
498  levelOfChoice,sManager,eManager);
499  auto effectiveTransitionTargetInExpl = stMap[t.target()];
500  std::for_each(explanations.inputEventTransitionBegin(effectiveTransitionTargetInExpl,traces.getEvent(t)),
501  explanations.inputEventTransitionEnd(effectiveTransitionTargetInExpl,traces.getEvent(t)),
502  [&](Transition trans)
503  {
504  auto trSourceInExpl = trans.source();
505  // if in the belief state in bsMap(trSourceInExpl) there is t.source()
506  // then I am sure that trans is one copy of the effectiveTransition
507  // I am looking for in explanation.
508  if(bsMap[trSourceInExpl]->findState(t.source())!= bsMap[trSourceInExpl]->end())
509  {
510  std::for_each(safeAlternativeTransitions.begin(),
511  safeAlternativeTransitions.end(),
512  [&](Transition safeTrans)
513  {
514  safeAlternatives[trSourceInExpl].insert(safeTrans);
515  });
516  }
517 
518  });
519  });
520  }
521  return result;
522  }
523 
524  Matcher
526  const std::vector<std::string> & observations)
527  {
528  Matcher result;
529  for(const auto & obs : observations)
530  {
531  if(result.find(obs) == result.end())
532  {
533  std::for_each(eManager.begin(),eManager.end(),
534  [&](DdAutEventManager::EventId eventId)
535  {
536  if(eManager.getEvent(eventId).find(obs)!=DdAutEventManager::Event::npos)
537  {
538  Matcher::iterator it = result.find(obs);
539  if(it==result.end())
540  {
541  bool found = false;
542  std::tie(it,found) =
543  result.insert(std::make_pair(obs,Observables()));
544 
545  }
546  it->second.insert(eventId);
547  }
548  });
549  }
550  }
551  return result;
552  }
553 
554  // je le fais sans template pour le moment mais il faudra generaliser
555  bool explain(const DdAutFA & fsa,
556  const DdAutStateManager & sManager,
557  const DdAutEventManager & eManager,
558  const std::vector<std::string> & observations,
559  Observables & observables,
560  DdAutFA & explanations,
561  DdAutFA & fullExplanations,
562  DdAutStateManager & sManagerExplanation,
563  std::unordered_map<DdAutFA::State, unordered_set<DdAutFA::Transition> > & safeAlternatives)
564  {
565  bool result = true;
566  Matcher matcher = initialiseMatcher(eManager,observations);
567  LocStateMap levelOfChoiceMap;
568  levelOfChoice(fsa,levelOfChoiceMap);
569  explanations.setName(fsa.name()+"_explained");
570  fullExplanations.setName(fsa.name()+"_consistent_traces");
572  fsa.initialStateEnd(),
573  fsa,
574  sManager,
575  eManager,
576  observations,
577  observables,
578  explanations,
579  fullExplanations,
580  sManagerExplanation,
581  matcher,
582  levelOfChoiceMap,
583  safeAlternatives);
584  return result;
585  }
586 
587  }
588  }
589 }
590 
591 #endif /* __DIADES__AUTOMATA__EXPERIMENTAL__EXPLANATION__HH */
void extractEffectiveChoiceTransitions(Fsm &traces, const ExplLocStateMap &levelOfChoice, unordered_set< typename Fsm::Transition > &solutions)
Extraction from the traces of A || Pbar || L, the set of effective choice transitions.
Definition: Explanation.hh:253
Set of functions that trim states/transitions from StateMachines.
#define LP(...)
bool levelOfChoice(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, LocStateMap &result)
Definition: Explanation.hh:209
Diades::Graph::ConstNodeMap< Type > CstStMap
InfoIdIterator end() const
Definition: InfoManager.hh:428
Transition newTransition(State source, State target, const EventPropertyId &event)
Diades::Graph::Edge Transition
Definition: Component.hh:46
StatePropertyId statePropertyId(const StateProperty &stateProperty)
Diades::Graph::NodeMap< int > ExplLocStateMap
Definition: Explanation.hh:32
Matcher initialiseMatcher(const DdAutEventManager &eManager, const std::vector< std::string > &observations)
Definition: Explanation.hh:525
FaultyEventStateMachine< CandidateId, EventInfoId > Fsm
bool isNotChoiceState(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State state, const LocStateMap &levels)
return true if the state is definitely considered as a no-choice state
Definition: Explanation.hh:47
bool setLevel(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &states, int currentLevel, LocStateMap &levels)
Definition: Explanation.hh:132
Diades::Graph::ConstNodeMap< int > LocStateMap
Definition: Explanation.hh:30
std::unordered_set< DdAutFA::Transition > getSafeAlternatives(const DdAutFA &traces, DdAutFA::State state, const ExplLocStateMap &levelOfChoiceInTraces, const Diades::Graph::NodeMap< DdAutFA::State > &mapping, const DdAutFA &fsa, const LocStateMap &levelOfChoiceInFsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager)
Definition: Explanation.hh:344
InitialStateIterator initialStateEnd() const
StIndexes states
Definition: Run.cc:266
bool explainFromStates(StateIterator begin, StateIterator end, const DdAutFA &fsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager, const Observations &observations, Observables &observables, DdAutFA &explanations, DdAutFA &traces, DdAutStateManager &sManagerExplanation, const Matcher &matcher, const LocStateMap &levelOfChoice, SafeAlt< DdAutFA > &safeAlternatives)
Definition: Explanation.hh:382
bool explain(const DdAutFA &fsa, const DdAutStateManager &sManager, const DdAutEventManager &eManager, const std::vector< std::string > &observations, Observables &observables, DdAutFA &explanations, DdAutFA &fullExplanations, DdAutStateManager &sManagerExplanation, std::unordered_map< DdAutFA::State, unordered_set< DdAutFA::Transition > > &safeAlternatives)
Definition: Explanation.hh:555
InfoIdIterator begin() const
Definition: InfoManager.hh:418
InputEventTransitionIterator inputEventTransitionEnd(State s, const EventPropertyId &e) const
AutFsm::State State
Definition: Run.cc:72
AutFsm::Transition Transition
Definition: Run.cc:73
std::unordered_map< Observation, Observables > Matcher
Definition: Explanation.hh:239
const string & setName(const string &name)
const EventPropertyId & getEvent(Transition t) const
FiniteAutomaton< DdAutStateId, DdAutEventId > DdAutFA
Definition: DdAutFile.hh:47
std::pair< AcceptingStateIterator, bool > setAcceptingState(State state)
const Event & getEvent(EventId id) const
Definition: Event.hh:183
Namespace of the Diades project.
bool project(const Fsm &machine, Fsm &abstractMachine, IsGoal isGoal, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)
Definition: Project.hh:426
std::vector< Observation > Observations
Definition: Explanation.hh:237
InitialStateIterator initialStateBegin() const
std::set< DdAutFA::EventPropertyId > Observables
Definition: Explanation.hh:238
void setLevelStateAndPropagate(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &states, int currentLevel, LocStateMap &levels, typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State state, std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &tagged, std::unordered_set< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &visited)
set the level of the current state and insert its untagged predecessors in the list &#39;states&#39; update t...
Definition: Explanation.hh:96
Diades::Graph::Node State
Definition: BeliefState.hh:36
Diades::Graph::NodeMap< Type > StMap
InputEventTransitionIterator inputEventTransitionBegin(State s, const EventPropertyId &e) const
StMap< BsPtr< Fsm > > BsMap
Definition: BeliefState.hh:482
boost::format Msg
Definition: Verbose.hh:42
const StateProperty & getStateProperty(StatePropertyId id) const
std::unordered_map< typename Fsm::State, std::unordered_set< typename Fsm::Transition > > SafeAlt
Definition: Explanation.hh:377
State getState(const StatePropertyId &sProperty) const