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.api;
018
019import java.util.Collection;
020
021import net.automatalib.automata.fsa.DFA;
022import net.automatalib.automata.transout.MealyMachine;
023import net.automatalib.words.Word;
024import de.learnlib.oracles.DefaultQuery;
025
026
027/**
028 * An equivalence oracle, which checks hypothesis automata against the (possibly unknown)
029 * system under learning (SUL).
030 * 
031 * Please note that equivalence oracles are implicitly connected to a SUL, there is no explicit
032 * references in terms of a {@link MembershipOracle} or such. However, this might be different
033 * in implementing classes.
034 * 
035 * <b>CAVEAT:</b> Equivalence oracles serve as an abstraction to tackle the (generally undecidable)
036 * problem of black-box equivalence testing. The contract imposed by this interface is that
037 * results returned by the {@link #findCounterExample(Object, Collection)} method are in fact
038 * counterexamples, <b>BUT</b> a <tt>null</tt> result signalling no counterexample was found
039 * does <b>not</b> mean that there can be none.
040 * 
041 * @author Maik Merten <maikmerten@googlemail.com>
042 * @author Malte Isberner <malte.isberner@gmail.com>
043 * 
044 * @param <A> automaton class this equivalence oracle works on
045 * @param <I> input symbol class
046 * @param <O> output class
047 */
048public interface EquivalenceOracle<A, I, O> {
049        
050        public static interface DFAEquivalenceOracle<I> extends EquivalenceOracle<DFA<?,I>,I,Boolean> {}
051        public static interface MealyEquivalenceOracle<I,O> extends EquivalenceOracle<MealyMachine<?,I,?,O>,I,Word<O>> {}
052        
053        
054        /**
055         * Searches for a counterexample disproving the subjected hypothesis.
056         * A counterexample is query which, when performed on the SUL, yields a different output
057         * than what was predicted by the hypothesis. If no counterexample could be found (this does
058         * not necessarily mean that none exists), <code>null</code> is returned.
059         * 
060         * @param hypothesis the conjecture
061         * @param inputs the set of inputs to consider
062         * @return a query exposing different behavior, or <tt>null</tt> if no counterexample
063         * could be found. In case a non-<tt>null</tt> value is returned, the output field
064         * in the {@link DefaultQuery} contains the SUL output for the respective query.
065         */
066        public DefaultQuery<I, O> findCounterExample(A hypothesis, Collection<? extends I> inputs);  
067        
068}