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}