diff --git a/java/Main.java b/java/Main.java index 7c03f4d..9bec0ec 100644 --- a/java/Main.java +++ b/java/Main.java @@ -1,27 +1,22 @@ package yannakakis; +import com.google.common.base.Supplier; import com.google.common.collect.Lists; import de.learnlib.acex.analyzers.AcexAnalyzers; -import de.learnlib.algorithms.dhc.mealy.MealyDHC; import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy; import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers; import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies; import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy; import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy; -import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealyBuilder; import de.learnlib.api.EquivalenceOracle; import de.learnlib.api.LearningAlgorithm; import de.learnlib.api.MembershipOracle; import de.learnlib.api.Query; import de.learnlib.counterexamples.LocalSuffixFinders; -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 de.learnlib.parallelism.DynamicParallelOracle; import de.learnlib.parallelism.ParallelOracle; import de.learnlib.parallelism.ParallelOracleBuilders; import net.automatalib.automata.transout.MealyMachine; @@ -29,73 +24,115 @@ 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 net.automatalib.words.impl.Alphabets; -import javax.annotation.Nullable; import java.io.IOException; import java.io.PrintStream; import java.io.PrintWriter; import java.nio.file.Paths; -import java.util.*; -import java.util.function.Consumer; -import java.util.function.Supplier; - -import static de.learnlib.cache.mealy.MealyCaches.createCache; +import java.util.Arrays; +import java.util.Calendar; +import java.util.Collection; +import java.util.List; /** * Test for the Lee and Yannakakis implementation. */ public class Main { + public static enum Method { LeeYannakakis, WMethod, WpMethod } + public static enum Learner { LStar, RivestSchapire, TTT, KearnsVazirani } + 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(); + // Some settings + boolean learnRealESM = false; + boolean saveAllHypotheses = false; + int threadsForMembershipQueries = 4; - Alphabet alphabet = fm.getInputAlphabet(); - Alphabet subAlphabet = Alphabets.fromArray("21.1", "21.0", "22", "53.4", "52.5"); - List> alphabets = Arrays.asList(subAlphabet, alphabet); + Method testMethod = Method.LeeYannakakis; + int maxDepthForWMethod = 2; - System.out.println("created machine with " + fm.size() + " states and " + alphabet.size() + " inputs\n"); + Learner learnAlgorithm = Learner.LStar; + + System.out.println("Setting up SUL"); + Supplier> supplier = null; + Alphabet alphabet = null; + List> alphabets = null; + + if(learnRealESM){ + // Real ESM + // I did not have this class, so I commented this out. +// long seed = 78465782; +// Random random = new Random(seed); +// supplier = new ESMOracleSupplier(random); +// +// alphabet = esmSupplier.getInputAlphabet(); +// Alphabet realSubAlphabet = esmSupplier.getSubAlphabet(); +// alphabets = Arrays.asList(realSubAlphabet, realAlphabet); + } else { + // A simulated ESM (by means of a mealy machine) + 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 = fm.getInputAlphabet(); + Alphabet simSubAlphabet = Alphabets.fromArray("21.1", "21.0", "22", "53.4", "52.5"); + alphabets = Arrays.asList(simSubAlphabet, alphabet); + + System.out.println(" created machine with " + fm.size() + " states and " + alphabet.size() + " inputs"); + + supplier = () -> { + return new SimulatorOracle.MealySimulatorOracle<>(fm); + }; + } + assert supplier != null; + assert alphabet != null; + assert alphabets != null; + + System.out.println("Setting up membership oracle"); + MembershipOracle> mParallelOracle = ParallelOracleBuilders + .newDynamicParallelOracle(supplier) + .withBatchSize(5) + .withPoolSize(threadsForMembershipQueries) + .withPoolPolicy(ParallelOracle.PoolPolicy.FIXED) + .create(); // 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); - DynamicParallelOracle> mParallelOracle = ParallelOracleBuilders.newDynamicParallelOracle(() -> { - return new SimulatorOracle.MealySimulatorOracle<>(fm); - }).withBatchSize(5) - .withPoolSize(4) - .withPoolPolicy(ParallelOracle.PoolPolicy.FIXED) - .create(); - CountingMembershipOracle> mOracleForLearning = new CountingMembershipOracle<>(mParallelOracle, "learning"); CountingMembershipOracle> mOracleForTesting = new CountingMembershipOracle<>(mParallelOracle, "testing"); - // We can test multiple equivalence oracles. They all treat the SUL as a black box. - System.out.println("Setting up equivalence oracles"); - WpMethodEQOracle.MealyWpMethodEQOracle eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mOracleForTesting); - WMethodEQOracle.MealyWMethodEQOracle eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mOracleForTesting); - EquivalenceOracle.MealyEquivalenceOracle eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mOracleForTesting); - - // The chosen oracle to experiment with. - EquivalenceOracle, String, Word> eqOracle = eqOracleYannakakis; + System.out.println("Setting up equivalence oracle"); + EquivalenceOracle, String, Word> eqOracle = null; + switch (testMethod){ + case LeeYannakakis: eqOracle = new YannakakisEQOracle<>(alphabets, mOracleForTesting); break; + case WMethod: eqOracle = new WMethodEQOracle.MealyWMethodEQOracle<>(maxDepthForWMethod, mOracleForTesting); break; + case WpMethod: eqOracle = new WpMethodEQOracle.MealyWpMethodEQOracle<>(maxDepthForWMethod, mOracleForTesting); break; + } + assert eqOracle != null; - // Learnlib comes with different learning algorithms - System.out.println("Setting up learner(s)"); - ExtensibleLStarMealy learnerLStar = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST); - TTTLearnerMealy learnerTTT = new TTTLearnerMealy<>(alphabet, mOracleForLearning, LocalSuffixFinders.FIND_LINEAR); - KearnsVaziraniMealy learnerKV = new KearnsVaziraniMealy<>(alphabet, mOracleForLearning, false, AcexAnalyzers.BINARY_SEARCH); - - // The chosen learning algorithm - LearningAlgorithm, String, Word> learner = learnerLStar; + System.out.println("Setting up learner"); + LearningAlgorithm, String, Word> learner = null; + switch (learnAlgorithm){ + case LStar: + learner = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST); + break; + case RivestSchapire: + learner = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.>newArrayList(), ObservationTableCEXHandlers.RIVEST_SCHAPIRE, ClosingStrategies.CLOSE_SHORTEST); + break; + case TTT: + learner = new TTTLearnerMealy<>(alphabet, mOracleForLearning, LocalSuffixFinders.FIND_LINEAR); + break; + case KearnsVazirani: + learner = new KearnsVaziraniMealy<>(alphabet, mOracleForLearning, false, AcexAnalyzers.BINARY_SEARCH); + break; + } + assert learner != null; // Here we will perform our experiment. I did not use the Experiment class from LearnLib, as I wanted some @@ -106,11 +143,13 @@ public class Main { learner.startLearning(); while(true) { -// 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(); + if(saveAllHypotheses) { + String dir = "/Users/joshua/Documents/PhD/Machines/Mealy/esms3/"; + String filename = dir + "hyp." + stage + ".obf.dot"; + PrintWriter output = new PrintWriter(filename); + GraphDOT.write(learner.getHypothesisModel(), alphabet, output); + output.close(); + } System.out.println(stage++ + ": " + Calendar.getInstance().getTime()); System.out.println("Hypothesis: " + learner.getHypothesisModel().getStates().size());