From 857fc5c5d4034d27f8b49a8b6f5055f63bbb1061 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 29 Aug 2016 13:16:14 +0200 Subject: [PATCH 1/2] Adds two randomized equivalence oracles based on the W method Maybe it is a good time to add better support for testing oracles --- .../learnlib/eqtests/basic/RandomWMethod.java | 129 +++++++++++++++ .../eqtests/basic/RandomWpMethod.java | 148 ++++++++++++++++++ 2 files changed, 277 insertions(+) create mode 100644 eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java create mode 100644 eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java diff --git a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java new file mode 100644 index 0000000000..b62e3cdd42 --- /dev/null +++ b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java @@ -0,0 +1,129 @@ +package learnlib; + +import de.learnlib.api.EquivalenceOracle; +import de.learnlib.api.MembershipOracle; +import de.learnlib.oracles.DefaultQuery; +import net.automatalib.automata.UniversalDeterministicAutomaton; +import net.automatalib.automata.concepts.Output; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; + +import javax.annotation.ParametersAreNonnullByDefault; +import java.util.*; + +/** + * Implements an equivalence test by applying the W-method test on the given hypothesis automaton. + * Generally the Wp-method performs better in finding counter examples. + * Instead of enumerating the test suite in order, this is a sampling implementation: + * 1. sample uniformly from the states for a prefix + * 2. sample geometrically a random word + * 3. sample a word from the set of suffixes / state identifiers + * There are two parameters: minimalSize determines the minimal size of the random word, this is + * useful when one first performs a W(p)-method with some depth and continue with this randomized + * tester from that depth onward. The second parameter rndLength determines the expected length + * of the random word. (The expected length in effect is minimalSize + rndLength.) + * In the unbounded case it will not terminate for a correct hypothesis. + * + * @param automaton type + * @param input symbol type + * @param output domain type + * @author Joshua Moerman + */ +public class RandomWMethod & Output, I, D> + implements EquivalenceOracle { + private final MembershipOracle sulOracle; + private final int minimalSize; + private final int rndLength; + private final int bound; + + /** + * Constructor for an unbounded testing oracle + * + * @param sulOracle oracle which answers tests. + * @param minimalSize minimal size of the random word + * @param rndLength expected length (in addition to minimalSize) of random word + */ + public RandomWMethod(MembershipOracle sulOracle, int minimalSize, int rndLength) { + this.sulOracle = sulOracle; + this.minimalSize = minimalSize; + this.rndLength = rndLength; + this.bound = 0; + } + + /** + * Constructor for a bounded testing oracle + * + * @param sulOracle oracle which answers tests. + * @param minimalSize minimal size of the random word + * @param rndLength expected length (in addition to minimalSize) of random word + * @param bound specifies the bound (set to 0 for unbounded). + */ + public RandomWMethod(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { + this.sulOracle = sulOracle; + this.minimalSize = minimalSize; + this.rndLength = rndLength; + this.bound = bound; + } + + /* + * (non-Javadoc) + * @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection) + */ + @Override + @ParametersAreNonnullByDefault + public DefaultQuery findCounterExample(A hypothesis, Collection inputs) { + UniversalDeterministicAutomaton aut = hypothesis; + Output out = hypothesis; + return doFindCounterExample(aut, out, inputs); + } + + /* + * Delegate target, used to bind the state-parameter of the automaton + */ + private DefaultQuery doFindCounterExample(UniversalDeterministicAutomaton hypothesis, + Output output, Collection inputs) { + // Note that we want to use ArrayLists because we want constant time random access + // We will sample from this for a prefix + ArrayList> stateCover = new ArrayList<>(hypothesis.size()); + Automata.cover(hypothesis, inputs, stateCover, null); + + // Then repeatedly from this for a random word + ArrayList arrayAlphabet = new ArrayList<>(inputs); + + // Finally we test the state with a suffix + ArrayList> globalSuffixes = new ArrayList<>(); + Automata.characterizingSet(hypothesis, inputs, globalSuffixes); + + Random rand = new Random(); + int currentBound = bound; + while (bound == 0 || currentBound-- > 0) { + WordBuilder wb = new WordBuilder<>(minimalSize + rndLength + 1); + + // pick a random state + wb.append(stateCover.get(rand.nextInt(stateCover.size()))); + + // construct random middle part (of some expected length) + int size = minimalSize; + while ((size > 0) || (rand.nextDouble() > 1 / (rndLength + 1.0))) { + wb.append(arrayAlphabet.get(rand.nextInt(arrayAlphabet.size()))); + if (size > 0) size--; + } + + // pick a random suffix for this state + if (!globalSuffixes.isEmpty()) { + wb.append(globalSuffixes.get(rand.nextInt(globalSuffixes.size()))); + } + + Word queryWord = wb.toWord(); + DefaultQuery query = new DefaultQuery<>(queryWord); + D hypOutput = output.computeOutput(queryWord); + sulOracle.processQueries(Collections.singleton(query)); + if (!Objects.equals(hypOutput, query.getOutput())) + return query; + } + + // no counter example found within the bound + return null; + } +} diff --git a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java new file mode 100644 index 0000000000..4058eb1d97 --- /dev/null +++ b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java @@ -0,0 +1,148 @@ +package learnlib; + +import de.learnlib.api.EquivalenceOracle; +import de.learnlib.api.MembershipOracle; +import de.learnlib.oracles.DefaultQuery; +import net.automatalib.automata.UniversalDeterministicAutomaton; +import net.automatalib.automata.concepts.Output; +import net.automatalib.commons.util.mappings.MutableMapping; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; + +import javax.annotation.ParametersAreNonnullByDefault; +import java.util.*; + +/** + * Implements an equivalence test by applying the Wp-method test on the given hypothesis automaton, + * as described in "Test Selection Based on Finite State Models" by S. Fujiwara et al. + * Instead of enumerating the test suite in order, this is a sampling implementation: + * 1. sample uniformly from the states for a prefix + * 2. sample geometrically a random word + * 3. sample a word from the set of suffixes / state identifiers (either local or global) + * There are two parameters: minimalSize determines the minimal size of the random word, this is + * useful when one first performs a W(p)-method with some depth and continue with this randomized + * tester from that depth onward. The second parameter rndLength determines the expected length + * of the random word. (The expected length in effect is minimalSize + rndLength.) + * In the unbounded case it will not terminate for a correct hypothesis. + * + * @param automaton type + * @param input symbol type + * @param output domain type + * @author Joshua Moerman + */ +public class RandomWpMethod & Output, I, D> + implements EquivalenceOracle { + private final MembershipOracle sulOracle; + private final int minimalSize; + private final int rndLength; + private final int bound; + + /** + * Constructor for an unbounded testing oracle + * + * @param sulOracle oracle which answers tests. + * @param minimalSize minimal size of the random word + * @param rndLength expected length (in addition to minimalSize) of random word + */ + public RandomWpMethod(MembershipOracle sulOracle, int minimalSize, int rndLength) { + this.sulOracle = sulOracle; + this.minimalSize = minimalSize; + this.rndLength = rndLength; + this.bound = 0; + } + + /** + * Constructor for a bounded testing oracle + * + * @param sulOracle oracle which answers tests. + * @param minimalSize minimal size of the random word + * @param rndLength expected length (in addition to minimalSize) of random word + * @param bound specifies the bound (set to 0 for unbounded). + */ + public RandomWpMethod(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { + this.sulOracle = sulOracle; + this.minimalSize = minimalSize; + this.rndLength = rndLength; + this.bound = bound; + } + + /* + * (non-Javadoc) + * @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection) + */ + @Override + @ParametersAreNonnullByDefault + public DefaultQuery findCounterExample(A hypothesis, Collection inputs) { + UniversalDeterministicAutomaton aut = hypothesis; + Output out = hypothesis; + return doFindCounterExample(aut, out, inputs); + } + + /* + * Delegate target, used to bind the state-parameter of the automaton + */ + private DefaultQuery doFindCounterExample(UniversalDeterministicAutomaton hypothesis, + Output output, Collection inputs) { + // Note that we want to use ArrayLists because we want constant time random access + // We will sample from this for a prefix + ArrayList> stateCover = new ArrayList<>(hypothesis.size()); + Automata.cover(hypothesis, inputs, stateCover, null); + + // Then repeatedly from this for a random word + ArrayList arrayAlphabet = new ArrayList<>(inputs); + + // Finally we test the state with a suffix, sometimes a global one, sometimes local + ArrayList> globalSuffixes = new ArrayList<>(); + Automata.characterizingSet(hypothesis, inputs, globalSuffixes); + + MutableMapping>> localSuffixSets = hypothesis.createStaticStateMapping(); + for (S state : hypothesis.getStates()) { + ArrayList> suffixSet = new ArrayList<>(); + Automata.stateCharacterizingSet(hypothesis, inputs, state, suffixSet); + localSuffixSets.put(state, suffixSet); + } + + Random rand = new Random(); + int currentBound = bound; + while (bound == 0 || currentBound-- > 0) { + WordBuilder wb = new WordBuilder<>(minimalSize + rndLength + 1); + + // pick a random state + wb.append(stateCover.get(rand.nextInt(stateCover.size()))); + + // construct random middle part (of some expected length) + int size = minimalSize; + while ((size > 0) || (rand.nextDouble() > 1 / (rndLength + 1.0))) { + wb.append(arrayAlphabet.get(rand.nextInt(arrayAlphabet.size()))); + if (size > 0) size--; + } + + // pick a random suffix for this state + // 50% chance for state testing, 50% chance for transition testing + if (rand.nextBoolean()) { + // global + if (!globalSuffixes.isEmpty()) { + wb.append(globalSuffixes.get(rand.nextInt(globalSuffixes.size()))); + } + } else { + // local + S state2 = hypothesis.getState(wb); + ArrayList> localSuffixes = localSuffixSets.get(state2); + if (!localSuffixes.isEmpty()) { + wb.append(localSuffixes.get(rand.nextInt(localSuffixes.size()))); + } + } + + Word queryWord = wb.toWord(); + DefaultQuery query = new DefaultQuery<>(queryWord); + D hypOutput = output.computeOutput(queryWord); + sulOracle.processQueries(Collections.singleton(query)); + if (!Objects.equals(hypOutput, query.getOutput())) + return query; + } + + // no counter example found within the bound + return null; + } +} From 6f8ea2ff929e412ff44dbfeda6183a79574ffb6b Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 27 Oct 2016 10:05:01 +0200 Subject: [PATCH 2/2] Renamed the oracles to be consistent with current style. --- .../{RandomWMethod.java => RandomWMethodEQOracle.java} | 8 ++++---- .../{RandomWpMethod.java => RandomWpMethodEQOracle.java} | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) rename eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/{RandomWMethod.java => RandomWMethodEQOracle.java} (93%) rename eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/{RandomWpMethod.java => RandomWpMethodEQOracle.java} (94%) diff --git a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethodEQOracle.java similarity index 93% rename from eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java rename to eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethodEQOracle.java index b62e3cdd42..6a2585b2c6 100644 --- a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethod.java +++ b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethodEQOracle.java @@ -1,4 +1,4 @@ -package learnlib; +package de.learnlib.eqtests.basic; import de.learnlib.api.EquivalenceOracle; import de.learnlib.api.MembershipOracle; @@ -30,7 +30,7 @@ * @param output domain type * @author Joshua Moerman */ -public class RandomWMethod & Output, I, D> +public class RandomWMethodEQOracle & Output, I, D> implements EquivalenceOracle { private final MembershipOracle sulOracle; private final int minimalSize; @@ -44,7 +44,7 @@ public class RandomWMethod sulOracle, int minimalSize, int rndLength) { + public RandomWMethodEQOracle(MembershipOracle sulOracle, int minimalSize, int rndLength) { this.sulOracle = sulOracle; this.minimalSize = minimalSize; this.rndLength = rndLength; @@ -59,7 +59,7 @@ public RandomWMethod(MembershipOracle sulOracle, int minimalSize, int rndL * @param rndLength expected length (in addition to minimalSize) of random word * @param bound specifies the bound (set to 0 for unbounded). */ - public RandomWMethod(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { + public RandomWMethodEQOracle(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { this.sulOracle = sulOracle; this.minimalSize = minimalSize; this.rndLength = rndLength; diff --git a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethodEQOracle.java similarity index 94% rename from eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java rename to eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethodEQOracle.java index 4058eb1d97..d19a11446d 100644 --- a/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethod.java +++ b/eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethodEQOracle.java @@ -1,4 +1,4 @@ -package learnlib; +package de.learnlib.eqtests.basic; import de.learnlib.api.EquivalenceOracle; import de.learnlib.api.MembershipOracle; @@ -31,7 +31,7 @@ * @param output domain type * @author Joshua Moerman */ -public class RandomWpMethod & Output, I, D> +public class RandomWpMethodEQOracle & Output, I, D> implements EquivalenceOracle { private final MembershipOracle sulOracle; private final int minimalSize; @@ -45,7 +45,7 @@ public class RandomWpMethod sulOracle, int minimalSize, int rndLength) { + public RandomWpMethodEQOracle(MembershipOracle sulOracle, int minimalSize, int rndLength) { this.sulOracle = sulOracle; this.minimalSize = minimalSize; this.rndLength = rndLength; @@ -60,7 +60,7 @@ public RandomWpMethod(MembershipOracle sulOracle, int minimalSize, int rnd * @param rndLength expected length (in addition to minimalSize) of random word * @param bound specifies the bound (set to 0 for unbounded). */ - public RandomWpMethod(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { + public RandomWpMethodEQOracle(MembershipOracle sulOracle, int minimalSize, int rndLength, int bound) { this.sulOracle = sulOracle; this.minimalSize = minimalSize; this.rndLength = rndLength;