add test case revealing non-determinacy issue

src/test/java/de/learnlib/ralib/example/array/ArrayListDataWordOracle.java

@@ -0,0 +1,62 @@
+package de.learnlib.ralib.example.array;
+
+import java.util.ArrayList;
+import java.util.Collection;
+
+import de.learnlib.query.Query;
+import de.learnlib.ralib.oracles.DataWordOracle;
+import de.learnlib.ralib.words.InputSymbol;
+import de.learnlib.ralib.words.PSymbolInstance;
+import net.automatalib.word.Word;
+
+public abstract class ArrayListDataWordOracle<T> implements DataWordOracle {
+
+	public static int DEFAULT_CAPACITY = 3;
+
+	private final InputSymbol PUSH = pushSymbol();
+	private final InputSymbol REMOVE = removeSymbol();
+
+	private int capacity;
+
+	public ArrayListDataWordOracle() {
+		this(DEFAULT_CAPACITY);
+	}
+
+	public ArrayListDataWordOracle(int capacity) {
+		this.capacity = capacity;
+	}
+
+	@Override
+	public void processQueries(Collection<? extends Query<PSymbolInstance, Boolean>> queries) {
+		for (Query<PSymbolInstance, Boolean> query : queries) {
+			query.answer(answer(query.getInput()));
+		}
+	}
+
+	private boolean answer(Word<PSymbolInstance> word) {
+		ArrayList<T> arr = new ArrayList<>();
+		try {
+			for(PSymbolInstance psi : word) {
+				if (!accepts(psi, arr)) {
+					return false;
+				}
+			}
+		} catch(Exception ex) {
+			return false;
+		}
+		return true;
+	}
+
+	private boolean accepts(PSymbolInstance psi, ArrayList<T> arr) {
+		if (psi.getBaseSymbol().equals(PUSH) && arr.size() < capacity) {
+			arr.add((T)psi.getParameterValues()[0].getId());
+			return true;
+		} else if (psi.getBaseSymbol().equals(REMOVE)) {
+			return arr.remove(psi.getParameterValues()[0].getId());
+		}
+		return false;
+	}
+
+	protected abstract InputSymbol pushSymbol();
+	protected abstract InputSymbol removeSymbol();
+}

src/test/java/de/learnlib/ralib/example/array/DoubleArrayListDataWordOracle.java

@@ -0,0 +1,29 @@
+package de.learnlib.ralib.example.array;
+
+import java.math.BigDecimal;
+
+import de.learnlib.ralib.data.DataType;
+import de.learnlib.ralib.words.InputSymbol;
+
+public class DoubleArrayListDataWordOracle extends ArrayListDataWordOracle<BigDecimal> {
+
+	public static final DataType DOUBLE_TYPE = new DataType("double", BigDecimal.class);
+
+	public static final InputSymbol PUSH = new InputSymbol("push", new DataType[] {DOUBLE_TYPE});
+	public static final InputSymbol REMOVE = new InputSymbol("remove", new DataType[] {DOUBLE_TYPE});
+
+	public DoubleArrayListDataWordOracle(int capacity) {
+		super(capacity);
+	}
+
+	@Override
+	protected InputSymbol pushSymbol() {
+		return PUSH;
+	}
+
+	@Override
+	protected InputSymbol removeSymbol() {
+		return REMOVE;
+	}
+
+}

src/test/java/de/learnlib/ralib/learning/ralambda/LearnBoundedListIneqTest.java

