diff --git a/java/Main.java b/java/Main.java index f4ca23d..db25dc0 100644 --- a/java/Main.java +++ b/java/Main.java @@ -15,6 +15,9 @@ import de.learnlib.eqtests.basic.WpMethodEQOracle; import de.learnlib.oracles.AbstractSingleQueryOracle; import de.learnlib.oracles.DefaultQuery; import de.learnlib.oracles.SimulatorOracle; +import de.learnlib.parallelism.DynamicParallelOracle; +import de.learnlib.parallelism.ParallelOracle; +import de.learnlib.parallelism.ParallelOracleBuilders; import net.automatalib.automata.transout.MealyMachine; import net.automatalib.automata.transout.impl.compact.CompactMealy; import net.automatalib.util.graphs.dot.GraphDOT; @@ -28,6 +31,7 @@ import java.io.IOException; import java.io.PrintWriter; import java.nio.file.Paths; import java.util.*; +import java.util.function.Supplier; import static de.learnlib.cache.mealy.MealyCaches.createCache; @@ -55,8 +59,12 @@ public class Main { // queries needed to find a counterexample. System.out.println("Setting up membership oracles"); SimulatorOracle.MealySimulatorOracle mOracleMealy = new SimulatorOracle.MealySimulatorOracle<>(fm); - CountingQueryOracle> mOracleCounting1 = new CountingQueryOracle<>(mOracleMealy); - CountingQueryOracle> mOracleCounting2 = new CountingQueryOracle<>(mOracleMealy); + DynamicParallelOracle> mParallelOracle = ParallelOracleBuilders.newDynamicParallelOracle(() -> { + return new SimulatorOracle.MealySimulatorOracle<>(fm); + }).withBatchSize(5) + .withPoolSize(4) + .withPoolPolicy(ParallelOracle.PoolPolicy.FIXED) + .create(); // We can test multiple equivalence oracles. The eqOracleMealy sees the SUL as a white box mealy machine to @@ -65,11 +73,9 @@ public class Main { // the Lee and Yannakakis oracle. System.out.println("Setting up equivalence oracles"); SimulatorEQOracle.MealySimulatorEQOracle eqOracleMealy = new SimulatorEQOracle.MealySimulatorEQOracle<>(fm); - WpMethodEQOracle.MealyWpMethodEQOracle eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mOracleCounting2); - WMethodEQOracle.MealyWMethodEQOracle eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mOracleCounting2); - EquivalenceOracle.MealyEquivalenceOracle eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mOracleCounting2); - EquivalenceOracle.MealyEquivalenceOracle eqOracleSpecific = new SpecificCounterExampleOracle(mOracleCounting2); - EQOracleChain.MealyEQOracleChain eqOracleYannakakisPlus = new EQOracleChain.MealyEQOracleChain(Arrays.asList(eqOracleSpecific, eqOracleYannakakis)); + WpMethodEQOracle.MealyWpMethodEQOracle eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mParallelOracle); + WMethodEQOracle.MealyWMethodEQOracle eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mParallelOracle); + EquivalenceOracle.MealyEquivalenceOracle eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mParallelOracle); // The chosen oracle to experiment with. EquivalenceOracle.MealyEquivalenceOracle eqOracle = eqOracleYannakakis; @@ -77,8 +83,8 @@ public class Main { // Learnlib comes with different learning algorithms System.out.println("Setting up learner(s)"); - MealyDHC learnerDHC = new MealyDHC<>(alphabet, mOracleCounting1); - ExtensibleLStarMealy learnerLStar = new ExtensibleLStarMealy<>(alphabet, mOracleCounting1, Lists.>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_FIRST); + MealyDHC learnerDHC = new MealyDHC<>(alphabet, mParallelOracle); + ExtensibleLStarMealy learnerLStar = new ExtensibleLStarMealy<>(alphabet, mParallelOracle, Lists.>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_FIRST); // The chosen learning algorithm LearningAlgorithm.MealyLearner learner = learnerLStar; @@ -106,15 +112,11 @@ public class Main { System.out.println(stage++ + ": " + Calendar.getInstance().getTime()); System.out.println("Hypothesis has " + learner.getHypothesisModel().getStates().size() + " states"); - mOracleCounting1.log_and_reset("learning"); - mOracleCounting2.log_and_reset("finding a counter example"); System.out.println(); } System.out.println(stage++ + ": " + Calendar.getInstance().getTime()); System.out.println("Conclusion has " + learner.getHypothesisModel().getStates().size() + " states"); - mOracleCounting1.log_and_reset("learning"); - mOracleCounting2.log_and_reset("finding a counter example"); System.out.println("Done!"); PrintWriter output = new PrintWriter("last_hypothesis.dot"); @@ -154,32 +156,4 @@ public class Main { return delegate.answerQuery(word, word1); } } - - /** - * An equivalence oracle to test a single sequence, which I needed to learn the Oce test case. - */ - public static class SpecificCounterExampleOracle implements EquivalenceOracle.MealyEquivalenceOracle { - private final MembershipOracle> sulOracle; - private boolean fired = false; - - SpecificCounterExampleOracle(MembershipOracle> sulOracle){ - this.sulOracle = sulOracle; - } - - @Nullable - @Override - public DefaultQuery> findCounterExample(MealyMachine objects, Collection collection) { - if(fired) return null; - - WordBuilder wb = new WordBuilder<>(); - wb.append("52.5", "53.4", "21.0", "21.0", "21.0", "21.0", "21.0", "21.0", "21.0", "21.0", "21.0", "37.2", "10", "9.4"); - - Word test = wb.toWord(); - DefaultQuery> query = new DefaultQuery<>(test); - sulOracle.processQueries(Collections.singleton(query)); - - fired = true; - return query; - } - } } diff --git a/java/YannakakisEQOracle.java b/java/YannakakisEQOracle.java index c1739e7..5dd4945 100644 --- a/java/YannakakisEQOracle.java +++ b/java/YannakakisEQOracle.java @@ -23,10 +23,15 @@ import java.util.*; public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalenceOracle { private final MembershipOracle> sulOracle; private final List> alphabets; - private final ProcessBuilder pb; + private final ProcessBuilder pb = new ProcessBuilder("/Users/joshua/Documents/PhD/Yannakakis/build/main", "--", "1", "stream"); - int currentAlphabet = 0; + private int currentAlphabet = 0; private long bound = 100; + private long boundFactor = 10; // How much should it grow? + + // We buffer queries, in order to allow for parallel membership queries. + private int bufferSize = 100; + private ArrayList>> buffer = new ArrayList<>(bufferSize); private Process process; private Writer processInput; @@ -41,7 +46,6 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence YannakakisEQOracle(List> alphabets, MembershipOracle> sulOracle) throws IOException { this.sulOracle = sulOracle; this.alphabets = alphabets; - pb = new ProcessBuilder("/Users/joshua/Documents/PhD/Yannakakis/build/main", "--", "1", "stream"); } /** @@ -121,14 +125,21 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence while(true) { // start where we left previously for(; currentAlphabet < alphabets.size(); ++currentAlphabet){ - System.err.println("ERROR> log> Testing with subalphabet " + currentAlphabet); + System.err.println("ERROR> log> Testing with sub alphabet " + currentAlphabet); Alphabet a = alphabets.get(currentAlphabet); DefaultQuery> r = findCounterExampleImpl(machine, a, bound); - if (r != null) return r; + if (r != null) return r; // NOTE: at this point we might want to clear the buffer + + // We want to process the buffer, because if the counter example is in here, we want to continue + // with the current sub alphabet + if(!buffer.isEmpty()){ + r = checkAndEmptyBuffer(machine); + if(r != null){ return r; } + } } - System.err.println("ERROR> log> Increasing bound by a factor of 10"); currentAlphabet = 0; - bound *= 10; + bound *= boundFactor; + System.err.println("ERROR> log> Increased bound by a factor of 10: " + bound); } } @@ -146,16 +157,9 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence processInput.flush(); // Read every line outputted on stdout. + // We buffer the queries, so that a parallel membership query can be applied String line; while ((line = processOutput.readLine()) != null) { - // Break if we did not fin one in time - ++queryCount; - if(queryCount > bound) { - System.err.println("ERROR> log> Bound is reached"); - closeAll(); - return null; - } - // Read every string of the line, this will be a symbol of the input sequence. WordBuilder wb = new WordBuilder<>(); Scanner s = new Scanner(line); @@ -166,21 +170,24 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence // Convert to a word and test on the SUL Word test = wb.toWord(); DefaultQuery> query = new DefaultQuery<>(test); - sulOracle.processQueries(Collections.singleton(query)); + buffer.add(query); - // Also test on the hypothesis - Word o1 = machine.computeOutput(test); - Word o2 = query.getOutput(); + // Break if we did not fin one in time + ++queryCount; + if(queryCount > bound) { + System.err.println("ERROR> log> Bound is reached"); + closeAll(); + return null; + } - assert o1 != null; - assert o2 != null; - - // If equal => no counterexample :( - if(o1.equals(o2)) continue; - - // If not equal => counterexample :D - closeAll(); - return query; + // If the buffer is filled, we can perform the checks (possibly in parallel) + if(buffer.size() >= bufferSize){ + DefaultQuery> r = checkAndEmptyBuffer(machine); + if(r != null){ + closeAll(); + return r; + } + } } } catch (IOException e) { throw new RuntimeException("Unable to communicate with the external program: " + e); @@ -204,4 +211,25 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence // Here, the program exited normally, without counterexample, so we may return null. return null; } + + private DefaultQuery> checkAndEmptyBuffer(MealyMachine machine){ + sulOracle.processQueries(buffer); + DefaultQuery> r = inspectBuffer(machine); + buffer.clear(); + return r; + } + + private DefaultQuery> inspectBuffer(MealyMachine machine){ + for(DefaultQuery> query : buffer){ + Word o1 = machine.computeOutput(query.getInput()); + Word o2 = query.getOutput(); + + assert o1 != null; + assert o2 != null; + + // If equal => no counterexample :( + if(!o1.equals(o2)) return query; + } + return null; + } }