|
36 | 36 | import net.automatalib.automaton.impl.CompactTransition; |
37 | 37 | import net.automatalib.automaton.transducer.MealyMachine; |
38 | 38 | import net.automatalib.automaton.transducer.impl.CompactMealy; |
39 | | -import net.automatalib.util.automaton.equivalence.NearLinearEquivalenceTest; |
| 39 | +import net.automatalib.incremental.util.DFSepWordFinder; |
| 40 | +import net.automatalib.incremental.util.DFSepWordFinder.Visitor; |
40 | 41 | import net.automatalib.word.Word; |
41 | 42 | import net.automatalib.word.WordBuilder; |
42 | 43 | import org.checkerframework.checker.nullness.qual.NonNull; |
| 44 | +import org.checkerframework.checker.nullness.qual.Nullable; |
43 | 45 |
|
44 | 46 | /** |
45 | 47 | * A cache for an {@link AdaptiveMembershipOracle}. Upon construction, it is provided with a delegate oracle. Queries |
@@ -135,16 +137,25 @@ public void processQueries(Collection<? extends AdaptiveQuery<I, O>> queries) { |
135 | 137 |
|
136 | 138 | @Override |
137 | 139 | public EquivalenceOracle<MealyMachine<?, I, ?, O>, I, Word<O>> createCacheConsistencyTest() { |
138 | | - return (hypothesis, alphabet) -> { |
139 | | - //TODO: If the hypothesis has undefined transitions, but the cache doesn't, it is a clear counterexample! |
140 | | - final Word<I> sepWord = NearLinearEquivalenceTest.findSeparatingWord(cache, hypothesis, alphabet, true); |
| 140 | + return this::findCounterexample; |
| 141 | + } |
| 142 | + |
| 143 | + private <S, T> @Nullable DefaultQuery<I, Word<O>> findCounterexample(MealyMachine<S, I, T, O> hypothesis, |
| 144 | + Collection<? extends I> inputs) { |
| 145 | + final Word<I> sepWord = DFSepWordFinder.findSeparatingWord(cache, hypothesis, inputs, false, new Visitor<>() { |
141 | 146 |
|
142 | | - if (sepWord != null) { |
143 | | - return new DefaultQuery<>(sepWord, cache.computeOutput(sepWord)); |
| 147 | + @Override |
| 148 | + public boolean succConflict(CompactTransition<O> incTrans, @Nullable T targetTrans) { |
| 149 | + return targetTrans == null || |
| 150 | + !Objects.equals(incTrans.getProperty(), hypothesis.getTransitionOutput(targetTrans)); |
144 | 151 | } |
| 152 | + }); |
| 153 | + |
| 154 | + if (sepWord != null) { |
| 155 | + return new DefaultQuery<>(sepWord, cache.computeOutput(sepWord)); |
| 156 | + } |
145 | 157 |
|
146 | | - return null; |
147 | | - }; |
| 158 | + return null; |
148 | 159 | } |
149 | 160 |
|
150 | 161 | @Override |
|
0 commit comments