diff --git a/java/Main.java b/java/Main.java index 3c977a3..f4ca23d 100644 --- a/java/Main.java +++ b/java/Main.java @@ -21,15 +21,15 @@ import net.automatalib.util.graphs.dot.GraphDOT; import net.automatalib.words.Alphabet; import net.automatalib.words.Word; import net.automatalib.words.WordBuilder; +import net.automatalib.words.impl.Alphabets; import javax.annotation.Nullable; import java.io.IOException; import java.io.PrintWriter; import java.nio.file.Paths; -import java.util.Arrays; -import java.util.Calendar; -import java.util.Collection; -import java.util.Collections; +import java.util.*; + +import static de.learnlib.cache.mealy.MealyCaches.createCache; /** * Test for the Lee and Yannakakis implementation. @@ -42,7 +42,10 @@ public class Main { System.out.println("Reading dot file: " + filename); GraphvizParser p = new GraphvizParser(Paths.get(filename)); CompactMealy fm = p.createMachine(); + Alphabet alphabet = fm.getInputAlphabet(); + Alphabet subAlphabet = Alphabets.fromArray("21.1", "21.0", "22", "53.4", "52.5"); + List> alphabets = Arrays.asList(subAlphabet, alphabet); System.out.println("created machine with " + fm.size() + " states and " + alphabet.size() + " inputs\n"); @@ -64,12 +67,12 @@ public class Main { 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<>(mOracleCounting2); + EquivalenceOracle.MealyEquivalenceOracle eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mOracleCounting2); EquivalenceOracle.MealyEquivalenceOracle eqOracleSpecific = new SpecificCounterExampleOracle(mOracleCounting2); EQOracleChain.MealyEQOracleChain eqOracleYannakakisPlus = new EQOracleChain.MealyEQOracleChain(Arrays.asList(eqOracleSpecific, eqOracleYannakakis)); // The chosen oracle to experiment with. - EQOracleChain.MealyEQOracleChain eqOracle = eqOracleYannakakisPlus; + EquivalenceOracle.MealyEquivalenceOracle eqOracle = eqOracleYannakakis; // Learnlib comes with different learning algorithms @@ -95,11 +98,11 @@ public class Main { learner.refineHypothesis(ce); // FIXME: Make this a command line option - String dir = "/Users/joshua/Documents/PhD/Machines/Mealy/esms3/"; - String filenameh = dir + "hyp." + stage + ".obf.dot"; - PrintWriter output = new PrintWriter(filenameh); - GraphDOT.write(learner.getHypothesisModel(), alphabet, output); - output.close(); +// String dir = "/Users/joshua/Documents/PhD/Machines/Mealy/esms3/"; +// String filenameh = dir + "hyp." + stage + ".obf.dot"; +// PrintWriter output = new PrintWriter(filenameh); +// GraphDOT.write(learner.getHypothesisModel(), alphabet, output); +// output.close(); System.out.println(stage++ + ": " + Calendar.getInstance().getTime()); System.out.println("Hypothesis has " + learner.getHypothesisModel().getStates().size() + " states"); diff --git a/java/YannakakisEQOracle.java b/java/YannakakisEQOracle.java index 43676cf..c1739e7 100644 --- a/java/YannakakisEQOracle.java +++ b/java/YannakakisEQOracle.java @@ -5,14 +5,13 @@ import de.learnlib.api.MembershipOracle; import de.learnlib.oracles.DefaultQuery; import net.automatalib.automata.transout.MealyMachine; import net.automatalib.util.graphs.dot.GraphDOT; +import net.automatalib.words.Alphabet; import net.automatalib.words.Word; import net.automatalib.words.WordBuilder; import javax.annotation.Nullable; import java.io.*; -import java.util.Collection; -import java.util.Collections; -import java.util.Scanner; +import java.util.*; /** * Implements the Lee & Yannakakis suffixes by invoking an external program. Because of this indirection to an external @@ -23,8 +22,12 @@ import java.util.Scanner; */ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalenceOracle { private final MembershipOracle> sulOracle; + private final List> alphabets; private final ProcessBuilder pb; + int currentAlphabet = 0; + private long bound = 100; + private Process process; private Writer processInput; private BufferedReader processOutput; @@ -35,9 +38,10 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence * @param sulOracle The membership oracle of the SUL, we need this to check the output on the test suite * @throws IOException */ - YannakakisEQOracle(MembershipOracle> sulOracle) throws IOException { + YannakakisEQOracle(List> alphabets, MembershipOracle> sulOracle) throws IOException { this.sulOracle = sulOracle; - pb = new ProcessBuilder("/Users/joshua/Documents/Code/Kweekvijver/Yannakakis/build/main", "--", "1", "stream"); + this.alphabets = alphabets; + pb = new ProcessBuilder("/Users/joshua/Documents/PhD/Yannakakis/build/main", "--", "1", "stream"); } /** @@ -113,12 +117,29 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence @Nullable @Override public DefaultQuery> findCounterExample(MealyMachine machine, Collection inputs) { + // we're ignoring the external alphabet, only our own are used! + while(true) { + // start where we left previously + for(; currentAlphabet < alphabets.size(); ++currentAlphabet){ + System.err.println("ERROR> log> Testing with subalphabet " + currentAlphabet); + Alphabet a = alphabets.get(currentAlphabet); + DefaultQuery> r = findCounterExampleImpl(machine, a, bound); + if (r != null) return r; + } + System.err.println("ERROR> log> Increasing bound by a factor of 10"); + currentAlphabet = 0; + bound *= 10; + } + } + + private DefaultQuery> findCounterExampleImpl(MealyMachine machine, Collection inputs, long bound) { try { setupProcess(); } catch (IOException e) { throw new RuntimeException("Unable to start the external program: " + e); } + long queryCount = 0; try { // Write the hypothesis to stdin of the external program GraphDOT.write(machine, inputs, processInput); @@ -127,6 +148,14 @@ public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalence // Read every line outputted on stdout. 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);