Skip to content

Commit

Permalink
correction
Browse files Browse the repository at this point in the history
  • Loading branch information
eric.bodden committed Sep 19, 2012
1 parent 0707366 commit fedc54a
Showing 1 changed file with 8 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ protected State<AbstractionAndSymbol> setupStatesAndTransitions() {
symSuccs.add(succ);
}
if(!symSuccs.isEmpty()) {
boolean subsumed = isSubsumedBySmallerAbstraction(currentStates,abstraction,sym,symSuccs);
boolean subsumed = transitionForSymbolAlreadyExists(currentStates,sym,symSuccs);

//create label for new transition: (abstraction,sym)
ISymbol<AbstractionAndSymbol, K> compoundSymbol = getSymbolByLabel(new AbstractionAndSymbol(abstraction, sym));
Expand Down Expand Up @@ -249,14 +249,16 @@ protected IAlphabet<AbstractSyncingFSMMonitorTemplate<L,K,V,A>.AbstractionAndSym
return new DynamicAlphabet<AbstractSyncingFSMMonitorTemplate<L,K,V,A>.AbstractionAndSymbol, K>();
}

private boolean isSubsumedBySmallerAbstraction(Set<State<L>> currentStates, A abstraction, ISymbol<L, K> symbol, Set<State<L>> symSuccs) {
private boolean transitionForSymbolAlreadyExists(Set<State<L>> currentStates, ISymbol<L, K> symbol, Set<State<L>> symSuccs) {
Map<ISymbol<AbstractionAndSymbol, K>, Set<State<L>>> symbolToTargets = transitions.get(currentStates);
if(symbolToTargets==null) return false;
for(Map.Entry<ISymbol<AbstractionAndSymbol, K>, Set<State<L>>> symbolAndTargets: symbolToTargets.entrySet()) {
// ISymbol<AbstractionAndSymbol, K> sym = symbolAndTargets.getKey();
Set<State<L>> targets = symbolAndTargets.getValue();
if(targets.equals(symSuccs)) { //TODO check that abstraction is actually smaller
return true;
ISymbol<AbstractionAndSymbol, K> sym = symbolAndTargets.getKey();
if(sym.getLabel().getSymbol().equals(symbol)) {
Set<State<L>> targets = symbolAndTargets.getValue();
if(targets.equals(symSuccs)) {
return true;
}
}
}
return false;
Expand Down

0 comments on commit fedc54a

Please sign in to comment.