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><Object,Object></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}