Skip to content

Commit 7dabaf2

Browse files
abainczykabainczyk
authored
Merge pull request #40 from Jaxan/randomized-eq-oracles
Adds two randomized equivalence oracles based on the W method
2 parents 63faed6 + 6f8ea2f commit 7dabaf2

File tree

2 files changed

+277
-0
lines changed

2 files changed

+277
-0
lines changed

‎eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWMethodEQOracle.java

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
package de.learnlib.eqtests.basic;
2+
3+
import de.learnlib.api.EquivalenceOracle;
4+
import de.learnlib.api.MembershipOracle;
5+
import de.learnlib.oracles.DefaultQuery;
6+
import net.automatalib.automata.UniversalDeterministicAutomaton;
7+
import net.automatalib.automata.concepts.Output;
8+
import net.automatalib.util.automata.Automata;
9+
import net.automatalib.words.Word;
10+
import net.automatalib.words.WordBuilder;
11+
12+
import javax.annotation.ParametersAreNonnullByDefault;
13+
import java.util.*;
14+
15+
/**
16+
* Implements an equivalence test by applying the W-method test on the given hypothesis automaton.
17+
* Generally the Wp-method performs better in finding counter examples.
18+
* Instead of enumerating the test suite in order, this is a sampling implementation:
19+
* 1. sample uniformly from the states for a prefix
20+
* 2. sample geometrically a random word
21+
* 3. sample a word from the set of suffixes / state identifiers
22+
* There are two parameters: minimalSize determines the minimal size of the random word, this is
23+
* useful when one first performs a W(p)-method with some depth and continue with this randomized
24+
* tester from that depth onward. The second parameter rndLength determines the expected length
25+
* of the random word. (The expected length in effect is minimalSize + rndLength.)
26+
* In the unbounded case it will not terminate for a correct hypothesis.
27+
*
28+
* @param <A> automaton type
29+
* @param <I> input symbol type
30+
* @param <D> output domain type
31+
* @author Joshua Moerman
32+
*/
33+
public class RandomWMethodEQOracle<A extends UniversalDeterministicAutomaton<?, I, ?, ?, ?> & Output<I, D>, I, D>
34+
implements EquivalenceOracle<A, I, D> {
35+
private final MembershipOracle<I, D> sulOracle;
36+
private final int minimalSize;
37+
private final int rndLength;
38+
private final int bound;
39+
40+
/**
41+
* Constructor for an unbounded testing oracle
42+
*
43+
* @param sulOracle oracle which answers tests.
44+
* @param minimalSize minimal size of the random word
45+
* @param rndLength expected length (in addition to minimalSize) of random word
46+
*/
47+
public RandomWMethodEQOracle(MembershipOracle<I, D> sulOracle, int minimalSize, int rndLength) {
48+
this.sulOracle = sulOracle;
49+
this.minimalSize = minimalSize;
50+
this.rndLength = rndLength;
51+
this.bound = 0;
52+
}
53+
54+
/**
55+
* Constructor for a bounded testing oracle
56+
*
57+
* @param sulOracle oracle which answers tests.
58+
* @param minimalSize minimal size of the random word
59+
* @param rndLength expected length (in addition to minimalSize) of random word
60+
* @param bound specifies the bound (set to 0 for unbounded).
61+
*/
62+
public RandomWMethodEQOracle(MembershipOracle<I, D> sulOracle, int minimalSize, int rndLength, int bound) {
63+
this.sulOracle = sulOracle;
64+
this.minimalSize = minimalSize;
65+
this.rndLength = rndLength;
66+
this.bound = bound;
67+
}
68+
69+
/*
70+
* (non-Javadoc)
71+
* @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection)
72+
*/
73+
@Override
74+
@ParametersAreNonnullByDefault
75+
public DefaultQuery<I, D> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
76+
UniversalDeterministicAutomaton<?, I, ?, ?, ?> aut = hypothesis;
77+
Output<I, D> out = hypothesis;
78+
return doFindCounterExample(aut, out, inputs);
79+
}
80+
81+
/*
82+
* Delegate target, used to bind the state-parameter of the automaton
83+
*/
84+
private <S> DefaultQuery<I, D> doFindCounterExample(UniversalDeterministicAutomaton<S, I, ?, ?, ?> hypothesis,
85+
Output<I, D> output, Collection<? extends I> inputs) {
86+
// Note that we want to use ArrayLists because we want constant time random access
87+
// We will sample from this for a prefix
88+
ArrayList<Word<I>> stateCover = new ArrayList<>(hypothesis.size());
89+
Automata.cover(hypothesis, inputs, stateCover, null);
90+
91+
// Then repeatedly from this for a random word
92+
ArrayList<I> arrayAlphabet = new ArrayList<>(inputs);
93+
94+
// Finally we test the state with a suffix
95+
ArrayList<Word<I>> globalSuffixes = new ArrayList<>();
96+
Automata.characterizingSet(hypothesis, inputs, globalSuffixes);
97+
98+
Random rand = new Random();
99+
int currentBound = bound;
100+
while (bound == 0 || currentBound-- > 0) {
101+
WordBuilder<I> wb = new WordBuilder<>(minimalSize + rndLength + 1);
102+
103+
// pick a random state
104+
wb.append(stateCover.get(rand.nextInt(stateCover.size())));
105+
106+
// construct random middle part (of some expected length)
107+
int size = minimalSize;
108+
while ((size > 0) || (rand.nextDouble() > 1 / (rndLength + 1.0))) {
109+
wb.append(arrayAlphabet.get(rand.nextInt(arrayAlphabet.size())));
110+
if (size > 0) size--;
111+
}
112+
113+
// pick a random suffix for this state
114+
if (!globalSuffixes.isEmpty()) {
115+
wb.append(globalSuffixes.get(rand.nextInt(globalSuffixes.size())));
116+
}
117+
118+
Word<I> queryWord = wb.toWord();
119+
DefaultQuery<I, D> query = new DefaultQuery<>(queryWord);
120+
D hypOutput = output.computeOutput(queryWord);
121+
sulOracle.processQueries(Collections.singleton(query));
122+
if (!Objects.equals(hypOutput, query.getOutput()))
123+
return query;
124+
}
125+
126+
// no counter example found within the bound
127+
return null;
128+
}
129+
}

