diff --git a/README.md b/README.md index e22ae74..6b0e432 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,7 @@ still useful for generating a seperating set (in the sense of Lee and Yannakakis). The partial leaves will be augmented via the classical seperating sequences. + ## Building ``` @@ -21,3 +22,8 @@ executable in the build directory. Note that you'll need c++14, but clang in Mac OSX will understand that (and if not, you'll have to update Xcode). +## Java + +For now the java code, which acts as a bridge between LearnLib and this c++ +tool, is included here. But it should earn its own repo at some point. Also, my +javanese is a bit rusty... diff --git a/java/GraphvizParser.java b/java/GraphvizParser.java new file mode 100644 index 0000000..2815a8d --- /dev/null +++ b/java/GraphvizParser.java @@ -0,0 +1,86 @@ +package yannakakis; + +import com.google.common.collect.Lists; +import net.automatalib.automata.transout.impl.compact.CompactMealy; +import net.automatalib.util.automata.builders.AutomatonBuilders; +import net.automatalib.util.automata.builders.MealyBuilder; +import net.automatalib.words.Alphabet; +import net.automatalib.words.impl.Alphabets; + +import java.io.IOException; +import java.nio.file.Path; +import java.util.HashSet; +import java.util.List; +import java.util.Scanner; +import java.util.Set; + +/** + * A class which is just able to parse the output generated by LearnLib (why is this not included in LearnLib itself? + * I have no clue.) It is *not* a general graphviz parser, it only parses the things I needed for the mealy machines. + */ +public class GraphvizParser { + public static class Edge { + public String from; + public String to; + public String label; + Edge(String b, String e, String l){ + from = b; + to = e; + label = l; + } + } + + public Set nodes; + public Set edges; + + GraphvizParser(Path filename) throws IOException { + nodes = new HashSet<>(); + edges = new HashSet<>(); + + Scanner s = new Scanner(filename); + while(s.hasNextLine()){ + String line = s.nextLine(); + + if(!line.contains("label")) continue; + + if(line.contains("->")){ + int e1 = line.indexOf('-'); + int e2 = line.indexOf('['); + int b3 = line.indexOf('"'); + int e3 = line.lastIndexOf('"'); + + String from = line.substring(0, e1).trim(); + String to = line.substring(e1+2, e2).trim(); + String label = line.substring(b3+1, e3).trim(); + + edges.add(new Edge(from, to, label)); + } else { + int end = line.indexOf('['); + if(end <= 0) continue; + String node = line.substring(0, end).trim(); + + nodes.add(node); + } + } + } + + CompactMealy createMachine(){ + Set inputs = new HashSet<>(); + for(GraphvizParser.Edge e : edges){ + String[] io = e.label.split("/"); + inputs.add(io[0].trim()); + } + + List inputList = Lists.newArrayList(inputs.iterator()); + Alphabet alphabet = Alphabets.fromList(inputList); + + MealyBuilder>.MealyBuilder__1 builder = AutomatonBuilders.newMealy(alphabet).withInitial("s0"); + for(GraphvizParser.Edge e : edges){ + String[] io = e.label.split("/"); + + builder.from(e.from).on(io[0].trim()).withOutput(io[1].trim()).to(e.to); + } + + return builder.create(); + } +} diff --git a/java/Main.java b/java/Main.java new file mode 100644 index 0000000..3c977a3 --- /dev/null +++ b/java/Main.java @@ -0,0 +1,182 @@ +package yannakakis; + +import com.google.common.collect.Lists; +import de.learnlib.algorithms.dhc.mealy.MealyDHC; +import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers; +import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies; +import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy; +import de.learnlib.api.EquivalenceOracle; +import de.learnlib.api.LearningAlgorithm; +import de.learnlib.api.MembershipOracle; +import de.learnlib.eqtests.basic.EQOracleChain; +import de.learnlib.eqtests.basic.SimulatorEQOracle; +import de.learnlib.eqtests.basic.WMethodEQOracle; +import de.learnlib.eqtests.basic.WpMethodEQOracle; +import de.learnlib.oracles.AbstractSingleQueryOracle; +import de.learnlib.oracles.DefaultQuery; +import de.learnlib.oracles.SimulatorOracle; +import net.automatalib.automata.transout.MealyMachine; +import net.automatalib.automata.transout.impl.compact.CompactMealy; +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.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; + +/** + * Test for the Lee and Yannakakis implementation. + */ +public class Main { + + public static void main(String[] args) throws IOException { + // We read the mealy machine we want to simulate + String filename = "esm-manual-controller.dot"; + System.out.println("Reading dot file: " + filename); + GraphvizParser p = new GraphvizParser(Paths.get(filename)); + CompactMealy fm = p.createMachine(); + Alphabet alphabet = fm.getInputAlphabet(); + + System.out.println("created machine with " + fm.size() + " states and " + alphabet.size() + " inputs\n"); + + + // We will have the simulating membership oracle. Since the equivalence oracles use a membership oracle to + // test equality, we make membership oracle which maintain a count. E.g. This way we can count the number of + // 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); + + + // We can test multiple equivalence oracles. The eqOracleMealy sees the SUL as a white box mealy machine to + // find a counterexample. The others all treat the SUL as a black box. Since there was one specific + // counterexample which was hard to find, I created an oracle precisely for that example, and chain it with + // 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<>(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; + + + // 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); + + // The chosen learning algorithm + LearningAlgorithm.MealyLearner learner = learnerLStar; + + + // Here we will perform our experiment. I did not use the Experiment class from LearnLib, as I wanted some + // more control (for example, I want to reset the counters in the membership oracles). This control flow + // is suggested by LearnLib (on their wiki). + System.out.println("Starting experiment\n"); + int stage = 0; + learner.startLearning(); + + while(true) { + DefaultQuery> ce = eqOracle.findCounterExample(learner.getHypothesisModel(), alphabet); + if(ce == null) break; + + 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(); + + 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"); + GraphDOT.write(learner.getHypothesisModel(), alphabet, output); + output.close(); + } + + /** + * An membership oracle which maintains a count of the number of queries (and symbols). Usefull for testing + * performance of equivalence oracles (which use membership oracles). + * @param Input alphabet + * @param Output alphabet + */ + public static class CountingQueryOracle extends AbstractSingleQueryOracle{ + private final AbstractSingleQueryOracle delegate; + public int query_count = 0; + public int symbol_count = 0; + + CountingQueryOracle(AbstractSingleQueryOracle delegate){ + this.delegate = delegate; + } + + public void reset(){ + query_count = 0; + symbol_count = 0; + } + + public void log_and_reset(String message){ + System.out.println("used " + query_count + " queries and " + symbol_count + " symbols for " + message); + reset(); + } + + @Override + public O answerQuery(Word word, Word word1) { + query_count++; + symbol_count += word.length() + word1.length(); + 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 new file mode 100644 index 0000000..43676cf --- /dev/null +++ b/java/YannakakisEQOracle.java @@ -0,0 +1,178 @@ +package yannakakis; + +import de.learnlib.api.EquivalenceOracle; +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.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; + +/** + * Implements the Lee & Yannakakis suffixes by invoking an external program. Because of this indirection to an external + * program, the findCounterexample method might throw a RuntimeException. Sorry for the hard-coded path to the + * executable! + * + * @param is the output alphabet. (So a query will have type Word>.) + */ +public class YannakakisEQOracle implements EquivalenceOracle.MealyEquivalenceOracle { + private final MembershipOracle> sulOracle; + private final ProcessBuilder pb; + + private Process process; + private Writer processInput; + private BufferedReader processOutput; + private StreamGobbler errorGobbler; + + + /** + * @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 { + this.sulOracle = sulOracle; + pb = new ProcessBuilder("/Users/joshua/Documents/Code/Kweekvijver/Yannakakis/build/main", "--", "1", "stream"); + } + + /** + * A small class to print all stuff to stderr. Useful as I do not want stderr and stdout of the external program to + * be merged, but still want to redirect stderr to java's stderr. + */ + class StreamGobbler extends Thread { + private final InputStream stream; + private final String prefix; + + StreamGobbler(InputStream stream, String prefix) { + this.stream = stream; + this.prefix = prefix; + } + + public void run() { + try { + BufferedReader reader = new BufferedReader(new InputStreamReader(stream)); + String line; + while ((line = reader.readLine()) != null) + System.err.println(prefix + "> " + line); + } catch (IOException e) { + // It's fine if this thread crashes, nothing depends on it + e.printStackTrace(); + } + } + } + + /** + * Starts the process and creates buffered/whatnot streams for stdin stderr or the external program + * @throws IOException if the process could not be started (see ProcessBuilder.start for details). + */ + private void setupProcess() throws IOException { + process = pb.start(); + processInput = new OutputStreamWriter(process.getOutputStream()); + processOutput = new BufferedReader(new InputStreamReader(process.getInputStream())); + errorGobbler = new StreamGobbler(process.getErrorStream(), "ERROR> main"); + errorGobbler.start(); + } + + /** + * I thought this might be a good idea, but I'm not a native Java speaker, so maybe it's not needed. + */ + private void closeAll() { + // Since we're closing, I think it's ok to continue in case of an exception + try { + processInput.close(); + processOutput.close(); + } catch (IOException e) { + e.printStackTrace(); + } + try { + errorGobbler.join(10); + } catch (InterruptedException e) { + e.printStackTrace(); + } + process.destroy(); + process = null; + processInput = null; + processOutput = null; + errorGobbler = null; + } + + /** + * Uses an external program to find counterexamples. The hypothesis will be written to stdin. Then the external + * program might do some calculations and write its test suite to stdout. This is in turn read here and fed + * to the SUL. If a discrepancy occurs, an counterexample is returned. If the external program exits (with value + * 0), then no counterexample is found, and the hypothesis is correct. + * + * This method might throw a RuntimeException if the external program crashes (which it shouldn't of course), or if + * the communication went wrong (for whatever IO reason). + */ + @Nullable + @Override + public DefaultQuery> findCounterExample(MealyMachine machine, Collection inputs) { + try { + setupProcess(); + } catch (IOException e) { + throw new RuntimeException("Unable to start the external program: " + e); + } + + try { + // Write the hypothesis to stdin of the external program + GraphDOT.write(machine, inputs, processInput); + processInput.flush(); + + // Read every line outputted on stdout. + String line; + while ((line = processOutput.readLine()) != 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); + while(s.hasNext()) { + wb.add(s.next()); + } + + // Convert to a word and test on the SUL + Word test = wb.toWord(); + DefaultQuery> query = new DefaultQuery<>(test); + sulOracle.processQueries(Collections.singleton(query)); + + // Also test on the hypothesis + Word o1 = machine.computeOutput(test); + Word o2 = query.getOutput(); + + assert o1 != null; + assert o2 != null; + + // If equal => no counterexample :( + if(o1.equals(o2)) continue; + + // If not equal => counterexample :D + closeAll(); + return query; + } + } catch (IOException e) { + throw new RuntimeException("Unable to communicate with the external program: " + e); + } + + // At this point, the external program closed its stream, so it should have exited. + if(process.isAlive()){ + System.err.println("ERROR> log> No counterexample but process stream still active!"); + closeAll(); + throw new RuntimeException("No counterexample but process stream still active!"); + } + + // If the program exited with a non-zero value, something went wrong (for example a segfault)! + int ret = process.exitValue(); + if(ret != 0){ + System.err.println("ERROR> log> Something went wrong with the process: return value = " + ret); + closeAll(); + throw new RuntimeException("Something went wrong with the process: return value = " + ret); + } + + // Here, the program exited normally, without counterexample, so we may return null. + return null; + } +} diff --git a/scripts.md b/scripts.md deleted file mode 100644 index 8123016..0000000 --- a/scripts.md +++ /dev/null @@ -1,46 +0,0 @@ -all -=== - - -for f in *.dot; do ../build/main $f; done -for f in *splitting_tree; do sed -i "" -e 's/label="........................................*"/label="truncated"/g' $f; done -for f in *dist_seq; do sed -i "" -e 's/label="........................................*"/label="truncated"/g' $f; done -dot -O -Tpng -Goverlap=false *dist_seq -dot -O -Tpng -Goverlap=false *splitting_tree - - -graphs -====== - -dot -O -Tpng -Goverlap=false *dist_seq -dot -O -Tpng -Goverlap=false *splitting_tree - -neato -O -Tpng -Goverlap=false *.dot - - -truncation -========== - -sed 's/label="........................................*"/label="truncated"/g' esm-manual-controller.dot.splitting_tree.dot > esm-manual-controller.dot.splitting_tree_truncated.dot - -for f in *splitting_tree; do echo $f; sed -i "" -e 's/label="........................................*"/label="truncated"/g' $f; done -for f in *dist_seq; do echo $f; sed -i "" -e 's/label="........................................*"/label="truncated"/g' $f; done - - -cleaning -======== - -sed 's/\[label.*I/ \[label="/g;s/<\/td>.*O/ \/ /g;s/<\/td>.*]/"\];/g' - - -not needed ctor -=============== - -partition_refine(Blocks other_blocks){ - auto beg = elements.begin(); - for(auto && block : other_blocks){ - std::copy(block.begin(), block.end(), std::back_inserter(elements)); - blocks.insert(blocks.end(), {beg, std::prev(elements.end())}); - beg = elements.end(); - } -}