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.algorithms.lstargeneric.ce;
018
019import java.util.Collections;
020import java.util.List;
021
022import net.automatalib.automata.concepts.SuffixOutput;
023import net.automatalib.words.Word;
024import de.learnlib.algorithms.lstargeneric.table.ObservationTable;
025import de.learnlib.algorithms.lstargeneric.table.Row;
026import de.learnlib.api.MembershipOracle;
027import de.learnlib.api.Query;
028import de.learnlib.counterexamples.GlobalSuffixFinder;
029import de.learnlib.counterexamples.GlobalSuffixFinders;
030import de.learnlib.counterexamples.LocalSuffixFinder;
031import de.learnlib.counterexamples.LocalSuffixFinders;
032import de.learnlib.oracles.DefaultQuery;
033
034public class ObservationTableCEXHandlers {
035        
036        public static ObservationTableCEXHandler<Object,Object> CLASSIC_LSTAR
037                = new ObservationTableCEXHandler<Object, Object>() {
038                        @Override
039                        public <RI,RO> List<List<Row<RI>>> handleCounterexample(
040                                        DefaultQuery<RI, RO> ceQuery,
041                                        ObservationTable<RI, RO> table,
042                                        SuffixOutput<RI, RO> hypOutput,
043                                        MembershipOracle<RI, RO> oracle) {
044                                return handleClassicLStar(ceQuery, table, oracle);
045                        }
046                        @Override
047                        public boolean needsConsistencyCheck() {
048                                return true;
049                        }
050                };
051                
052        public static ObservationTableCEXHandler<Object,Object> SUFFIX1BY1
053                = new ObservationTableCEXHandler<Object,Object>() {
054                        @Override
055                        public <RI,RO>
056                        List<List<Row<RI>>> handleCounterexample(
057                                        DefaultQuery<RI, RO> ceQuery,
058                                        ObservationTable<RI, RO> table,
059                                        SuffixOutput<RI, RO> hypOutput,
060                                        MembershipOracle<RI, RO> oracle) {
061                                return handleSuffix1by1(ceQuery, table, oracle);
062                        }
063                        @Override
064                        public boolean needsConsistencyCheck() {
065                                return false;
066                        }
067                };
068                
069        public static ObservationTableCEXHandler<Object,Object> MAHLER_PNUELI
070                = fromGlobalSuffixFinder(GlobalSuffixFinders.MAHLER_PNUELI);
071        
072        public static ObservationTableCEXHandler<Object,Object> SHAHBAZ
073                = fromGlobalSuffixFinder(GlobalSuffixFinders.SHAHBAZ);
074        
075        public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR
076                = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR, false);
077        
078        public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_ALLSUFFIXES
079                = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR, true);
080        
081        public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_REVERSE
082                = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, false);
083        
084        public static ObservationTableCEXHandler<Object,Object> FIND_LINEAR_REVERSE_ALLSUFFIXES
085                = fromLocalSuffixFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, true);
086        
087        public static ObservationTableCEXHandler<Object,Object> RIVEST_SCHAPIRE
088                = fromLocalSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, false);
089        
090        public static ObservationTableCEXHandler<Object,Object> RIVEST_SCHAPIRE_ALLSUFFIXES
091                = fromLocalSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, true);
092                
093        
094        
095        public static <I,O> 
096        ObservationTableCEXHandler<I, O> fromGlobalSuffixFinder(final GlobalSuffixFinder<I,O> globalFinder) {
097                return new ObservationTableCEXHandler<I, O>() {
098                        @Override
099                        public <RI extends I,RO extends O>
100                        List<List<Row<RI>>> handleCounterexample(
101                                        DefaultQuery<RI,RO> ceQuery, ObservationTable<RI,RO> table,
102                                        SuffixOutput<RI,RO> hypOutput, MembershipOracle<RI,RO> oracle) {
103                                List<Word<RI>> suffixes = globalFinder.findSuffixes(ceQuery, table, hypOutput, oracle);
104                                return handleGlobalSuffixes(table, suffixes, oracle);
105                        }
106                        @Override
107                        public boolean needsConsistencyCheck() {
108                                return false;
109                        }
110                };
111        }
112        
113        public static <I,O>
114        ObservationTableCEXHandler<I, O> fromLocalSuffixFinder(final LocalSuffixFinder<I,O> localFinder, final boolean allSuffixes) {
115                return new ObservationTableCEXHandler<I, O>() {
116                        @Override
117                        public <RI extends I,RO extends O>
118                        List<List<Row<RI>>> handleCounterexample(
119                                        DefaultQuery<RI,RO> ceQuery, ObservationTable<RI,RO> table,
120                                        SuffixOutput<RI,RO> hypOutput, MembershipOracle<RI,RO> oracle) {
121                                int suffixIdx = localFinder.findSuffixIndex(ceQuery, table, hypOutput, oracle);
122                                return handleLocalSuffix(ceQuery, table, suffixIdx, allSuffixes, oracle);
123                        }
124                        @Override
125                        public boolean needsConsistencyCheck() {
126                                return false;
127                        }
128                };
129        }
130        
131        
132        
133        public static <I,O>
134        ObservationTableCEXHandler<I, O> fromLocalSuffixFinder(final LocalSuffixFinder<I,O> localFinder) {
135                return fromLocalSuffixFinder(localFinder, false);
136        }
137        
138        public static <I,O>
139        List<List<Row<I>>> handleClassicLStar(DefaultQuery<I, O> ceQuery,
140                        ObservationTable<I, O> table, MembershipOracle<I, O> oracle) {
141                
142                List<Word<I>> prefixes = ceQuery.getInput().prefixes(false);
143                
144                return table.addShortPrefixes(prefixes, oracle);
145        }
146        
147        public static <I,O>
148        List<List<Row<I>>> handleSuffix1by1(DefaultQuery<I, O> ceQuery,
149                        ObservationTable<I, O> table, MembershipOracle<I, O> oracle) {
150                List<List<Row<I>>> unclosed = Collections.emptyList();
151                
152                List<Word<I>> suffixes = table.getSuffixes();
153                
154                Word<I> ceWord = ceQuery.getInput();
155                int ceLen = ceWord.length();
156                
157                for(int i = 1; i <= ceLen; i++) {
158                        Word<I> suffix = ceWord.suffix(i);
159                        if(suffixes != null) {
160                                if(suffixes.contains(suffix))
161                                        continue;
162                                suffixes = null;
163                        }
164                        
165                        unclosed = table.addSuffix(suffix, oracle);
166                        if(!unclosed.isEmpty())
167                                break;
168                }
169                
170                return unclosed;
171        }
172        
173        public static <I,O>
174        List<List<Row<I>>> handleGlobalSuffixes(ObservationTable<I,O> table, List<Word<I>> suffixes,
175                        MembershipOracle<I,O> oracle) {
176                return table.addSuffixes(suffixes, oracle);
177        }
178        
179        public static <I,O>
180        List<List<Row<I>>> handleLocalSuffix(Query<I,O> ceQuery, ObservationTable<I,O> table,
181                        int suffixIndex, boolean allSuffixes, MembershipOracle<I,O> oracle) {
182                List<Word<I>> suffixes
183                        = GlobalSuffixFinders.suffixesForLocalOutput(ceQuery, suffixIndex, allSuffixes);
184                return handleGlobalSuffixes(table, suffixes, oracle);
185        }
186        
187        public static <I,O>
188        List<List<Row<I>>> handleLocalSuffix(Query<I,O> ceQuery, ObservationTable<I,O> table,
189                        int suffixIndex, MembershipOracle<I,O> oracle) {
190                return handleLocalSuffix(ceQuery, table, suffixIndex, false, oracle);
191        }
192}