joshua/hybrid-ads
1
Fork 0
mirror of https://github.com/Jaxan/hybrid-ads.git synced 2025-04-27 23:17:44 +02:00
Code Issues Releases Activity

java: Buffers queries to enable parallelism

Browse source
This commit is contained in:
Joshua Moerman 2015-04-08 17:03:07 +02:00
parent 7817edbb90
commit 1033d8e74e
2 changed files with 71 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
java/Main.java
View file

@ -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<String, String> mOracleMealy = new SimulatorOracle.MealySimulatorOracle<>(fm);
CountingQueryOracle<String, Word<String>> mOracleCounting1 = new CountingQueryOracle<>(mOracleMealy);
CountingQueryOracle<String, Word<String>> mOracleCounting2 = new CountingQueryOracle<>(mOracleMealy);
DynamicParallelOracle<String, Word<String>> 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<String, String> eqOracleMealy = new SimulatorEQOracle.MealySimulatorEQOracle<>(fm);
WpMethodEQOracle.MealyWpMethodEQOracle<String, String> eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mOracleCounting2);
WMethodEQOracle.MealyWMethodEQOracle<String, String> eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mOracleCounting2);
EquivalenceOracle.MealyEquivalenceOracle<String, String> eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mOracleCounting2);
EquivalenceOracle.MealyEquivalenceOracle<String, String> eqOracleSpecific = new SpecificCounterExampleOracle(mOracleCounting2);
EQOracleChain.MealyEQOracleChain eqOracleYannakakisPlus = new EQOracleChain.MealyEQOracleChain(Arrays.asList(eqOracleSpecific, eqOracleYannakakis));
WpMethodEQOracle.MealyWpMethodEQOracle<String, String> eqOracleWp = new WpMethodEQOracle.MealyWpMethodEQOracle<>(3, mParallelOracle);
WMethodEQOracle.MealyWMethodEQOracle<String, String> eqOracleW = new WMethodEQOracle.MealyWMethodEQOracle<>(2, mParallelOracle);
EquivalenceOracle.MealyEquivalenceOracle<String, String> eqOracleYannakakis = new YannakakisEQOracle<>(alphabets, mParallelOracle);
// The chosen oracle to experiment with.
EquivalenceOracle.MealyEquivalenceOracle<String, String> eqOracle = eqOracleYannakakis;
@ -77,8 +83,8 @@ public class Main {
// Learnlib comes with different learning algorithms
System.out.println("Setting up learner(s)");
MealyDHC<String, String> learnerDHC = new MealyDHC<>(alphabet, mOracleCounting1);
ExtensibleLStarMealy<String, String> learnerLStar = new ExtensibleLStarMealy<>(alphabet, mOracleCounting1, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_FIRST);
MealyDHC<String, String> learnerDHC = new MealyDHC<>(alphabet, mParallelOracle);
ExtensibleLStarMealy<String, String> learnerLStar = new ExtensibleLStarMealy<>(alphabet, mParallelOracle, Lists.<Word<String>>newArrayList(), ObservationTableCEXHandlers.CLASSIC_LSTAR, ClosingStrategies.CLOSE_FIRST);
// The chosen learning algorithm
LearningAlgorithm.MealyLearner<String, String> 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<String, String> {
private final MembershipOracle<String, Word<String>> sulOracle;
private boolean fired = false;
SpecificCounterExampleOracle(MembershipOracle<String, Word<String>> sulOracle){
this.sulOracle = sulOracle;
}
@Nullable
@Override
public DefaultQuery<String, Word<String>> findCounterExample(MealyMachine<?, String, ?, String> objects, Collection<? extends String> collection) {
if(fired) return null;
WordBuilder<String> 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<String> test = wb.toWord();
DefaultQuery<String, Word<String>> query = new DefaultQuery<>(test);
sulOracle.processQueries(Collections.singleton(query));
fired = true;
return query;
}
}
}

84
java/YannakakisEQOracle.java
View file

@ -23,10 +23,15 @@ import java.util.*;
public class YannakakisEQOracle<O> implements EquivalenceOracle.MealyEquivalenceOracle<String, O> {
private final MembershipOracle<String, Word<O>> sulOracle;
private final List<Alphabet<String>> 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<DefaultQuery<String, Word<O>>> buffer = new ArrayList<>(bufferSize);
private Process process;
private Writer processInput;
@ -41,7 +46,6 @@ public class YannakakisEQOracle<O> implements EquivalenceOracle.MealyEquivalence
YannakakisEQOracle(List<Alphabet<String>> alphabets, MembershipOracle<String, Word<O>> 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<O> 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<String> a = alphabets.get(currentAlphabet);
DefaultQuery<String, Word<O>> 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<O> 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<String> wb = new WordBuilder<>();
Scanner s = new Scanner(line);
@ -166,21 +170,24 @@ public class YannakakisEQOracle<O> implements EquivalenceOracle.MealyEquivalence
// Convert to a word and test on the SUL
Word<String> test = wb.toWord();
DefaultQuery<String, Word<O>> query = new DefaultQuery<>(test);
sulOracle.processQueries(Collections.singleton(query));
buffer.add(query);
// Also test on the hypothesis
Word<O> o1 = machine.computeOutput(test);
Word<O> 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<String, Word<O>> 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<O> implements EquivalenceOracle.MealyEquivalence
// Here, the program exited normally, without counterexample, so we may return null.
return null;
}
private DefaultQuery<String, Word<O>> checkAndEmptyBuffer(MealyMachine<?, String, ?, O> machine){
sulOracle.processQueries(buffer);
DefaultQuery<String, Word<O>> r = inspectBuffer(machine);
buffer.clear();
return r;
}
private DefaultQuery<String, Word<O>> inspectBuffer(MealyMachine<?, String, ?, O> machine){
for(DefaultQuery<String, Word<O>> query : buffer){
Word<O> o1 = machine.computeOutput(query.getInput());
Word<O> o2 = query.getOutput();
assert o1 != null;
assert o2 != null;
// If equal => no counterexample :(
if(!o1.equals(o2)) return query;
}
return null;
}
}