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}