diff --git a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java index f7e4e594..8b142b7f 100644 --- a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java +++ b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java @@ -335,7 +335,7 @@ public SDTGuard conjoin(SDTGuard guard1, SDTGuard guard2) { SDTGuard.SDTAndGuard andGuard = guard1 instanceof SDTGuard.SDTAndGuard sdtAndGuard ? sdtAndGuard : (SDTGuard.SDTAndGuard) guard2; SDTGuard otherGuard = guard2 instanceof SDTGuard.SDTAndGuard ? guard1 : guard2; - List conjuncts = andGuard.conjuncts(); + List conjuncts = new ArrayList(andGuard.conjuncts()); conjuncts.add(otherGuard); return new SDTGuard.SDTAndGuard(guard1.getParameter(), conjuncts); } diff --git a/src/test/java/de/learnlib/ralib/example/palindrome/Palindrome.java b/src/test/java/de/learnlib/ralib/example/palindrome/Palindrome.java new file mode 100644 index 00000000..138df94d --- /dev/null +++ b/src/test/java/de/learnlib/ralib/example/palindrome/Palindrome.java @@ -0,0 +1,46 @@ +package de.learnlib.ralib.example.palindrome; + +import java.util.ArrayList; +import java.util.List; + +public class Palindrome { + public static final int DEFAULT_MAX = 3; + + private final int max; + + private List vals; + + public Palindrome(int max) { + this.max = max; + vals = new ArrayList<>(); + } + + public Palindrome() { + this(DEFAULT_MAX); + } + + public void reset() { + vals.clear(); + } + + public boolean in(int d) { + vals.add(d); + if (vals.size() > max) { + return false; + } + return isPalindrome(); + } + + private boolean isPalindrome() { + int left = 0; + int right = vals.size() - 1; + while (left < right) { + if (!vals.get(left).equals(vals.get(right))) { + return false; + } + left++; + right--; + } + return true; + } +} diff --git a/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeGenerator.java b/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeGenerator.java new file mode 100644 index 00000000..d1bc7f0f --- /dev/null +++ b/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeGenerator.java @@ -0,0 +1,318 @@ +package de.learnlib.ralib.example.palindrome; + +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.IN; +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.TYPE; + +import java.math.BigDecimal; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Queue; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; + +import org.testng.Assert; +import org.testng.annotations.Test; + +import de.learnlib.ralib.automata.Assignment; +import de.learnlib.ralib.automata.MutableRegisterAutomaton; +import de.learnlib.ralib.automata.RALocation; +import de.learnlib.ralib.automata.RegisterAutomaton; +import de.learnlib.ralib.automata.Transition; +import de.learnlib.ralib.data.DataType; +import de.learnlib.ralib.data.DataValue; +import de.learnlib.ralib.data.SymbolicDataValue; +import de.learnlib.ralib.data.SymbolicDataValue.Parameter; +import de.learnlib.ralib.data.SymbolicDataValue.Register; +import de.learnlib.ralib.data.VarMapping; +import de.learnlib.ralib.data.util.SymbolicDataValueGenerator; +import de.learnlib.ralib.words.PSymbolInstance; +import de.learnlib.ralib.words.ParameterizedSymbol; +import gov.nasa.jpf.constraints.api.Expression; +import gov.nasa.jpf.constraints.expressions.NumericBooleanExpression; +import gov.nasa.jpf.constraints.expressions.NumericComparator; +import gov.nasa.jpf.constraints.util.ExpressionUtil; +import net.automatalib.word.WordBuilder; + +public class PalindromeGenerator { + + /** + * Returns a {@link RegisterAutomaton} of a language which accepts palindromes up to a length {code maxLen}. + * @param maxLen The maximum length of the palindromes + * @return the constructed RegisterAutomaton + */ + public static RegisterAutomaton generate(int maxLen) { + Node root = createPalindromeTree(maxLen); + RegisterAutomaton ra = convertToRA(root, IN); + return ra; + } + + /** + * Tree for compactly specifying accepting traces of a {@link RegisterAutomaton} with equality. + */ + public static class Node { + private Integer maxMemV; + private BiMap children; + private Node parent; + private boolean accept; + + public Node(Node parent, int maxMemV) { + this.parent = parent; + this.maxMemV = maxMemV; + this.children = HashBiMap.create(); + } + + public List getPrefix() { + Node parent = this.parent, child = this; + List prefix = new LinkedList(); + while (parent != null) { + Integer trans = parent.children.inverse().get(child); + prefix.addFirst(trans); + child = parent; + parent = parent.parent; + } + return prefix; + } + + public void setAccept(boolean accept) { + this.accept = accept; + } + + public Node createChildIfAbsent(Integer edge) { + Node child = children.get(edge); + if (child == null) { + child = new Node(this, maxMemV); + children.put(edge, child); + } + return child; + } + + public Integer determineMaxDownstreamEdge() { + Integer maxEdge = 0; + for (Entry entry : children.entrySet()) { + maxEdge = Math.max(maxEdge, entry.getValue().determineMaxDownstreamEdge()); + maxEdge = Math.max(maxEdge, entry.getKey()); + } + return maxEdge; + } + + private Integer determineMaxMemV () { + Integer futureMaxMemV = determineMaxDownstreamEdge(); + for (Entry entry : children.entrySet()) { + entry.getValue().determineMaxMemV(); + } + Integer pastMaxMemV = parent == null? 0 : Collections.max(this.getPrefix()); + maxMemV = Math.min(futureMaxMemV, pastMaxMemV); + return maxMemV; + } + + public Integer getMaxMemV() { + return maxMemV; + } + + public String toString() { + return toString(0, 2); + } + + public Map getChildren() { + return children; + } + + public boolean getAccept() { + return accept; + } + + public String toString(int indent, int indentIncrease) { + StringBuilder builder = new StringBuilder(); + builder.append(getPrefix()). + append(", maxMemV: ").append(maxMemV).append(", acc: ").append(accept).append("{").append(System.lineSeparator()); + for (Entry entry : children.entrySet()) { + builder.repeat(" ", indent).append(entry.getKey()).append(" -> ").append(entry.getValue() + .toString(indent + indentIncrease, indentIncrease)); + } + builder.append("}"); + return builder.toString(); + } + } + + + private static record WorkItem (Node node) {}; + + /** + * Creates a tree capturing encoding valid palindrome sequences up to a given length + * @param maxLen The maximum length of the palindromes + * @return the root of the constructed tree + */ + private static Node createPalindromeTree(int maxLen) { + Node root = new Node(null, 0); + Queue q = new ArrayDeque(); + q.add(new WorkItem(root)); + while (!q.isEmpty()) { + WorkItem i = q.poll(); + Node node = i.node; + List p = node.getPrefix(); + if (2*p.size() <= maxLen) { + Node last = node; + for (int idx = p.size()-1; idx>=0; idx--) { + last = last.createChildIfAbsent(p.get(idx)); + q.add(new WorkItem(last)); + } + last.setAccept(true); + if (2*p.size() + 1 <= maxLen) { + Integer maxVal = p.stream().max((i1, i2) -> i1.compareTo(i2)).orElse(0); + for (int middleVal = 1; middleVal <= maxVal+1; middleVal++) { + last = node.createChildIfAbsent(middleVal); + q.add(new WorkItem(last)); + for (int idx = p.size()-1; idx>=0; idx--) { + last = last.createChildIfAbsent(p.get(idx)); + q.add(new WorkItem(last)); + } + last.setAccept(true); + } + } + } + } + root.determineMaxMemV(); + return root; + } + + /** + * Converts a tree with root {@code root} into a corresponding {@link RegisterAutomaton} with alphabet containing only {@code in}. + * + * @param root root {@link Node} of the tree + * @param in the (only) symbol used in the constructed RegisterAutomaton + * @return the constructed RegisterAutomaton + */ + private static RegisterAutomaton convertToRA(Node root, ParameterizedSymbol in) { + MutableRegisterAutomaton ra = new MutableRegisterAutomaton(); + DataType type = in.getPtypes()[0]; + Queue q = new ArrayDeque(); + Map map = new HashMap<>(); + q.add(root); + map.put(root, ra.addState(root.getAccept())); + ra.setInitialState(map.get(root)); + RALocation sink = ra.addState(false); + while (!q.isEmpty()) { + Node srcNode = q.poll(); + RALocation srcLoc = map.get(srcNode); + + // create srcNode registers and parameter + SymbolicDataValueGenerator.RegisterGenerator srcRgen = new SymbolicDataValueGenerator.RegisterGenerator(); + Register [] srcRegs = new Register [srcNode.getMaxMemV()]; + for (int i=0; i eqRegs = new ArrayList<>(); + for (int edge=1; edge<=srcNode.getMaxMemV() + 1; edge++) { + Node destNode = srcNode.getChildren().get(edge); + if (destNode == null) { + continue; + } + RALocation destLoc = ra.addState(destNode.getAccept()); + map.put(destNode, destLoc); + + // create assignment + SymbolicDataValueGenerator.RegisterGenerator destRgen = new SymbolicDataValueGenerator.RegisterGenerator(); + VarMapping assignmentMapping = new VarMapping<>(); + for (int i=1; i<=srcNode.getMaxMemV(); i++) { + if (destNode.getMaxMemV() >= i) { + assignmentMapping.put(destRgen.next(type), srcRegs[i-1]); + } + } + if (destNode.getMaxMemV() > srcNode.getMaxMemV()) { + assignmentMapping.put(destRgen.next(type), param); + } + + // create guard + Expression guard = null; + if (edge <= srcNode.getMaxMemV()) { // equality case + guard = new NumericBooleanExpression(srcRegs[edge-1], NumericComparator.EQ, param); + // update list of registers over which we have equality + eqRegs.add(srcRegs[edge-1]); + } else { // fresh case + List> conjuncts = new ArrayList<>(srcRegs.length); + for (Register r : eqRegs) { + conjuncts.add(new NumericBooleanExpression(r, NumericComparator.NE, param)); + } + guard = ExpressionUtil.and(conjuncts); + } + + Transition transition = new Transition(in, guard, srcLoc, destLoc, new Assignment(assignmentMapping)); + ra.addTransition(srcLoc, in, transition); + q.add(destNode); + } + + // add sink transition to sink + if (!srcNode.getChildren().containsKey(srcNode.getMaxMemV()+1)) { + VarMapping assignmentMapping = new VarMapping<>(); + // create guard for the fresh case + List> conjuncts = new ArrayList<>(srcRegs.length); + for (Register r : eqRegs) { + conjuncts.add(new NumericBooleanExpression(r, NumericComparator.NE, param)); + } + Expression guard = ExpressionUtil.and(conjuncts); + Transition transition = new Transition(in, guard, srcLoc, sink, new Assignment(assignmentMapping)); + ra.addTransition(srcLoc, in, transition); + } + } + + // add sink self-loop transition + VarMapping assignmentMapping = new VarMapping<>(); + Expression guard = ExpressionUtil.TRUE; + Transition transition = new Transition(in, guard, sink, sink, new Assignment(assignmentMapping)); + ra.addTransition(sink, in, transition); + + return ra; + } + + private static int TEST_MAX_LEN = 8; + + private static boolean isPalindrome(List word) { + for (int i=0; i> q = new ArrayDeque<>(); + q.add(Collections.emptyList()); + while (!q.isEmpty()) { + List valWord = q.poll(); + WordBuilder wb = new WordBuilder(); + valWord.forEach(d -> + wb.add(new PSymbolInstance(IN, + new DataValue(TYPE, BigDecimal.valueOf(d))))); + Assert.assertEquals(ra.accepts(wb.toWord()), isPalindrome(valWord), "Mismatch for word " + valWord); + if (valWord.size() < TEST_MAX_LEN) { + if (valWord.isEmpty()) { + q.add(Arrays.asList(1)); + } else { + Integer maxVal = valWord.stream().max((i1, i2) -> i1.compareTo(i2)).get(); + for (int i=1; i<= maxVal+1; i++) { + List next = new ArrayList<>(valWord); + next.add(i); + q.add(next); + } + } + } + } + } +} diff --git a/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeOracle.java b/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeOracle.java new file mode 100644 index 00000000..caf06a7f --- /dev/null +++ b/src/test/java/de/learnlib/ralib/example/palindrome/PalindromeOracle.java @@ -0,0 +1,46 @@ +package de.learnlib.ralib.example.palindrome; + +import java.util.Collection; + +import de.learnlib.query.Query; +import de.learnlib.ralib.data.DataType; +import de.learnlib.ralib.oracles.DataWordOracle; +import de.learnlib.ralib.words.InputSymbol; +import de.learnlib.ralib.words.PSymbolInstance; +import net.automatalib.word.Word; + +public class PalindromeOracle implements DataWordOracle { + + public static final DataType TYPE = new DataType("int"); + public static final InputSymbol IN = new InputSymbol("in", new DataType[] {TYPE}); + + private final Palindrome pal; + + public PalindromeOracle(Palindrome pal) { + this.pal = pal; + } + + @Override + public void processQueries(Collection> queries) { + for (Query q : queries) { + q.answer(answer(q.getInput())); + } + } + + private boolean answer(Word word) { + pal.reset(); + boolean isPalindrome = true; + for (PSymbolInstance psi : word) { + isPalindrome = answer(psi); + } + return isPalindrome; + } + + private boolean answer(PSymbolInstance psi) { + if (!psi.getBaseSymbol().equals(IN)) { + return false; + } + int d = psi.getParameterValues()[0].getValue().intValue(); + return pal.in(d); + } +} diff --git a/src/test/java/de/learnlib/ralib/learning/LearnPalindromeTest.java b/src/test/java/de/learnlib/ralib/learning/LearnPalindromeTest.java new file mode 100644 index 00000000..20ac7be3 --- /dev/null +++ b/src/test/java/de/learnlib/ralib/learning/LearnPalindromeTest.java @@ -0,0 +1,120 @@ +package de.learnlib.ralib.learning; + +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.IN; +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.TYPE; + +import java.util.LinkedHashMap; +import java.util.Map; + +import org.testng.annotations.Test; + +import de.learnlib.query.DefaultQuery; +import de.learnlib.ralib.CacheDataWordOracle; +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.equivalence.RAEquivalenceTest; +import de.learnlib.ralib.example.palindrome.Palindrome; +import de.learnlib.ralib.example.palindrome.PalindromeGenerator; +import de.learnlib.ralib.example.palindrome.PalindromeOracle; +import de.learnlib.ralib.learning.ralambda.SLLambda; +import de.learnlib.ralib.learning.rastar.RaStar; +import de.learnlib.ralib.oracles.DataWordOracle; +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.smt.ConstraintSolver; +import de.learnlib.ralib.theory.Theory; +import de.learnlib.ralib.tools.theories.IntegerEqualityTheory; +import de.learnlib.ralib.words.PSymbolInstance; + +public class LearnPalindromeTest extends RaLibTestSuite { + + // TODO Create a system for managing configuration of tests. + private static final int PALINDROME_SIZE = Integer.valueOf(System.getProperty("palindrome.size", "6")); + + private void printHeader() { + System.out.println("======================="); + System.out.println("========== " + PALINDROME_SIZE + " =========="); + System.out.println("======================="); + } + + @Test(enabled = true) + public void testLearnPalindromeSLLambda() { + testLearnPalindrome(PALINDROME_SIZE, RaLearningAlgorithmName.RALAMBDA); + } + + @Test(enabled = true) + public void testLearnPalindromeSLStar() { + testLearnPalindrome(PALINDROME_SIZE, RaLearningAlgorithmName.RASTAR); + } + + public void testLearnPalindrome(int size, RaLearningAlgorithmName name) { + RegisterAutomaton model = PalindromeGenerator.generate(size); + + RaLearningAlgorithm algorithm = makeLearner(name); + printHeader(); + + Map teachers = new LinkedHashMap<>(); + teachers.put(TYPE, new IntegerEqualityTheory(TYPE)); + RAEquivalenceTest checker = new RAEquivalenceTest(model, teachers, new Constants(), true, IN); + learn(algorithm, checker, name); + } + + private RaLearningAlgorithm makeLearner(RaLearningAlgorithmName name) { + Constants consts = new Constants(); + ConstraintSolver solver = new ConstraintSolver(); + + Palindrome pal = new Palindrome(PALINDROME_SIZE); + DataWordOracle oracle = new PalindromeOracle(pal); + CacheDataWordOracle cacheOracle = new CacheDataWordOracle(oracle); + + Map teachers = new LinkedHashMap<>(); + IntegerEqualityTheory iet = new IntegerEqualityTheory(TYPE); + iet.setUseSuffixOpt(true); + teachers.put(TYPE, iet); + + MultiTheoryTreeOracle mto = new MultiTheoryTreeOracle(cacheOracle, teachers, consts, solver); + SDTLogicOracle slo = new MultiTheorySDTLogicOracle(consts, solver); + TreeOracleFactory hypFactory = (RegisterAutomaton hyp) -> new MultiTheoryTreeOracle(new SimulatorOracle(hyp), + teachers, consts, solver); + + Measurements mes = new Measurements(); + QueryStatistics queryStats = new QueryStatistics(mes, cacheOracle); + + RaLearningAlgorithm learner = null; + switch (name) { + case RALAMBDA -> learner = new SLLambda(mto, teachers, consts, false, solver, IN); + case RASTAR -> learner = new RaStar(mto, hypFactory, slo, consts, false, IN); + default -> throw new RuntimeException("Unsupported algorithm %s".formatted(name.name())); + } + learner.setStatisticCounter(queryStats); + + return learner; + } + + private void learn(RaLearningAlgorithm learner, RAEquivalenceTest checker, RaLearningAlgorithmName name) { + learner.learn(); + DefaultQuery ce = checker.findCounterExample(learner.getHypothesis(), null); + while (ce != null) { + System.out.println(ce); + learner.addCounterexample(ce); + learner.learn(); + ce = checker.findCounterExample(learner.getHypothesis(), null); + } + + System.out.println(learner.getQueryStatistics()); + Hypothesis hyp = learner.getHypothesis(); + System.out.println("Hyp. Locations: " + hyp.getStates().size()); + System.out.println("Hyp. Transitions: " + hyp.getTransitions().size()); + + // input locations + transitions + System.out.println("Hyp. Input Locations: " + hyp.getInputStates().size()); + System.out.println("Hyp. Input Transitions: " + hyp.getInputTransitions().size()); + + System.out.println("Hyp. Registers: " + hyp.getRegisters().size()); + } +} diff --git a/src/test/java/de/learnlib/ralib/learning/ralambda/LearnPalindromeTest.java b/src/test/java/de/learnlib/ralib/learning/ralambda/LearnPalindromeTest.java new file mode 100644 index 00000000..13bd5a19 --- /dev/null +++ b/src/test/java/de/learnlib/ralib/learning/ralambda/LearnPalindromeTest.java @@ -0,0 +1,172 @@ +package de.learnlib.ralib.learning.ralambda; + +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.IN; +import static de.learnlib.ralib.example.palindrome.PalindromeOracle.TYPE; + +import java.math.BigDecimal; +import java.util.ArrayList; +import java.util.Collection; +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.CacheDataWordOracle; +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.equivalence.RAEquivalenceTest; +import de.learnlib.ralib.example.palindrome.Palindrome; +import de.learnlib.ralib.example.palindrome.PalindromeGenerator; +import de.learnlib.ralib.example.palindrome.PalindromeOracle; +import de.learnlib.ralib.learning.Measurements; +import de.learnlib.ralib.learning.QueryStatistics; +import de.learnlib.ralib.learning.RaLearningAlgorithm; +import de.learnlib.ralib.oracles.DataWordOracle; +import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle; +import de.learnlib.ralib.smt.ConstraintSolver; +import de.learnlib.ralib.theory.Theory; +import de.learnlib.ralib.tools.theories.IntegerEqualityTheory; +import de.learnlib.ralib.words.PSymbolInstance; +import net.automatalib.word.Word; + +public class LearnPalindromeTest extends RaLibTestSuite { + + private static final int SIZE = Integer.valueOf(System.getProperty("palindrome.size", "10")); + + @Test(enabled=true) + public void testLearnPalindrome() { + System.out.println("======================="); + System.out.println("========== " + SIZE + " =========="); + System.out.println("======================="); + + SLLambda learnerLambda = makeLearner(); + + Collection> ces = generateCounterexamples(SIZE); + + RegisterAutomaton model = PalindromeGenerator.generate(SIZE); + for (DefaultQuery ce : ces) { + Assert.assertEquals(model.accepts(ce.getInput()), ce.getOutput()); + } + + Map teachers = new LinkedHashMap<>(); + teachers.put(TYPE, new IntegerEqualityTheory(TYPE)); + RAEquivalenceTest checker = new RAEquivalenceTest(model, teachers, new Constants(), true, IN); + + learn(learnerLambda, checker, "SLLambda"); + //learn(learnerStar, checker, "SLStar"); + } + + private SLLambda makeLearner() { + Constants consts = new Constants(); + ConstraintSolver solver = new ConstraintSolver(); + + Palindrome pal = new Palindrome(SIZE); + DataWordOracle oracle = new PalindromeOracle(pal); + CacheDataWordOracle cacheOracle = new CacheDataWordOracle(oracle); + + Map teachers = new LinkedHashMap<>(); + IntegerEqualityTheory iet = new IntegerEqualityTheory(TYPE); + teachers.put(TYPE, iet); + + MultiTheoryTreeOracle mto = new MultiTheoryTreeOracle(cacheOracle, teachers, consts, solver); + + Measurements mes = new Measurements(); + QueryStatistics queryStats = new QueryStatistics(mes, cacheOracle); + +// SLLambda learner = version > 0 ? +// new SLLambda(mto, teachers, consts, false, solver, SymbolicSuffixRestrictionBuilder.Version.fromInt(version), in) : +// new SLLambda(mto, teachers, consts, false, solver, in); + SLLambda learner = new SLLambda(mto, teachers, consts, false, solver, IN); + learner.setStatisticCounter(queryStats); + + learner.learn(); + + return learner; + } + + + private void learn(RaLearningAlgorithm learner, RAEquivalenceTest checker, String name) { + String dashes = "----"; + for (int i = 0; i < name.length(); i++) { + dashes = dashes + "-"; + } + dashes = dashes + "----"; + System.out.println(dashes); + System.out.println("--- " + name + " ---"); + System.out.println(dashes); + + DefaultQuery ce = checker.findCounterExample(learner.getHypothesis(), null); + while (ce != null) { + System.out.println(ce); + learner.addCounterexample(ce); + learner.learn(); + ce = checker.findCounterExample(learner.getHypothesis(), null); + } + + System.out.println(learner.getQueryStatistics()); + } + + private Collection> generateCounterexamples(int size) { + Collection> ces = new ArrayList<>(); + if (size < 2) { + return ces; + } + + ces.add(new DefaultQuery<>(Word.fromSymbols( + new PSymbolInstance(IN, new DataValue(TYPE, BigDecimal.ZERO)), + new PSymbolInstance(IN, new DataValue(TYPE, BigDecimal.ONE))), false)); + + if (size < 3) { + return ces; + } + + for (int s = 3; s <= size; s++) { + int[] pal = generatePalindrome(s); + Word ce = Word.epsilon(); + for (int p : pal) { + PSymbolInstance psi = new PSymbolInstance(IN, new DataValue(TYPE, BigDecimal.valueOf(p))); + ce = ce.append(psi); + } + ces.add(new DefaultQuery<>(ce, true)); + } + + Word ce = Word.epsilon(); + for (int i = 0; i <= size; i++) { + PSymbolInstance psi = new PSymbolInstance(IN, new DataValue(TYPE, BigDecimal.ZERO)); + ce = ce.append(psi); + } + ces.add(new DefaultQuery<>(ce, false)); + + return ces; + } + + private boolean checkCe(DefaultQuery q) { + Palindrome pal = new Palindrome(SIZE); + + boolean acc = true; + for (PSymbolInstance psi : q.getInput()) { + int d = psi.getParameterValues()[0].getValue().intValue(); + acc = pal.in(d); + } + return q.getOutput().booleanValue() == acc; + } + + private int[] generatePalindrome(int n) { + int[] arr = new int[n]; + for (int i = 0; i < n/2; i++) { + arr[i] = i; + } + if (n % 2 == 1) { + arr[n/2] = n/2; + } + for (int i = 0; i < n/2; i++) { + arr[n-i-1] = arr[i]; + } + return arr; + } +}