001/* Copyright (C) 2013 TU Dortmund 002 * This file is part of LearnLib, http://www.learnlib.de/. 003 * 004 * LearnLib is free software; you can redistribute it and/or 005 * modify it under the terms of the GNU Lesser General Public 006 * License version 3.0 as published by the Free Software Foundation. 007 * 008 * LearnLib is distributed in the hope that it will be useful, 009 * but WITHOUT ANY WARRANTY; without even the implied warranty of 010 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 011 * Lesser General Public License for more details. 012 * 013 * You should have received a copy of the GNU Lesser General Public 014 * License along with LearnLib; if not, see 015 * <http://www.gnu.de/documents/lgpl.en.html>. 016 */ 017package de.learnlib.eqtests.basic; 018 019import java.util.ArrayList; 020import java.util.Collection; 021import java.util.Collections; 022import java.util.List; 023import java.util.Objects; 024 025import net.automatalib.automata.UniversalDeterministicAutomaton; 026import net.automatalib.automata.concepts.Output; 027import net.automatalib.automata.fsa.DFA; 028import net.automatalib.automata.transout.MealyMachine; 029import net.automatalib.commons.util.collections.CollectionsUtil; 030import net.automatalib.commons.util.mappings.MutableMapping; 031import net.automatalib.util.automata.Automata; 032import net.automatalib.words.Word; 033import net.automatalib.words.WordBuilder; 034import de.learnlib.api.EquivalenceOracle; 035import de.learnlib.api.MembershipOracle; 036import de.learnlib.oracles.DefaultQuery; 037 038/** 039 * Implements an equivalence test by applying the Wp-method test on the given hypothesis automaton, 040 * as described in "Test Selection Based on Finite State Models" by S. Fujiwara et al. 041 * 042 * @author Malte Isberner <malte.isberner@gmail.com> 043 * 044 * @param <A> automaton class 045 * @param <I> input symbol class 046 * @param <O> output class 047 */ 048public class WpMethodEQOracle<A extends UniversalDeterministicAutomaton<?, I, ?, ?, ?> & Output<I,O>,I,O> 049 implements EquivalenceOracle<A, I, O> { 050 051 public static class DFAWpMethodEQOracle<I> extends WpMethodEQOracle<DFA<?,I>,I,Boolean> 052 implements DFAEquivalenceOracle<I> { 053 public DFAWpMethodEQOracle(int maxDepth, 054 MembershipOracle<I, Boolean> sulOracle) { 055 super(maxDepth, sulOracle); 056 } 057 } 058 059 public static class MealyWpMethodEQOracle<I,O> extends WpMethodEQOracle<MealyMachine<?,I,?,O>,I,Word<O>> { 060 public MealyWpMethodEQOracle(int maxDepth, 061 MembershipOracle<I, Word<O>> sulOracle) { 062 super(maxDepth, sulOracle); 063 } 064 } 065 066 private final int maxDepth; 067 private final MembershipOracle<I, O> sulOracle; 068 069 /** 070 * Constructor. 071 * @param maxDepth the maximum length of the "middle" part of the test cases 072 * @param sulOracle interface to the system under learning 073 */ 074 public WpMethodEQOracle(int maxDepth, MembershipOracle<I,O> sulOracle) { 075 this.maxDepth = maxDepth; 076 this.sulOracle = sulOracle; 077 } 078 079 /* 080 * (non-Javadoc) 081 * @see de.learnlib.api.EquivalenceOracle#findCounterExample(java.lang.Object, java.util.Collection) 082 */ 083 @Override 084 public DefaultQuery<I, O> findCounterExample(A hypothesis, 085 Collection<? extends I> inputs) { 086 UniversalDeterministicAutomaton<?, I, ?, ?, ?> aut = hypothesis; 087 Output<I,O> out = hypothesis; 088 return doFindCounterExample(aut, out, inputs); 089 } 090 091 092 /* 093 * Delegate target, used to bind the state-parameter of the automaton 094 */ 095 private <S> DefaultQuery<I,O> doFindCounterExample(UniversalDeterministicAutomaton<S, I, ?, ?, ?> hypothesis, 096 Output<I,O> output, Collection<? extends I> inputs) { 097 098 List<Word<I>> stateCover = new ArrayList<Word<I>>(hypothesis.size()); 099 List<Word<I>> transitions = new ArrayList<Word<I>>(hypothesis.size() * (inputs.size() - 1)); 100 101 Automata.cover(hypothesis, inputs, stateCover, transitions); 102 103 List<Word<I>> globalSuffixes = Automata.characterizingSet(hypothesis, inputs); 104 if(globalSuffixes.isEmpty()) 105 globalSuffixes = Collections.singletonList(Word.<I>epsilon()); 106 107 WordBuilder<I> wb = new WordBuilder<>(); 108 109 110 // Phase 1: state cover * middle part * global suffixes 111 for(List<? extends I> middle : CollectionsUtil.allTuples(inputs, 1, maxDepth)) { 112 for(Word<I> as : stateCover) { 113 for(Word<I> suffix : globalSuffixes) { 114 wb.append(as).append(middle).append(suffix); 115 Word<I> queryWord = wb.toWord(); 116 wb.clear(); 117 DefaultQuery<I,O> query = new DefaultQuery<>(queryWord); 118 O hypOutput = output.computeOutput(queryWord); 119 sulOracle.processQueries(Collections.singleton(query)); 120 if(!Objects.equals(hypOutput, query.getOutput())) 121 return query; 122 } 123 } 124 } 125 126 // Phase 2: transitions (not in state cover) * middle part * local suffixes 127 MutableMapping<S,List<Word<I>>> localSuffixSets 128 = hypothesis.createStaticStateMapping(); 129 130 for(List<? extends I> middle : CollectionsUtil.allTuples(inputs, 1, maxDepth)) { 131 for(Word<I> trans : transitions) { 132 S state = hypothesis.getState(trans); 133 List<Word<I>> localSuffixes = localSuffixSets.get(state); 134 if(localSuffixes == null) { 135 localSuffixes = Automata.stateCharacterizingSet(hypothesis, inputs, state); 136 if(localSuffixes.isEmpty()) 137 localSuffixes = Collections.singletonList(Word.<I>epsilon()); 138 localSuffixSets.put(state, localSuffixes); 139 } 140 141 for(Word<I> suffix : localSuffixes) { 142 wb.append(trans).append(middle).append(suffix); 143 Word<I> queryWord = wb.toWord(); 144 wb.clear(); 145 DefaultQuery<I,O> query = new DefaultQuery<>(queryWord); 146 O hypOutput = output.computeOutput(queryWord); 147 sulOracle.processQueries(Collections.singleton(query)); 148 if(!Objects.equals(hypOutput, query.getOutput())) 149 return query; 150 } 151 } 152 } 153 154 return null; 155 } 156 157}