9 #ifndef __DIADES__AUTOMATA__EXPERIMENTAL__EXPLANATION__HH 10 #define __DIADES__AUTOMATA__EXPERIMENTAL__EXPLANATION__HH 12 #include<unordered_map> 13 #include<unordered_set> 28 namespace Experimental {
46 template<
typename _SPId,
typename _ISId,
typename _NSPId = NullValue<_SPId>,
typename _NISId = NullValue< _ISId>>
56 result = (levels[it->target()] != -1);
61 commonLevel = levels[it->target()];
63 result = (commonLevel == levels[it->target()]);
67 LP(
Msg(
"\\item The state %1% is %2% considered as a no-choice state.\n")
69 % (result?
"definitely":
"not yet"));
92 template<
typename _SPId,
106 levels[state] = currentLevel;
107 tagged.insert(state);
108 visited.insert(state);
115 if((levels[t.source()]== -1) && (visited.find(t.source()) == visited.end()))
117 LP(
Msg(
"\\item State %1% is a non-visited predecessor of State %2% and is inserted.\n")
121 visited.insert(t.source());
128 template<
typename _SPId,
137 bool result = !
states.empty();
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;
149 std::unordered_set<State> tagged;
150 std::unordered_set<State> visited;
152 auto last = --
states.end();
168 ListStatesIterator firstPostponedStateIt =
states.end();
171 while(firstPostponedStateIt !=
states.begin())
173 if(levels[
states.front()]==-1)
180 firstPostponedStateIt =
states.end();
185 if(firstPostponedStateIt ==
states.end())
205 template<
typename _SPId,
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())
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");
239 using Matcher = std::unordered_map<Observation,Observables>;
252 template<
typename Fsm>
254 unordered_set<typename Fsm::Transition> & solutions)
261 stack<Transition> visitingTransitions;
266 MinMaxPathEdgeMap minMaxPath(traces.behaviour(),
267 traces.numberOfTransitions(),
268 std::make_pair(-1,
false));
279 std::for_each(traces.acceptingStateBegin(),
280 traces.acceptingStateEnd(),
282 std::for_each(traces.inputTransitionBegin(s), traces.inputTransitionEnd(s),
285 minMaxPath[t] = std::make_pair(levelOfChoice[t.target()],
true);
286 visitingTransitions.push(t);
292 while(!visitingTransitions.empty())
294 auto currentTransition = visitingTransitions.top();
295 if(levelOfChoice[currentTransition.source()] > minMaxPath[currentTransition].first)
297 solutions.insert(currentTransition);
301 solutions.erase(currentTransition);
303 visitingTransitions.pop();
304 minMaxPath[currentTransition].second =
false;
308 auto currentState = currentTransition.source();
309 std::for_each(traces.inputTransitionBegin(currentState),
310 traces.inputTransitionEnd(currentState),
312 bool mustBeVisited =
false;
313 if(minMaxPath[t].first == -1)
315 minMaxPath[t].first = std::max(levelOfChoice[t.target()],minMaxPath[currentTransition].first);
316 mustBeVisited =
true;
320 int locPathMax = std::max(levelOfChoice[t.target()],minMaxPath[currentTransition].first);
321 if(minMaxPath[t].first > locPathMax)
323 minMaxPath[t].first = locPathMax;
324 mustBeVisited =
true;
331 if(!minMaxPath[t].second)
333 visitingTransitions.push(t);
334 minMaxPath[t].second =
true;
354 std::unordered_set<DdAutFA::Transition> result;
355 auto source = mapping[state];
360 auto targetLevel = levelOfChoiceInFsa[it->target()];
362 bool isGreater =
true;
365 isGreater = targetLevel > levelOfChoiceInTraces[it2->target()];
376 template<
typename Fsm>
377 using SafeAlt = std::unordered_map<typename Fsm::State, std::unordered_set<typename Fsm::Transition> >;
381 template<
typename StateIterator>
399 using TransList = std::list<Transition>;
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)
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(); },
416 std::inserter(transitions,transitions.begin()),
417 std::inserter(targetTransitions,targetTransitions.begin()));
419 for(
auto transition: transitions)
421 std::stringstream streamSource;
422 streamSource << levelOfChoice[transition.source()] <<
"_" 425 std::stringstream streamTarget;
426 streamTarget << levelOfChoice[transition.target()] <<
"_" 429 auto sourceId = sManagerExplanation.
statePropertyId(streamSource.str());
430 auto targetId = sManagerExplanation.
statePropertyId(streamTarget.str());
432 mapping[traces.
getState(sourceId)] = transition.source();
433 mapping[traces.
getState(targetId)] = transition.target();
445 levelOfChoiceInExplanation[traces.
getState(sourceId)] = levelOfChoice[transition.source()];
446 levelOfChoiceInExplanation[traces.
getState(targetId)] = levelOfChoice[transition.target()];
449 for(
auto transition: targetTransitions)
451 std::stringstream streamSource;
452 streamSource << levelOfChoice[transition.source()] <<
"_" 455 std::stringstream streamTarget;
456 streamTarget << levelOfChoice[transition.target()] <<
"_" 459 auto sourceId = sManagerExplanation.
statePropertyId(streamSource.str());
460 auto targetId = sManagerExplanation.
statePropertyId(streamTarget.str());
462 if(i == observations.size()-1)
466 levelOfChoiceInExplanation[traces.
getState(sourceId)] = levelOfChoice[transition.source()];
467 levelOfChoiceInExplanation[traces.
getState(targetId)] = levelOfChoice[transition.target()];
470 targetTransitions.clear();
473 std::unordered_set<Transition> effectiveChoiceTransitions;
475 effectiveChoiceTransitions);
480 bool result =
project(traces, explanations,
483 return effectiveChoiceTransitions.find(t) != effectiveChoiceTransitions.end();
489 std::for_each(effectiveChoiceTransitions.begin(),
490 effectiveChoiceTransitions.end(),
495 levelOfChoiceInExplanation,
499 auto effectiveTransitionTargetInExpl = stMap[t.target()];
504 auto trSourceInExpl = trans.source();
508 if(bsMap[trSourceInExpl]->findState(t.source())!= bsMap[trSourceInExpl]->end())
510 std::for_each(safeAlternativeTransitions.begin(),
511 safeAlternativeTransitions.end(),
514 safeAlternatives[trSourceInExpl].insert(safeTrans);
526 const std::vector<std::string> & observations)
529 for(
const auto & obs : observations)
531 if(result.find(obs) == result.end())
533 std::for_each(eManager.
begin(),eManager.
end(),
536 if(eManager.
getEvent(eventId).find(obs)!=DdAutEventManager::Event::npos)
538 Matcher::iterator it = result.find(obs);
546 it->second.insert(eventId);
558 const std::vector<std::string> & observations,
563 std::unordered_map<
DdAutFA::State, unordered_set<DdAutFA::Transition> > & safeAlternatives)
570 fullExplanations.
setName(fsa.
name()+
"_consistent_traces");
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.
Set of functions that trim states/transitions from StateMachines.
bool levelOfChoice(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, LocStateMap &result)
Diades::Graph::ConstNodeMap< Type > CstStMap
InfoIdIterator end() const
Transition newTransition(State source, State target, const EventPropertyId &event)
Diades::Graph::Edge Transition
StatePropertyId statePropertyId(const StateProperty &stateProperty)
Diades::Graph::NodeMap< int > ExplLocStateMap
typename IM::InfoId EventId
Matcher initialiseMatcher(const DdAutEventManager &eManager, const std::vector< std::string > &observations)
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
bool setLevel(const FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId > &fsa, std::list< typename FiniteAutomaton< _SPId, _ISId, _NSPId, _NISId >::State > &states, int currentLevel, LocStateMap &levels)
Diades::Graph::ConstNodeMap< int > LocStateMap
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)
OutputTransitionIterator outputTransitionBegin(State s) const
InitialStateIterator initialStateEnd() const
InputTransitionIterator inputTransitionBegin(State s) const
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)
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)
InfoIdIterator begin() const
InputEventTransitionIterator inputEventTransitionEnd(State s, const EventPropertyId &e) const
AutFsm::Transition Transition
std::unordered_map< Observation, Observables > Matcher
typename SM::Transition Transition
const string & setName(const string &name)
const EventPropertyId & getEvent(Transition t) const
FiniteAutomaton< DdAutStateId, DdAutEventId > DdAutFA
std::pair< AcceptingStateIterator, bool > setAcceptingState(State state)
const Event & getEvent(EventId id) const
Namespace of the Diades project.
OutputTransitionIterator outputTransitionEnd(State s) const
bool project(const Fsm &machine, Fsm &abstractMachine, IsGoal isGoal, BsMap< Fsm > &bsMap, CstStMap< typename Fsm::State > &stMap)
InputTransitionIterator inputTransitionEnd(State s) const
void setInitial(State state)
std::vector< Observation > Observations
Graph::Graph & behaviour()
InitialStateIterator initialStateBegin() const
std::set< DdAutFA::EventPropertyId > Observables
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 'states' update t...
Diades::Graph::Node State
Diades::Graph::NodeMap< Type > StMap
InputEventTransitionIterator inputEventTransitionBegin(State s, const EventPropertyId &e) const
StMap< BsPtr< Fsm > > BsMap
const StatePropertyId & getStatePropertyId(State state) const
const StateProperty & getStateProperty(StatePropertyId id) const
std::unordered_map< typename Fsm::State, std::unordered_set< typename Fsm::Transition > > SafeAlt
bool isInitial(State state) const
const string & name() const
State getState(const StatePropertyId &sProperty) const