@@ -0,0 +1,89 @@
+package de.learnlib.ralib.learning.ralambda;
+
+import static de.learnlib.ralib.example.array.DoubleArrayListDataWordOracle.DOUBLE_TYPE;
+import static de.learnlib.ralib.example.array.DoubleArrayListDataWordOracle.PUSH;
+import static de.learnlib.ralib.example.array.DoubleArrayListDataWordOracle.REMOVE;
+
+import java.math.BigDecimal;
+import java.util.LinkedHashMap;
+import java.util.Map;
+
+import org.testng.Assert;
+import org.testng.annotations.Test;
+
+import de.learnlib.query.DefaultQuery;
+import de.learnlib.ralib.RaLibTestSuite;
+import de.learnlib.ralib.automata.RegisterAutomaton;
+import de.learnlib.ralib.data.Constants;
+import de.learnlib.ralib.data.DataType;
+import de.learnlib.ralib.data.DataValue;
+import de.learnlib.ralib.example.array.DoubleArrayListDataWordOracle;
+import de.learnlib.ralib.learning.Hypothesis;
+import de.learnlib.ralib.oracles.SDTLogicOracle;
+import de.learnlib.ralib.oracles.SimulatorOracle;
+import de.learnlib.ralib.oracles.TreeOracleFactory;
+import de.learnlib.ralib.oracles.mto.MultiTheorySDTLogicOracle;
+import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle;
+import de.learnlib.ralib.solver.ConstraintSolver;
+import de.learnlib.ralib.solver.ConstraintSolverFactory;
+import de.learnlib.ralib.theory.Theory;
+import de.learnlib.ralib.tools.theories.DoubleInequalityTheory;
+import de.learnlib.ralib.words.PSymbolInstance;
+import net.automatalib.word.Word;
+
+public class LearnBoundedListIneqTest extends RaLibTestSuite {
+
+	@Test
+	public void learnArrayListTest() {
+
+		Constants consts = new Constants();
+
+		DoubleArrayListDataWordOracle dwOracle = new DoubleArrayListDataWordOracle(2);
+
+		final Map<DataType, Theory> teachers = new LinkedHashMap<>();
+		DoubleInequalityTheory dit = new DoubleInequalityTheory(DOUBLE_TYPE);
+		teachers.put(DOUBLE_TYPE, dit);
+        ConstraintSolver solver = ConstraintSolverFactory.createZ3ConstraintSolver();
+        MultiTheoryTreeOracle mto = new MultiTheoryTreeOracle(dwOracle, teachers, consts, solver);
+
+        SDTLogicOracle mlo = new MultiTheorySDTLogicOracle(consts, solver);
+
+        TreeOracleFactory hypFactory = (RegisterAutomaton hyp) ->
+                new MultiTheoryTreeOracle(new SimulatorOracle(hyp), teachers, consts, solver);
+
+        RaLambda learner = new RaLambda(mto, hypFactory, mlo, consts, PUSH, REMOVE);
+        learner.learn();
+
+        DataValue<BigDecimal> dv1 = new DataValue<>(DOUBLE_TYPE, BigDecimal.ONE);
+        DataValue<BigDecimal> dv2 = new DataValue<>(DOUBLE_TYPE, BigDecimal.valueOf(2));
+        DataValue<BigDecimal> dv3 = new DataValue<>(DOUBLE_TYPE, BigDecimal.valueOf(3));
+
+        PSymbolInstance push1 = new PSymbolInstance(PUSH, dv1);
+        PSymbolInstance push2 = new PSymbolInstance(PUSH, dv2);
+        PSymbolInstance push3 = new PSymbolInstance(PUSH, dv3);
+        PSymbolInstance rem1 = new PSymbolInstance(REMOVE, dv1);
+        PSymbolInstance rem2 = new PSymbolInstance(REMOVE, dv2);
+
+        Word<PSymbolInstance> ce = Word.fromSymbols(push1, push2, push3);
+
+        learner.addCounterexample(new DefaultQuery<>(ce, false));
+        learner.learn();
+
+        ce = Word.fromSymbols(push1, rem1);
+        learner.addCounterexample(new DefaultQuery<>(ce, true));
+        learner.learn();
+
+        ce = Word.fromSymbols(push1, push2, rem1);
+        learner.addCounterexample(new DefaultQuery<>(ce, true));
+        learner.learn();
+
+        ce = Word.fromSymbols(push2, push1, rem2);
+        learner.addCounterexample(new DefaultQuery<>(ce, true));
+        learner.learn();
+
+        Hypothesis hyp = learner.getHypothesis();
+
+        Assert.assertEquals(hyp.getStates().size(), 5);
+        Assert.assertEquals(hyp.getTransitions().size(), 18);
+	}
+}