Skip to content

Commit 88d7cb1

Browse files
mtf90mtf90
authored
Add equivalence oracles based on k-way state/transition coverage (#156)
* initial work on kWayOracles * cleanups * adjust to AutomataLib + consolidations * adjust to upstream changes * reorder attributes * test the correct oracle * hide some type variables * add additional documentation * cleanups * adjust configs * declutter type information * do not use special characters in documentation
1 parent f278465 commit 88d7cb1

5 files changed

Lines changed: 448 additions & 0 deletions

File tree

‎build-parent/pom.xml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ limitations under the License.
6262

6363
<!-- generated builders for reuse trees/oracles -->
6464
<exclude>de/learnlib/filter/reuse/**/Reuse*Builder.class</exclude>
65+
<exclude>de/learnlib/oracle/equivalence/KWay*Builder.class</exclude>
6566

6667
<!-- generated refinements for oracles -->
6768
<exclude>de/learnlib/filter/cache/**/*Interning*.class</exclude>

‎oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/KWayStateCoverEQOracle.java‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.oracle.equivalence;
17+
18+
import java.util.Collection;
19+
import java.util.Random;
20+
import java.util.stream.Stream;
21+
22+
import de.learnlib.oracle.EquivalenceOracle;
23+
import de.learnlib.oracle.MembershipOracle;
24+
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
25+
import net.automatalib.automaton.DeterministicAutomaton;
26+
import net.automatalib.automaton.concept.Output;
27+
import net.automatalib.common.util.collection.IteratorUtil;
28+
import net.automatalib.util.automaton.conformance.KWayStateCoverTestsIterator;
29+
import net.automatalib.util.automaton.conformance.KWayStateCoverTestsIterator.CombinationMethod;
30+
import net.automatalib.word.Word;
31+
32+
/**
33+
* An {@link EquivalenceOracle} based on the concepts of mutation testing as described in the paper <a
34+
* href="https://doi.org/10.1007/978-3-319-57288-8_2">Learning from Faults: Mutation Testing in Active Automata
35+
* Learning</a> by Bernhard K. Aichernig and Martin Tappler.
36+
* <p>
37+
* A test case will be computed for every k-combination or k-permutation of states with additional random walk at the
38+
* end.
39+
* <p>
40+
* <b>Implementation detail:</b> Note that this test generator heavily relies on the sampling of states. If the given
41+
* automaton has very few or very many states, the number of generated test cases may be very low or high, respectively.
42+
* As a result, it may be advisable to {@link EQOracleChain combine} this generator with other generators or limit the
43+
* number of generated test cases.
44+
*
45+
* @param <A>
46+
* automaton type
47+
* @param <I>
48+
* input symbol type
49+
* @param <D>
50+
* output domain
51+
*
52+
* @see KWayStateCoverTestsIterator
53+
*/
54+
public class KWayStateCoverEQOracle<A extends DeterministicAutomaton<?, I, ?> & Output<I, D>, I, D>
55+
extends AbstractTestWordEQOracle<A, I, D> {
56+
57+
private final Random random;
58+
private final int randomWalkLen;
59+
private final int k;
60+
private final CombinationMethod combinationMethod;
61+
62+
/**
63+
* Constructor.
64+
*
65+
* @param oracle
66+
* the oracle for accessing the system under learning
67+
* @param random
68+
* the random number generator to use
69+
* @param randomWalkLen
70+
* length of random walk performed at the end of each combination/permutation
71+
* @param k
72+
* k value used for k-wise combinations/permutations of states
73+
* @param combinationMethod
74+
* the method for computing combinations
75+
* @param batchSize
76+
* size of the batches sent to the membership oracle
77+
*
78+
* @see KWayStateCoverTestsIterator#KWayStateCoverTestsIterator(DeterministicAutomaton, Collection, Random, int,
79+
* int, CombinationMethod)
80+
*/
81+
@GenerateBuilder(defaults = BuilderDefaults.class)
82+
public KWayStateCoverEQOracle(MembershipOracle<I, D> oracle,
83+
Random random,
84+
int randomWalkLen,
85+
int k,
86+
CombinationMethod combinationMethod,
87+
int batchSize) {
88+
super(oracle, batchSize);
89+
this.random = random;
90+
this.randomWalkLen = randomWalkLen;
91+
this.k = k;
92+
this.combinationMethod = combinationMethod;
93+
}
94+
95+
@Override
96+
public Stream<Word<I>> generateTestWords(A hypothesis, Collection<? extends I> inputs) {
97+
final DeterministicAutomaton<?, I, ?> casted = hypothesis;
98+
return doGenerateTestWords(casted, inputs, this.random, this.randomWalkLen, this.k, this.combinationMethod);
99+
}
100+
101+
private static <A extends DeterministicAutomaton<S, I, ?>, S, I> Stream<Word<I>> doGenerateTestWords(A hypothesis,
102+
Collection<? extends I> inputs,
103+
Random random,
104+
int randomWalkLen,
105+
int k,
106+
CombinationMethod combinationMethod) {
107+
return IteratorUtil.stream(new KWayStateCoverTestsIterator<>(hypothesis,
108+
inputs,
109+
random,
110+
randomWalkLen,
111+
k,
112+
combinationMethod));
113+
}
114+
115+
static final class BuilderDefaults {
116+
117+
private BuilderDefaults() {
118+
// prevent instantiation
119+
}
120+
121+
static Random random() {
122+
return new Random();
123+
}
124+
125+
static int batchSize() {
126+
return 1;
127+
}
128+
129+
static int k() {
130+
return KWayStateCoverTestsIterator.DEFAULT_K;
131+
}
132+
133+
static int randomWalkLen() {
134+
return KWayStateCoverTestsIterator.DEFAULT_R_WALK_LEN;
135+
}
136+
137+
static CombinationMethod combinationMethod() {
138+
return CombinationMethod.PERMUTATIONS;
139+
}
140+
}
141+
}

‎oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/KWayTransitionCoverEQOracle.java‎

Lines changed: 198 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,198 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.oracle.equivalence;
17+
18+
import java.util.Collection;
19+
import java.util.Random;
20+
import java.util.stream.Stream;
21+
22+
import de.learnlib.oracle.EquivalenceOracle;
23+
import de.learnlib.oracle.MembershipOracle;
24+
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
25+
import net.automatalib.automaton.DeterministicAutomaton;
26+
import net.automatalib.automaton.concept.Output;
27+
import net.automatalib.common.util.collection.IteratorUtil;
28+
import net.automatalib.util.automaton.conformance.KWayTransitionCoverTestsIterator;
29+
import net.automatalib.util.automaton.conformance.KWayTransitionCoverTestsIterator.GenerationMethod;
30+
import net.automatalib.util.automaton.conformance.KWayTransitionCoverTestsIterator.OptimizationMetric;
31+
import net.automatalib.word.Word;
32+
33+
/**
34+
* An {@link EquivalenceOracle} based on the concepts of mutation testing as described in the paper <a
35+
* href="https://doi.org/10.1007/978-3-319-57288-8_2">Learning from Faults: Mutation Testing in Active Automata
36+
* Learning</a> by Bernhard K. Aichernig and Martin Tappler.
37+
* <p>
38+
* This Equivalence oracle selects test cases based on k-way transitions coverage. It does that by generating random
39+
* queries and finding the smallest subset with the highest coverage. In other words, this oracle finds counter examples
40+
* by running random paths that cover all pairwise / k-way transitions.
41+
* <p>
42+
* <b>Implementation detail:</b> Note that this test generator heavily relies on the sampling of states. If the given
43+
* automaton has very few or very many states, the number of generated test cases may be very low or high, respectively.
44+
* As a result, it may be advisable to {@link EQOracleChain combine} this generator with other generators or limit the
45+
* number of generated test cases.
46+
*
47+
* @param <A>
48+
* automaton type
49+
* @param <I>
50+
* input symbol type
51+
* @param <D>
52+
* output domain
53+
*
54+
* @see KWayTransitionCoverTestsIterator
55+
*/
56+
public class KWayTransitionCoverEQOracle<A extends DeterministicAutomaton<?, I, ?> & Output<I, D>, I, D>
57+
extends AbstractTestWordEQOracle<A, I, D> {
58+
59+
private final Random random;
60+
private final int randomWalkLen;
61+
private final int numGeneratePaths;
62+
private final int maxPathLen;
63+
private final int maxNumberOfSteps;
64+
private final int k;
65+
private final OptimizationMetric optimizationMetric;
66+
private final GenerationMethod generationMethod;
67+
68+
/**
69+
* Constructor.
70+
*
71+
* @param oracle
72+
* the oracle for accessing the system under learning
73+
* @param random
74+
* the random number generator to use
75+
* @param randomWalkLen
76+
* the number of steps that are added by {@link GenerationMethod#PREFIX prefix}-generated paths
77+
* @param numGeneratePaths
78+
* number of {@link GenerationMethod#RANDOM randomly}-generated queries used to find the optimal subset
79+
* @param maxPathLen
80+
* the maximum step size of {@link GenerationMethod#RANDOM randomly}-generated queries
81+
* @param maxNumberOfSteps
82+
* threshold for the number of steps after which no more new test words will be generated (a value less than
83+
* zero means no limit)
84+
* @param k
85+
* k value used for K-Way transitions, i.e the number of steps between the start and the end of a
86+
* transition
87+
* @param optimizationMetric
88+
* the metric after which test queries are minimized
89+
* @param generationMethod
90+
* defines how the queries are generated
91+
* @param batchSize
92+
* size of the batches sent to the membership oracle
93+
*
94+
* @see KWayTransitionCoverTestsIterator#KWayTransitionCoverTestsIterator(DeterministicAutomaton, Collection,
95+
* Random, int, int, int, int, int, OptimizationMetric, GenerationMethod)
96+
*/
97+
@GenerateBuilder(defaults = BuilderDefaults.class)
98+
public KWayTransitionCoverEQOracle(MembershipOracle<I, D> oracle,
99+
Random random,
100+
int randomWalkLen,
101+
int numGeneratePaths,
102+
int maxPathLen,
103+
int maxNumberOfSteps,
104+
int k,
105+
OptimizationMetric optimizationMetric,
106+
GenerationMethod generationMethod,
107+
int batchSize) {
108+
super(oracle, batchSize);
109+
this.random = random;
110+
this.randomWalkLen = randomWalkLen;
111+
this.numGeneratePaths = numGeneratePaths;
112+
this.maxPathLen = maxPathLen;
113+
this.maxNumberOfSteps = maxNumberOfSteps;
114+
this.k = k;
115+
this.optimizationMetric = optimizationMetric;
116+
this.generationMethod = generationMethod;
117+
}
118+
119+
@Override
120+
public Stream<Word<I>> generateTestWords(A hypothesis, Collection<? extends I> inputs) {
121+
final DeterministicAutomaton<?, I, ?> casted = hypothesis;
122+
return doGenerateTestWords(casted,
123+
inputs,
124+
this.random,
125+
this.randomWalkLen,
126+
this.numGeneratePaths,
127+
this.maxPathLen,
128+
this.maxNumberOfSteps,
129+
this.k,
130+
this.optimizationMetric,
131+
this.generationMethod);
132+
}
133+
134+
private static <A extends DeterministicAutomaton<S, I, ?>, S, I> Stream<Word<I>> doGenerateTestWords(A hypothesis,
135+
Collection<? extends I> inputs,
136+
Random random,
137+
int randomWalkLen,
138+
int numGeneratePaths,
139+
int maxPathLen,
140+
int maxNumberOfSteps,
141+
int k,
142+
OptimizationMetric optimizationMetric,
143+
GenerationMethod generationMethod) {
144+
return IteratorUtil.stream(new KWayTransitionCoverTestsIterator<>(hypothesis,
145+
inputs,
146+
random,
147+
randomWalkLen,
148+
numGeneratePaths,
149+
maxPathLen,
150+
maxNumberOfSteps,
151+
k,
152+
optimizationMetric,
153+
generationMethod));
154+
}
155+
156+
static final class BuilderDefaults {
157+
158+
private BuilderDefaults() {
159+
// prevent instantiation
160+
}
161+
162+
static Random random() {
163+
return new Random();
164+
}
165+
166+
static int batchSize() {
167+
return 1;
168+
}
169+
170+
static int k() {
171+
return KWayTransitionCoverTestsIterator.DEFAULT_K;
172+
}
173+
174+
static GenerationMethod generationMethod() {
175+
return GenerationMethod.RANDOM;
176+
}
177+
178+
static int numGeneratePaths() {
179+
return KWayTransitionCoverTestsIterator.DEFAULT_NUM_GEN_PATHS;
180+
}
181+
182+
static int maxPathLen() {
183+
return KWayTransitionCoverTestsIterator.DEFAULT_MAX_PATH_LENGTH;
184+
}
185+
186+
static int maxNumberOfSteps() {
187+
return KWayTransitionCoverTestsIterator.DEFAULT_MAX_NUM_STEPS;
188+
}
189+
190+
static OptimizationMetric optimizationMetric() {
191+
return OptimizationMetric.STEPS;
192+
}
193+
194+
static int randomWalkLen() {
195+
return KWayTransitionCoverTestsIterator.DEFAULT_R_WALK_LEN;
196+
}
197+
}
198+
}

0 commit comments

Comments
 (0)