implemented bounding of transitions:

if taking, for example, a transition <3,update> from a state s that only has an outgoing transition for <2,update> then we take that transition instead.

MOPBox/src/de/bodden/mopbox/finitestate/AbstractFSMMonitorTemplate.java

@@ -20,8 +20,8 @@
  */
 public abstract class AbstractFSMMonitorTemplate<L,K,V> extends AbstractMonitorTemplate<DefaultFSMMonitor<L>,L,K,V> {
 
-	private int nextStateNum = 0;
-	private State<L> initialState;	
+	protected int nextStateNum = 0;
+	protected State<L> initialState;	
 
 	protected State<L> makeState(boolean isFinal) {
 		return new State<L>(getAlphabet(),isFinal,Integer.toString(nextStateNum++));

MOPBox/src/de/bodden/mopbox/finitestate/sync/AbstractSyncingFSMMonitorTemplate.java

@@ -442,6 +442,40 @@ public SyncFSMMonitor createMonitorPrototype() {
 	public IVariableBinding<K, V> createEmptyBinding() {
 		return delegate.createEmptyBinding();
 	}
+
+	@Override
+	protected State<AbstractionAndSymbol> makeState(boolean isFinal) {
+		return new SyncState(getAlphabet(),isFinal,Integer.toString(nextStateNum++));
+	}
+
+	public class SyncState extends State<AbstractionAndSymbol> {
+
+		Map<ISymbol<L, K>,A> symToMaxAbstraction = new HashMap<ISymbol<L, K>,A>();
+		Map<ISymbol<L, K>,ISymbol<AbstractionAndSymbol, ?>> symToMaxSymbol = new HashMap<ISymbol<L, K>,ISymbol<AbstractionAndSymbol, ?>>();
+
+		public SyncState(IAlphabet<AbstractionAndSymbol, ?> alphabet, boolean isFinal, String label) {
+			super(alphabet, isFinal, label);
+		}
+
+		@Override
+		public State<AbstractionAndSymbol> successor(ISymbol<AbstractionAndSymbol, ?> sym) {
+			A max = symToMaxAbstraction.get(sym.getLabel().getSymbol());
+			if(max!=null && max.isSmallerOrEqualThan(sym.getLabel().getAbstraction())) {
+				sym = symToMaxSymbol.get(sym.getLabel().getSymbol());
+			}
+			return super.successor(sym);
+		}
+
+		@Override
+		public void addTransition(ISymbol<AbstractionAndSymbol, ?> sym, State<AbstractionAndSymbol> succ) {
+			super.addTransition(sym, succ);
+			A abstraction = sym.getLabel().getAbstraction();
+			ISymbol<L, K> symbol = sym.getLabel().getSymbol();
+			symToMaxAbstraction.put(symbol,abstraction);
+			symToMaxSymbol.put(symbol,getAlphabet().getSymbolByLabel(new AbstractionAndSymbol(abstraction, sym.getLabel().getSymbol())));
+		}
+
+	}
 
 	public class SyncFSMMonitor extends DefaultFSMMonitor<AbstractionAndSymbol> {
 
@@ -462,7 +496,7 @@ public boolean processEvent(ISymbol<AbstractionAndSymbol, ?> s) {
 			} else {
 				lastAccess = reenableTime;
 			}
-
+						
 			return super.processEvent(s);
 		}
 	}
@@ -473,6 +507,8 @@ public abstract class SymbolMultisetAbstraction {
 		public abstract boolean equals(Object obj);		
 
 		protected abstract A add(ISymbol<L, K> sym);
+
+		protected abstract boolean isSmallerOrEqualThan(A other);
 	}
 
 }

MOPBox/src/de/bodden/mopbox/finitestate/sync/FullSyncingTemplate.java

@@ -63,6 +63,11 @@ protected FullAbstraction add(ISymbol<L, K> sym) {
 			return new FullAbstraction(true);
 		}
 
+		@Override
+		protected boolean isSmallerOrEqualThan(FullAbstraction other) {
+			return !skippedSomething;
+		}
+
 	}
 
 }

MOPBox/src/de/bodden/mopbox/finitestate/sync/MultisetSyncingTemplate.java

@@ -71,5 +71,9 @@ protected AbstractionAsMultiset add(ISymbol<L, K> sym) {
 			copy.add(sym);
 			return new AbstractionAsMultiset(copy);
 		}
+
+		protected boolean isSmallerOrEqualThan(AbstractionAsMultiset other) {
+			return other.symbols.containsAll(symbols);
+		}
 	}	
 }

MOPBox/src/de/bodden/mopbox/finitestate/sync/NumberAndSymbolSetSyncingTemplate.java

@@ -75,5 +75,10 @@ protected AbstractionBySizeAndSymbols add(ISymbol<L, K> sym) {
 			copy.add(sym);
 			return new AbstractionBySizeAndSymbols(size+1, copy);
 		}
+
+		@Override
+		protected boolean isSmallerOrEqualThan(AbstractionBySizeAndSymbols other) {
+			return other.symbols.containsAll(symbols) && other.size>=size;
+		}
 	}	
 }

MOPBox/src/de/bodden/mopbox/finitestate/sync/NumberSyncingTemplate.java

@@ -61,6 +61,11 @@ public boolean equals(Object obj) {
 		protected AbstractionBySize add(ISymbol<L, K> sym) {
 			return new AbstractionBySize(size+1);
 		}
+
+		@Override
+		protected boolean isSmallerOrEqualThan(AbstractionBySize other) {
+			return other.size>=size;
+		}
 
 	}
 

MOPBox/src/de/bodden/mopbox/finitestate/sync/SymbolSetSyncingTemplate.java

@@ -69,5 +69,10 @@ protected AbstractionBySymbolSet add(ISymbol<L, K> sym) {
 			copy.add(sym);
 			return new AbstractionBySymbolSet(copy);
 		}
+
+		@Override
+		protected boolean isSmallerOrEqualThan(AbstractionBySymbolSet other) {
+			return other.symbols.containsAll(symbols);
+		}
 	}	
 }