check all subwords

learnlib/DumpRFSAEQOracle.java

@@ -2,15 +2,17 @@ import de.learnlib.api.oracle.MembershipOracle;
 import de.learnlib.api.query.DefaultQuery;
 import de.learnlib.oracle.equivalence.RandomWordsEQOracle;
 import net.automatalib.automata.fsa.FiniteStateAcceptor;
-import net.automatalib.automata.fsa.NFA;
 import net.automatalib.automata.fsa.impl.compact.CompactNFA;
 import net.automatalib.words.Word;
 
 import javax.annotation.Nullable;
 import java.util.Collection;
+import java.util.Objects;
 import java.util.Random;
+import java.util.Set;
+import java.util.stream.Stream;
 
-public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends RandomWordsEQOracle<A, I, Boolean> {
+public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<Integer, I>, I> extends RandomWordsEQOracle<A, I, Boolean> {
     CompactNFA<I> target;
 
     public DumpRFSAEQOracle(CompactNFA<I> target, MembershipOracle<I, Boolean> mqOracle, int minLength, int maxLength, int maxTests) {
@@ -33,9 +35,20 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends Ra
     @Nullable
     @Override
     public DefaultQuery<I, Boolean> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
-        DefaultQuery<I, Boolean> a = super.findCounterExample(hypothesis, inputs);
-        if (a == null) { // no counterexample using random words found
         long startTime = System.nanoTime()/1000;
+        // Fail fast on empty inputs
+        if (inputs.isEmpty()) {
+            return null;
+        }
+
+        final Stream<Word<I>> testWordStream = generateTestWords(hypothesis, inputs);
+        final Stream<Word<I>> ceStream = testWordStream.map(word -> findCounterExampleElementwise(hypothesis, word));
+        Word<I> a = ceStream.filter(Objects::nonNull).findFirst().orElse(null);
+        System.out.print("random words: ");
+        System.out.println(System.nanoTime()/1000-startTime);
+
+        if (a == null) { // no counterexample using random words found
+            startTime = System.nanoTime()/1000;
             Word<I> counterEx = AutomataEq.eqCounterex(target, hypothesis);
             System.out.println(System.nanoTime()/1000-startTime);
 
@@ -45,6 +58,26 @@ public class DumpRFSAEQOracle<A extends FiniteStateAcceptor<?, I>, I> extends Ra
                 return new DefaultQuery<I, Boolean>(counterEx, target.computeOutput(counterEx));
             }
         }
-        return a;
+        return new DefaultQuery<I, Boolean>(a, target.computeOutput(a));
+    }
+
+    Word<I> findCounterExampleElementwise(A hypothesis, Word<I> word) {
+        Set<Integer> st1 = target.getInitialStates();
+        Set<Integer> st2 = hypothesis.getInitialStates();
+        int i = 0;
+        for (I c : word){
+            if (target.isAccepting(st1) != hypothesis.isAccepting(st2)) {
+                return word.subWord(0, i);
+            }
+
+            st1 = target.getSuccessors(st1, Word.fromSymbols(c));
+            st2 = hypothesis.getSuccessors(st2, Word.fromSymbols(c));
+
+            i++;
+        }
+        if(target.isAccepting(st1) != hypothesis.isAccepting(st2)) {
+            return word;
+        } else
+            return null;
     }
 }

learnlib/RFSALearnAndCompare.java

@@ -44,11 +44,11 @@ public class RFSALearnAndCompare<I> {
         NLStarLearner<I> nlstar2 = new NLStarLearnerBuilder<I>().withAlphabet(target.getInputAlphabet()) // input alphabet
                         .withOracle(mqOracle2) // reverse membership oracle
                         .create();
-        DumpRFSAEQOracle<NFA<?, I>, I> eqOracle = new DumpRFSAEQOracle<>(target, mqOracle_2, 0, maxLength, maxTests);
-        DumpRFSAEQOracle<NFA<?, I>, I> eqOracle2 = new DumpRFSAEQOracle<>(reverseTarget, mqOracle2_2, 0, maxLength, maxTests);
+        DumpRFSAEQOracle<NFA<Integer, I>, I> eqOracle = new DumpRFSAEQOracle<>(target, mqOracle_2, 0, maxLength, maxTests);
+        DumpRFSAEQOracle<NFA<Integer, I>, I> eqOracle2 = new DumpRFSAEQOracle<>(reverseTarget, mqOracle2_2, 0, maxLength, maxTests);
 
-        experiment = new Experiment<>(nlstar, eqOracle, target.getInputAlphabet());
-        experiment2 = new Experiment<>(nlstar2, eqOracle2, target.getInputAlphabet());
+        experiment = new Experiment(nlstar, eqOracle, target.getInputAlphabet()); //no type-checking here sry
+        experiment2 = new Experiment(nlstar2, eqOracle2, target.getInputAlphabet());
 
         experiment.run();
         experiment2.run();