Complete overhaul of Inequality Theory

src/main/java/de/learnlib/ralib/automata/guards/AtomicGuardExpression.java

@@ -61,6 +61,8 @@ public boolean isSatisfied(Mapping<SymbolicDataValue, DataValue<?>> val) {
                 return !lv.equals(rv);
             case BIGGER:
             case SMALLER:
+            case BIGGER_OR_EQUAL:
+            case SMALLER_OR_EQUAL:
                 return numCompare(lv, rv, relation);
 
             default:
@@ -116,8 +118,12 @@ private boolean numCompare(DataValue l, DataValue r, Relation relation) {
         switch (relation) {
             case SMALLER:
                 return result < 0;
+            case SMALLER_OR_EQUAL:
+            	return result < 0 || result == 0;
             case BIGGER:
                 return result > 0;
+            case BIGGER_OR_EQUAL:
+            	return result > 0 || result == 0;
 
             default:
                 throw new UnsupportedOperationException(

src/main/java/de/learnlib/ralib/automata/guards/Relation.java

@@ -19,7 +19,9 @@
 public enum Relation {
 
     SMALLER("<"),
+    SMALLER_OR_EQUAL("<="),
     BIGGER(">"),
+    BIGGER_OR_EQUAL(">="),
     EQUALS("=="),
     NOT_EQUALS("!=");
 

src/main/java/de/learnlib/ralib/automata/xml/ExpressionParser.java

@@ -96,10 +96,18 @@ else if (pred.contains("!!")) {
             related = pred.split("!!");
             relation = Relation.NOT_EQUALS;
         }
+        else if (pred.contains("<=")) {
+        	related = pred.split("<=");
+        	relation = Relation.SMALLER_OR_EQUAL;
+        }
         else if (pred.contains("<")) {
             related = pred.split("<");
             relation = Relation.SMALLER;
         }
+        else if (pred.contains(">=")) {
+        	related = pred.split(">=");
+        	relation = Relation.BIGGER_OR_EQUAL;
+        }
         else if (pred.contains(">")) {
             related = pred.split(">");
             relation = Relation.BIGGER;

src/main/java/de/learnlib/ralib/ceanalysis/PrefixFinder.java

@@ -30,6 +30,8 @@
 import de.learnlib.ralib.oracles.SDTLogicOracle;
 import de.learnlib.ralib.oracles.TreeOracle;
 import de.learnlib.ralib.oracles.TreeQueryResult;
+import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle;
+import de.learnlib.ralib.oracles.mto.SymbolicSuffixRestrictionBuilder;
 import de.learnlib.ralib.words.DataWords;
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
@@ -45,6 +47,7 @@ public class PrefixFinder {
 
     private final SDTLogicOracle sdtOracle;
 
+    private final SymbolicSuffixRestrictionBuilder restrictionBuilder;
     //private Map<Word<PSymbolInstance>, LocationComponent> components;
 
     private final Constants consts;
@@ -67,6 +70,11 @@ public PrefixFinder(TreeOracle sulOracle, TreeOracle hypOracle,
         this.sdtOracle = sdtOracle;
         //this.components = components;
         this.consts = consts;
+        if (sulOracle instanceof MultiTheoryTreeOracle) {
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts, ((MultiTheoryTreeOracle)sulOracle).getTeachers());
+        } else {
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts);
+        }
     }
 
     public CEAnalysisResult analyzeCounterexample(Word<PSymbolInstance> ce) {
@@ -102,7 +110,7 @@ private int findIndex(Word<PSymbolInstance> ce) {
 			// check for location counterexample ...
 			//
 			Word<PSymbolInstance> suffix = ce.suffix(ce.length() - nextPrefix.length());
-			SymbolicSuffix symSuffix = new SymbolicSuffix(nextPrefix, suffix, consts);
+			SymbolicSuffix symSuffix = new SymbolicSuffix(nextPrefix, suffix, restrictionBuilder);
 			LOC_CHECK: for (Word<PSymbolInstance> u : hypothesis.possibleAccessSequences(prefix)) {
 				Word<PSymbolInstance> uAlpha = hypothesis.transformTransitionSequence(nextPrefix, u);
 				TreeQueryResult uAlphaResult = sulOracle.treeQuery(uAlpha, symSuffix);
@@ -179,7 +187,7 @@ private boolean transitionHasCE(Word<PSymbolInstance> ce, int idx) {
     	Word<PSymbolInstance> prefix = ce.prefix(idx+1);
 
     	Word<PSymbolInstance> suffix = ce.suffix(ce.length() - (idx+1));
-    	SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, consts);
+    	SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, restrictionBuilder);
 
     	Set<Word<PSymbolInstance>> locations = hypothesis.possibleAccessSequences(prefix);
     	for (Word<PSymbolInstance> location : locations) {
@@ -217,7 +225,7 @@ private void storeCandidateCEs(Word<PSymbolInstance> ce, int idx) {
     	Word<PSymbolInstance> prefix = ce.prefix(idx+1);
 
     	Word<PSymbolInstance> suffix = ce.suffix(ce.length() - (idx+1));
-    	SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, consts);
+    	SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, restrictionBuilder);
 
     	Set<Word<PSymbolInstance>> locations = hypothesis.possibleAccessSequences(prefix);
     	for (Word<PSymbolInstance> location : locations) {
@@ -264,7 +272,7 @@ private SymbolicWord candidate(Word<PSymbolInstance> prefix,
 
         	if (exprR.isSatisfied(vals)) {
         		candidate = path.prefix(prefix.length() + 1);
-        		SymbolicSuffix suffix = new SymbolicSuffix(candidate, ce.suffix(symSuffix.length() - 1), consts);
+        		SymbolicSuffix suffix = new SymbolicSuffix(candidate, ce.suffix(symSuffix.length() - 1), restrictionBuilder);
         		return new SymbolicWord(candidate, suffix);
         	}
         }

src/main/java/de/learnlib/ralib/dt/DT.java

@@ -25,9 +25,11 @@
 import de.learnlib.ralib.learning.ralambda.RaLambda;
 import de.learnlib.ralib.oracles.TreeOracle;
 import de.learnlib.ralib.oracles.TreeQueryResult;
+import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle;
 import de.learnlib.ralib.oracles.mto.OptimizedSymbolicSuffixBuilder;
 import de.learnlib.ralib.oracles.mto.SDT;
 import de.learnlib.ralib.oracles.mto.SDTLeaf;
+import de.learnlib.ralib.oracles.mto.SymbolicSuffixRestrictionBuilder;
 import de.learnlib.ralib.theory.SDTGuard;
 import de.learnlib.ralib.theory.SDTTrueGuard;
 import de.learnlib.ralib.words.OutputSymbol;
@@ -48,12 +50,17 @@ public class DT implements DiscriminationTree {
     private boolean ioMode;
     private final Constants consts;
     private DTLeaf sink = null;
+    private final SymbolicSuffixRestrictionBuilder restrictionBuilder;
 
     public DT(TreeOracle oracle, boolean ioMode, Constants consts, ParameterizedSymbol... inputs) {
         this.oracle = oracle;
         this.ioMode = ioMode;
         this.inputs = inputs;
         this.consts = consts;
+        if (oracle instanceof MultiTheoryTreeOracle)
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts, ((MultiTheoryTreeOracle)oracle).getTeachers());
+        else
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts);
 
         Word<PSymbolInstance> epsilon = Word.epsilon();
         SymbolicSuffix suffEps = new SymbolicSuffix(epsilon, epsilon);
@@ -67,13 +74,18 @@ public DT(DTInnerNode root, TreeOracle oracle, boolean ioMode, Constants consts,
         this.ioMode = ioMode;
         this.inputs = inputs;
         this.consts = consts;
+        if (oracle instanceof MultiTheoryTreeOracle)
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts, ((MultiTheoryTreeOracle)oracle).getTeachers());
+        else
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts);
     }
 
     public DT(DT dt) {
         this.inputs = dt.inputs;
         this.oracle = dt.oracle;
         this.ioMode = dt.ioMode;
         this.consts = dt.consts;
+        this.restrictionBuilder = dt.restrictionBuilder;
 
         root = new DTInnerNode(dt.root);
     }
@@ -247,7 +259,7 @@ public void addSuffix(SymbolicSuffix suffix, DTLeaf leaf) {
     public boolean addLocation(Word<PSymbolInstance> target, DTLeaf src_c, DTLeaf dest_c, DTLeaf target_c) {
 
         Word<PSymbolInstance> prefix = target.prefix(target.length() - 1);
-        SymbolicSuffix suff1 = new SymbolicSuffix(prefix, target.suffix(1), consts);
+        SymbolicSuffix suff1 = new SymbolicSuffix(prefix, target.suffix(1), restrictionBuilder);
         SymbolicSuffix suff2 = findLCA(dest_c, target_c).getSuffix();
         SymbolicSuffix suffix = suff1.concat(suff2);
 

src/main/java/de/learnlib/ralib/dt/DTLeaf.java

@@ -487,8 +487,10 @@ private boolean checkVariableConsistency(MappedPrefix mp, DT dt, Constants const
             	for (SymbolicSuffix suffix : suffixes) {
             		TreeQueryResult suffixTQR = mp.getTQRs().get(suffix);
             		SymbolicDecisionTree sdt = suffixTQR.getSdt();
+            		// suffixBuilder == null ==> suffix.isOptimizedGeneric()
+            		assert suffixBuilder != null || suffix.isOptimizationGeneric() : "Optimized with restriction builder, but no restriction builder provided";
             		SymbolicSuffix newSuffix = suffixBuilder != null && sdt instanceof SDT ?
-            				suffixBuilder.extendSuffix(mp.getPrefix(), (SDT)sdt, suffixTQR.getPiv(), suffix) :
+            				suffixBuilder.extendSuffix(mp.getPrefix(), (SDT)sdt, suffixTQR.getPiv(), suffix, suffixTQR.getPiv().get(p)) :
             				new SymbolicSuffix(mp.getPrefix(), suffix, consts);
             		if (prefixSuffixes.contains(newSuffix))
             			continue;

src/main/java/de/learnlib/ralib/learning/CounterexampleAnalysis.java

@@ -30,6 +30,8 @@
 import de.learnlib.ralib.oracles.SDTLogicOracle;
 import de.learnlib.ralib.oracles.TreeOracle;
 import de.learnlib.ralib.oracles.TreeQueryResult;
+import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle;
+import de.learnlib.ralib.oracles.mto.SymbolicSuffixRestrictionBuilder;
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
 import net.automatalib.word.Word;
@@ -50,6 +52,8 @@ public class CounterexampleAnalysis {
 
     private final SDTLogicOracle sdtOracle;
 
+    private final SymbolicSuffixRestrictionBuilder restrictionBuilder;
+
     private final Map<Word<PSymbolInstance>, LocationComponent> components;
 
     private final Constants consts;
@@ -68,6 +72,11 @@ public CounterexampleAnalysis(TreeOracle sulOracle, TreeOracle hypOracle,
         this.sdtOracle = sdtOracle;
         this.components = components;
         this.consts = consts;
+        if (sulOracle instanceof MultiTheoryTreeOracle) {
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts, ((MultiTheoryTreeOracle)sulOracle).getTeachers());
+        } else {
+        	this.restrictionBuilder = new SymbolicSuffixRestrictionBuilder(consts);
+        }
     }
 
     public CEAnalysisResult analyzeCounterexample(Word<PSymbolInstance> ce) {
@@ -77,7 +86,7 @@ public CEAnalysisResult analyzeCounterexample(Word<PSymbolInstance> ce) {
 
         Word<PSymbolInstance> prefix = ce.prefix(idx);
         Word<PSymbolInstance> suffix = ce.suffix(ce.length() -idx);
-        SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, consts);
+        SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, restrictionBuilder);
 
         return new CEAnalysisResult(prefix, symSuffix);
     }
@@ -91,7 +100,7 @@ private IndexResult computeIndex(Word<PSymbolInstance> ce, int idx) {
             ce.prefix(idx+1));
 
         Word<PSymbolInstance> suffix = ce.suffix(ce.length() -idx);
-        SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, consts);
+        SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, restrictionBuilder);
 
         TreeQueryResult resHyp = hypOracle.treeQuery(location, symSuffix);
         TreeQueryResult resSul = sulOracle.treeQuery(location, symSuffix);

src/main/java/de/learnlib/ralib/learning/MeasuringOracle.java

@@ -2,23 +2,32 @@
 
 import java.util.Map;
 
+import de.learnlib.ralib.data.Constants;
+import de.learnlib.ralib.data.DataType;
 import de.learnlib.ralib.data.PIV;
 import de.learnlib.ralib.oracles.Branching;
-import de.learnlib.ralib.oracles.TreeOracle;
+import de.learnlib.ralib.oracles.DataWordOracle;
 import de.learnlib.ralib.oracles.TreeQueryResult;
+import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle;
+import de.learnlib.ralib.solver.ConstraintSolver;
+import de.learnlib.ralib.theory.Theory;
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
 import net.automatalib.word.Word;
 
-public class MeasuringOracle implements TreeOracle {
-
-	private final TreeOracle oracle;
+public class MeasuringOracle extends MultiTheoryTreeOracle {
 
 	private final Measurements result;
 
-	public MeasuringOracle(TreeOracle oracle, Measurements m) {
-		this.oracle = oracle;
-		this.result = m;
+	public MeasuringOracle(DataWordOracle oracle, Map<DataType, Theory> teachers, Constants constants,
+            ConstraintSolver solver, Measurements m) {
+		super(oracle, teachers, constants, solver);
+		result = m;
+	}
+
+	public MeasuringOracle(MultiTheoryTreeOracle mto, Measurements m) {
+		super(mto);
+		result = m;
 	}
 
 	@Override
@@ -29,24 +38,24 @@ public TreeQueryResult treeQuery(Word<PSymbolInstance> prefix, SymbolicSuffix su
 			result.treeQueryWords.put(key, result.treeQueryWords.get(key) + 1);
 		else
 			result.treeQueryWords.put(key, 1);
-		return oracle.treeQuery(prefix, suffix);
+		return super.treeQuery(prefix, suffix);
 	}
 
 	@Override
 	public Branching getInitialBranching(Word<PSymbolInstance> prefix, ParameterizedSymbol ps, PIV piv,
 			SymbolicDecisionTree... sdts) {
-		return oracle.getInitialBranching(prefix, ps, piv, sdts);
+		return super.getInitialBranching(prefix, ps, piv, sdts);
 	}
 
 	@Override
 	public Branching updateBranching(Word<PSymbolInstance> prefix, ParameterizedSymbol ps, Branching current, PIV piv,
 			SymbolicDecisionTree... sdts) {
-		return oracle.updateBranching(prefix, ps, current, piv, sdts);
+		return super.updateBranching(prefix, ps, current, piv, sdts);
 	}
 
 	@Override
 	public Map<Word<PSymbolInstance>, Boolean> instantiate(Word<PSymbolInstance> prefix, SymbolicSuffix suffix,
 			SymbolicDecisionTree sdt, PIV piv) {
-		return oracle.instantiate(prefix, suffix, sdt, piv);
+		return super.instantiate(prefix, suffix, sdt, piv);
 	}
 }