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.counterexamples;
018
019import net.automatalib.automata.concepts.SuffixOutput;
020import de.learnlib.api.AccessSequenceTransformer;
021import de.learnlib.api.LearningAlgorithm;
022import de.learnlib.api.MembershipOracle;
023import de.learnlib.api.Query;
024
025/**
026 * Suffix-based local counterexample analyzer.
027 * <p>
028 * Given a query <tt>(u, v)</tt> which is a counterexample (i.e., the suffix-output for
029 * <tt>(u,v)</tt> is distinct from the target system's output for <tt>(u,v)</tt>), it
030 * calculates the index <tt>i</tt> of the suffix such that <tt>w[i:]</tt> (<tt>w = uv</tt>)
031 * still allows to expose a behavioral difference for an adequate prefix. This adequate prefix
032 * can be determined as <tt>{w[:i]}</tt>, where <tt>{.}</tt> denotes the access sequence of
033 * the corresponding word.
034 * <p>
035 * The effect of adding such a suffix can be described as follows: <tt>{w[:i]}</tt> and
036 * <tt>{w[:i-1]}w[i-1]</tt> both lead to the same state in the hypothesis, but a local suffix finder
037 * chooses the index i such that the output for <tt>({w[:i]}, w[i:])</tt> and
038 * <tt>({w[:i-1]}w[i-1], w[i:])</tt> will differ. Hence, the transition to the state reached by
039 * <tt>{w[:i]}</tt> from <tt>{w[:i-1]}</tt> is disproved.
040 * <p>
041 * Please note that the type parameters of these class only constitute <i>upper</i> bounds
042 * for the respective input symbol and output classes, denoting the requirements of the
043 * process in general. A suffix finder which does not
044 * exploit any properties of the used classes will implement this interface with
045 * <tt>&lt;Object,Object&gt;</tt> generic arguments only. The genericity is still maintained
046 * due to the <tt>RI</tt> and <tt>RO</tt> generic parameters in the
047 * {@link #findSuffixIndex(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)}
048 * method.
049 * 
050 * @author Malte Isberner <malte.isberner@gmail.com>
051 *
052 * @param <I> input symbol class upper bound
053 * @param <O> output class upper bound
054 */
055public interface LocalSuffixFinder<I, O> {
056        
057        /** 
058         * Finds, for a given counterexample, a "split index", such that:
059         * - the part of the query word <i>before this index</i> leads to the state being split
060         * - the part of the query word <i>from this index on</i> is a suffix capable of splitting
061         * this state.
062         * 
063         * @param <RI> real input symbol class used for *this* counterexample analysis
064         * @param <RO> real output class used for *this* counterexample analysis
065         * @param ceQuery the counterexample query that triggered the refinement. Note that the same
066         * restrictions as in {@link LearningAlgorithm#refineHypothesis(de.learnlib.oracles.DefaultQuery)}
067         * apply.
068         * @param asTransformer an {@link AccessSequenceTransformer} used for access sequence transformation,
069         * if applicable.
070         * @param hypOutput interface to the output generation of the hypothesis, with the aim of
071         * comparing outputs of the hypothesis and the SUL.
072         * @param oracle interface to the System Under Learning (SUL).
073         * @return an adequate split index, or <tt>-1</tt> if the counterexample could not be analyzed.
074         */
075        public <RI extends I,RO extends O>
076        int findSuffixIndex(Query<RI,RO> ceQuery,
077                        AccessSequenceTransformer<RI> asTransformer,
078                        SuffixOutput<RI,RO> hypOutput,
079                        MembershipOracle<RI,RO> oracle);
080        
081}