‎eqtests/basic-eqtests/src/main/java/de/learnlib/eqtests/basic/RandomWpMethodEQOracle.java

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
package de.learnlib.eqtests.basic;
2+
3+
import de.learnlib.api.EquivalenceOracle;
4+
import de.learnlib.api.MembershipOracle;
5+
import de.learnlib.oracles.DefaultQuery;
6+
import net.automatalib.automata.UniversalDeterministicAutomaton;
7+
import net.automatalib.automata.concepts.Output;
8+
import net.automatalib.commons.util.mappings.MutableMapping;
9+
import net.automatalib.util.automata.Automata;
10+
import net.automatalib.words.Word;
11+
import net.automatalib.words.WordBuilder;
12+
13+
import javax.annotation.ParametersAreNonnullByDefault;
14+
import java.util.*;
15+
16+
/**
17+
* Implements an equivalence test by applying the Wp-method test on the given hypothesis automaton,
18+
* as described in "Test Selection Based on Finite State Models" by S. Fujiwara et al.
19+
* Instead of enumerating the test suite in order, this is a sampling implementation:
20+
* 1. sample uniformly from the states for a prefix
21+
* 2. sample geometrically a random word
22+
* 3. sample a word from the set of suffixes / state identifiers (either local or global)
23+
* There are two parameters: minimalSize determines the minimal size of the random word, this is
24+
* useful when one first performs a W(p)-method with some depth and continue with this randomized
25+
* tester from that depth onward. The second parameter rndLength determines the expected length
26+
* of the random word. (The expected length in effect is minimalSize + rndLength.)
27+
* In the unbounded case it will not terminate for a correct hypothesis.
28+
*
29+
* @param <A> automaton type
30+
* @param <I> input symbol type
31+
* @param <D> output domain type
32+
* @author Joshua Moerman
33+
*/
34+
public class RandomWpMethodEQOracle<A extends UniversalDeterministicAutomaton<?, I, ?, ?, ?> & Output<I, D>, I, D>
35+
implements EquivalenceOracle<A, I, D> {
36+
private final MembershipOracle<I, D> sulOracle;
37+
private final int minimalSize;
38+
private final int rndLength;
39+
private final int bound;
40+
41+
/**
42+
* Constructor for an unbounded testing oracle
43+
*
44+
* @param sulOracle oracle which answers tests.
45+
* @param minimalSize minimal size of the random word
46+
* @param rndLength expected length (in addition to minimalSize) of random word
47+
*/
48+
public RandomWpMethodEQOracle(MembershipOracle<I, D> sulOracle, int minimalSize, int rndLength) {
49+
this.sulOracle = sulOracle;
50+
this.minimalSize = minimalSize;
51+
this.rndLength = rndLength;
52+
this.bound = 0;
53+
}
54+
55+
/**
56+
* Constructor for a bounded testing oracle
57+
*
58+
* @param sulOracle oracle which answers tests.
59+
* @param minimalSize minimal size of the random word
60+
* @param rndLength expected length (in addition to minimalSize) of random word
61+
* @param bound specifies the bound (set to 0 for unbounded).
62+
*/
63+
public RandomWpMethodEQOracle(MembershipOracle<I, D> sulOracle, int minimalSize, int rndLength, int bound) {
64+
this.sulOracle = sulOracle;
65+
this.minimalSize = minimalSize;
66+
this.rndLength = rndLength;
67+
this.bound = bound;
68+
}
69+
70+
/*
71+
* (non-Javadoc)
72+
* @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection)
73+
*/
74+
@Override
75+
@ParametersAreNonnullByDefault
76+
public DefaultQuery<I, D> findCounterExample(A hypothesis, Collection<? extends I> inputs) {
77+
UniversalDeterministicAutomaton<?, I, ?, ?, ?> aut = hypothesis;
78+
Output<I, D> out = hypothesis;
79+
return doFindCounterExample(aut, out, inputs);
80+
}
81+
82+
/*
83+
* Delegate target, used to bind the state-parameter of the automaton
84+
*/
85+
private <S> DefaultQuery<I, D> doFindCounterExample(UniversalDeterministicAutomaton<S, I, ?, ?, ?> hypothesis,
86+
Output<I, D> output, Collection<? extends I> inputs) {
87+
// Note that we want to use ArrayLists because we want constant time random access
88+
// We will sample from this for a prefix
89+
ArrayList<Word<I>> stateCover = new ArrayList<>(hypothesis.size());
90+
Automata.cover(hypothesis, inputs, stateCover, null);
91+
92+
// Then repeatedly from this for a random word
93+
ArrayList<I> arrayAlphabet = new ArrayList<>(inputs);
94+
95+
// Finally we test the state with a suffix, sometimes a global one, sometimes local
96+
ArrayList<Word<I>> globalSuffixes = new ArrayList<>();
97+
Automata.characterizingSet(hypothesis, inputs, globalSuffixes);
98+
99+
MutableMapping<S, ArrayList<Word<I>>> localSuffixSets = hypothesis.createStaticStateMapping();
100+
for (S state : hypothesis.getStates()) {
101+
ArrayList<Word<I>> suffixSet = new ArrayList<>();
102+
Automata.stateCharacterizingSet(hypothesis, inputs, state, suffixSet);
103+
localSuffixSets.put(state, suffixSet);
104+
}
105+
106+
Random rand = new Random();
107+
int currentBound = bound;
108+
while (bound == 0 || currentBound-- > 0) {
109+
WordBuilder<I> wb = new WordBuilder<>(minimalSize + rndLength + 1);
110+
111+
// pick a random state
112+
wb.append(stateCover.get(rand.nextInt(stateCover.size())));
113+
114+
// construct random middle part (of some expected length)
115+
int size = minimalSize;
116+
while ((size > 0) || (rand.nextDouble() > 1 / (rndLength + 1.0))) {
117+
wb.append(arrayAlphabet.get(rand.nextInt(arrayAlphabet.size())));
118+
if (size > 0) size--;
119+
}
120+
121+
// pick a random suffix for this state
122+
// 50% chance for state testing, 50% chance for transition testing
123+
if (rand.nextBoolean()) {
124+
// global
125+
if (!globalSuffixes.isEmpty()) {
126+
wb.append(globalSuffixes.get(rand.nextInt(globalSuffixes.size())));
127+
}
128+
} else {
129+
// local
130+
S state2 = hypothesis.getState(wb);
131+
ArrayList<Word<I>> localSuffixes = localSuffixSets.get(state2);
132+
if (!localSuffixes.isEmpty()) {
133+
wb.append(localSuffixes.get(rand.nextInt(localSuffixes.size())));
134+
}
135+
}
136+
137+
Word<I> queryWord = wb.toWord();
138+
DefaultQuery<I, D> query = new DefaultQuery<>(queryWord);
139+
D hypOutput = output.computeOutput(queryWord);
140+
sulOracle.processQueries(Collections.singleton(query));
141+
if (!Objects.equals(hypOutput, query.getOutput()))
142+
return query;
143+
}
144+
145+
// no counter example found within the bound
146+
return null;
147+
}
148+
}

0 commit comments

Comments
 (0)