mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 23:17:44 +02:00
Incorporates some changes by Wouter.
Makes main more dynamic and easy to adjust.
This commit is contained in:
parent
f13d8a0dd6
commit
ba868d39c5
1 changed files with 91 additions and 52 deletions
137
java/Main.java
137
java/Main.java
|
@ -1,27 +1,22 @@
|
||||||
package yannakakis;
|
package yannakakis;
|
||||||
|
|
||||||
|
import com.google.common.base.Supplier;
|
||||||
import com.google.common.collect.Lists;
|
import com.google.common.collect.Lists;
|
||||||
import de.learnlib.acex.analyzers.AcexAnalyzers;
|
import de.learnlib.acex.analyzers.AcexAnalyzers;
|
||||||
import de.learnlib.algorithms.dhc.mealy.MealyDHC;
|
|
||||||
import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy;
|
import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy;
|
||||||
import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers;
|
import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers;
|
||||||
import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies;
|
import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies;
|
||||||
import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy;
|
import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy;
|
||||||
import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy;
|
import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy;
|
||||||
import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealyBuilder;
|
|
||||||
import de.learnlib.api.EquivalenceOracle;
|
import de.learnlib.api.EquivalenceOracle;
|
||||||
import de.learnlib.api.LearningAlgorithm;
|
import de.learnlib.api.LearningAlgorithm;
|
||||||
import de.learnlib.api.MembershipOracle;
|
import de.learnlib.api.MembershipOracle;
|
||||||
import de.learnlib.api.Query;
|
import de.learnlib.api.Query;
|
||||||
import de.learnlib.counterexamples.LocalSuffixFinders;
|
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.WMethodEQOracle;
|
||||||
import de.learnlib.eqtests.basic.WpMethodEQOracle;
|
import de.learnlib.eqtests.basic.WpMethodEQOracle;
|
||||||
import de.learnlib.oracles.AbstractSingleQueryOracle;
|
|
||||||
import de.learnlib.oracles.DefaultQuery;
|
import de.learnlib.oracles.DefaultQuery;
|
||||||
import de.learnlib.oracles.SimulatorOracle;
|
import de.learnlib.oracles.SimulatorOracle;
|
||||||
import de.learnlib.parallelism.DynamicParallelOracle;
|
|
||||||
import de.learnlib.parallelism.ParallelOracle;
|
import de.learnlib.parallelism.ParallelOracle;
|
||||||
import de.learnlib.parallelism.ParallelOracleBuilders;
|
import de.learnlib.parallelism.ParallelOracleBuilders;
|
||||||
import net.automatalib.automata.transout.MealyMachine;
|
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.util.graphs.dot.GraphDOT;
|
||||||
import net.automatalib.words.Alphabet;
|
import net.automatalib.words.Alphabet;
|
||||||
import net.automatalib.words.Word;
|
import net.automatalib.words.Word;
|
||||||
import net.automatalib.words.WordBuilder;
|
|
||||||
import net.automatalib.words.impl.Alphabets;
|
import net.automatalib.words.impl.Alphabets;
|
||||||
|
|
||||||
import javax.annotation.Nullable;
|
|
||||||
import java.io.IOException;
|
import java.io.IOException;
|
||||||
import java.io.PrintStream;
|
import java.io.PrintStream;
|
||||||
import java.io.PrintWriter;
|
import java.io.PrintWriter;
|
||||||
import java.nio.file.Paths;
|
import java.nio.file.Paths;
|
||||||
import java.util.*;
|
import java.util.Arrays;
|
||||||
import java.util.function.Consumer;
|
import java.util.Calendar;
|
||||||
import java.util.function.Supplier;
|
import java.util.Collection;
|
||||||
|
import java.util.List;
|
||||||
import static de.learnlib.cache.mealy.MealyCaches.createCache;
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Test for the Lee and Yannakakis implementation.
|
* Test for the Lee and Yannakakis implementation.
|
||||||
*/
|
*/
|
||||||
public class Main {
|
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 {
|
public static void main(String[] args) throws IOException {
|
||||||
// We read the mealy machine we want to simulate
|
// Some settings
|
||||||
|
boolean learnRealESM = false;
|
||||||
|
boolean saveAllHypotheses = false;
|
||||||
|
int threadsForMembershipQueries = 4;
|
||||||
|
|
||||||
|
Method testMethod = Method.LeeYannakakis;
|
||||||
|
int maxDepthForWMethod = 2;
|
||||||
|
|
||||||
|
Learner learnAlgorithm = Learner.LStar;
|
||||||
|
|
||||||
|
System.out.println("Setting up SUL");
|
||||||
|
Supplier<MembershipOracle.MealyMembershipOracle<String, String>> supplier = null;
|
||||||
|
Alphabet<String> alphabet = null;
|
||||||
|
List<Alphabet<String>> 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<String> realSubAlphabet = esmSupplier.getSubAlphabet();
|
||||||
|
// alphabets = Arrays.asList(realSubAlphabet, realAlphabet);
|
||||||
|
} else {
|
||||||
|
// A simulated ESM (by means of a mealy machine)
|
||||||
String filename = "esm-manual-controller.dot";
|
String filename = "esm-manual-controller.dot";
|
||||||
System.out.println("Reading dot file: " + filename);
|
System.out.println(" Reading dot file: " + filename);
|
||||||
GraphvizParser p = new GraphvizParser(Paths.get(filename));
|
GraphvizParser p = new GraphvizParser(Paths.get(filename));
|
||||||
CompactMealy<String, String> fm = p.createMachine();
|
CompactMealy<String, String> fm = p.createMachine();
|
||||||
|
|
||||||
Alphabet<String> alphabet = fm.getInputAlphabet();
|
alphabet = fm.getInputAlphabet();
|
||||||
Alphabet<String> subAlphabet = Alphabets.fromArray("21.1", "21.0", "22", "53.4", "52.5");
|
Alphabet<String> simSubAlphabet = Alphabets.fromArray("21.1", "21.0", "22", "53.4", "52.5");
|
||||||
List<Alphabet<String>> alphabets = Arrays.asList(subAlphabet, alphabet);
|
alphabets = Arrays.asList(simSubAlphabet, alphabet);
|
||||||
|
|
||||||
System.out.println("created machine with " + fm.size() + " states and " + alphabet.size() + " inputs\n");
|
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<String, Word<String>> 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
|
// 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
|
// 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.
|
// queries needed to find a counterexample.
|
||||||
System.out.println("Setting up membership oracles");
|
|
||||||
SimulatorOracle.MealySimulatorOracle<String, String> mOracleMealy = new SimulatorOracle.MealySimulatorOracle<>(fm);
|
|
||||||
DynamicParallelOracle<String, Word<String>> mParallelOracle = ParallelOracleBuilders.newDynamicParallelOracle(() -> {
|
|
||||||
return new SimulatorOracle.MealySimulatorOracle<>(fm);
|
|
||||||
}).withBatchSize(5)
|
|
||||||
.withPoolSize(4)
|
|
||||||
.withPoolPolicy(ParallelOracle.PoolPolicy.FIXED)
|
|
||||||
.create();
|
|
||||||
|
|
||||||
CountingMembershipOracle<String, Word<String>> mOracleForLearning = new CountingMembershipOracle<>(mParallelOracle, "learning");
|
CountingMembershipOracle<String, Word<String>> mOracleForLearning = new CountingMembershipOracle<>(mParallelOracle, "learning");
|
||||||
CountingMembershipOracle<String, Word<String>> mOracleForTesting = new CountingMembershipOracle<>(mParallelOracle, "testing");
|
CountingMembershipOracle<String, Word<String>> 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 oracle");
|
||||||
System.out.println("Setting up equivalence oracles");
|
EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle = null;
|
||||||
WpMethodEQOracle.MealyWpMethodEQOracle<String, String> eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mOracleForTesting);
|
switch (testMethod){
|
||||||
WMethodEQOracle.MealyWMethodEQOracle<String, String> eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mOracleForTesting);
|
case LeeYannakakis: eqOracle = new YannakakisEQOracle<>(alphabets, mOracleForTesting); break;
|
||||||
EquivalenceOracle.MealyEquivalenceOracle<String, String> eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mOracleForTesting);
|
case WMethod: eqOracle = new WMethodEQOracle.MealyWMethodEQOracle<>(maxDepthForWMethod, mOracleForTesting); break;
|
||||||
|
case WpMethod: eqOracle = new WpMethodEQOracle.MealyWpMethodEQOracle<>(maxDepthForWMethod, mOracleForTesting); break;
|
||||||
// The chosen oracle to experiment with.
|
}
|
||||||
EquivalenceOracle<MealyMachine<?, String, ?, String>, String, Word<String>> eqOracle = eqOracleYannakakis;
|
assert eqOracle != null;
|
||||||
|
|
||||||
|
|
||||||
// Learnlib comes with different learning algorithms
|
System.out.println("Setting up learner");
|
||||||
System.out.println("Setting up learner(s)");
|
LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner = null;
|
||||||
ExtensibleLStarMealy<String, String> learnerLStar = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST);
|
switch (learnAlgorithm){
|
||||||
TTTLearnerMealy<String, String> learnerTTT = new TTTLearnerMealy<>(alphabet, mOracleForLearning, LocalSuffixFinders.FIND_LINEAR);
|
case LStar:
|
||||||
KearnsVaziraniMealy<String, String> learnerKV = new KearnsVaziraniMealy<>(alphabet, mOracleForLearning, false, AcexAnalyzers.BINARY_SEARCH);
|
learner = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_SHORTEST);
|
||||||
|
break;
|
||||||
// The chosen learning algorithm
|
case RivestSchapire:
|
||||||
LearningAlgorithm<MealyMachine<?, String, ?, String>, String, Word<String>> learner = learnerLStar;
|
learner = new ExtensibleLStarMealy<>(alphabet, mOracleForLearning, Lists.<Word<String>>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
|
// 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();
|
learner.startLearning();
|
||||||
|
|
||||||
while(true) {
|
while(true) {
|
||||||
// String dir = "/Users/joshua/Documents/PhD/Machines/Mealy/esms3/";
|
if(saveAllHypotheses) {
|
||||||
// String filenameh = dir + "hyp." + stage + ".obf.dot";
|
String dir = "/Users/joshua/Documents/PhD/Machines/Mealy/esms3/";
|
||||||
// PrintWriter output = new PrintWriter(filenameh);
|
String filename = dir + "hyp." + stage + ".obf.dot";
|
||||||
// GraphDOT.write(learner.getHypothesisModel(), alphabet, output);
|
PrintWriter output = new PrintWriter(filename);
|
||||||
// output.close();
|
GraphDOT.write(learner.getHypothesisModel(), alphabet, output);
|
||||||
|
output.close();
|
||||||
|
}
|
||||||
|
|
||||||
System.out.println(stage++ + ": " + Calendar.getInstance().getTime());
|
System.out.println(stage++ + ": " + Calendar.getInstance().getTime());
|
||||||
System.out.println("Hypothesis: " + learner.getHypothesisModel().getStates().size());
|
System.out.println("Hypothesis: " + learner.getHypothesisModel().getStates().size());
|
||||||
|
|
Loading…
Add table
Reference in a new issue