001/* Copyright (C) 2013 TU Dortmund 002 * This file is part of AutomataLib, http://www.automatalib.net/. 003 * 004 * AutomataLib 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 * AutomataLib 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 AutomataLib; if not, see 015 * http://www.gnu.de/documents/lgpl.en.html. 016 */ 017package net.automatalib.incremental.dfa; 018 019import net.automatalib.incremental.ConflictException; 020import net.automatalib.words.Alphabet; 021import net.automatalib.words.Word; 022 023public class IncrementalPCDFABuilder<I> extends AbstractIncrementalDFABuilder<I> { 024 025 public IncrementalPCDFABuilder(Alphabet<I> inputAlphabet) { 026 super(inputAlphabet); 027 } 028 029 /* 030 * (non-Javadoc) 031 * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#getState(net.automatalib.words.Word) 032 */ 033 @Override 034 protected State getState(Word<I> word) { 035 State s = init; 036 037 for(I sym : word) { 038 int idx = inputAlphabet.getSymbolIndex(sym); 039 s = s.getSuccessor(idx); 040 if(s == null || s == sink) 041 return s; 042 } 043 return s; 044 } 045 046 /* 047 * (non-Javadoc) 048 * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#lookup(net.automatalib.words.Word) 049 */ 050 @Override 051 public Acceptance lookup(Word<I> word) { 052 State s = getState(word); 053 if(s == null) 054 return Acceptance.DONT_KNOW; 055 return (s != sink) ? s.getAcceptance() : Acceptance.FALSE; 056 } 057 058 /* 059 * (non-Javadoc) 060 * @see net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder#insert(net.automatalib.words.Word, boolean) 061 */ 062 @Override 063 public void insert(Word<I> word, boolean accepting) { 064 int len = word.length(); 065 Acceptance acc = Acceptance.fromBoolean(accepting); 066 067 State curr = init; 068 State conf = null; 069 070 int confIndex = -1; 071 072 int prefixLen = 0; 073 for(I sym : word) { 074 if(curr == sink) 075 break; 076 if(conf == null && curr.isConfluence()) { 077 conf = curr; 078 confIndex = prefixLen; 079 } 080 081 int idx = inputAlphabet.getSymbolIndex(sym); 082 State succ = curr.getSuccessor(idx); 083 if(succ == null) 084 break; 085 curr = succ; 086 prefixLen++; 087 } 088 089 if(curr == sink) { 090 if(accepting) 091 throw new RuntimeException("Conflict"); 092 return; 093 } 094 095 if(prefixLen == len) { 096 Acceptance currAcc = curr.getAcceptance(); 097 if(currAcc == acc) 098 return; 099 else if(conf == null) { 100 if(currAcc == Acceptance.DONT_KNOW) { 101 if(accepting) { 102 State upd = updateSignature(curr, Acceptance.TRUE); 103 if(upd == curr) 104 return; 105 curr = upd; 106 } 107 else { 108 purge(curr); 109 curr = sink; 110 } 111 } 112 else 113 throw new ConflictException("Incompatible acceptances: " + currAcc + " vs " + acc); 114 } 115 } 116 117 118 Word<I> suffix = word.subWord(prefixLen); 119 120 State last; 121 122 State suffixState = null; 123 int suffTransIdx = -1; 124 if(!suffix.isEmpty()) { 125 suffixState = createSuffix(suffix.subWord(1), accepting); 126 I sym = suffix.getSymbol(0); 127 suffTransIdx = inputAlphabet.getSymbolIndex(sym); 128 } 129 130 int currentIndex; 131 if(conf != null) { 132 if(suffTransIdx == -1) 133 last = clone(curr, acc); 134 else /* if(accepting) */ 135 last = clone(curr, Acceptance.TRUE, suffTransIdx, suffixState); 136 137 for(int i = prefixLen - 1; i >= confIndex; i--) { 138 State s = getState(word.prefix(i)); 139 I sym = word.getSymbol(i); 140 int idx = inputAlphabet.getSymbolIndex(sym); 141 if(accepting) 142 last = clone(s, Acceptance.TRUE, idx, last); 143 else 144 last = clone(s, idx, last); 145 } 146 147 currentIndex = confIndex; 148 } 149 else { 150 if(suffTransIdx == -1) 151 last = updateSignature(curr, acc); 152 else /* if(accepting) */ 153 last = updateSignature(curr, Acceptance.TRUE, suffTransIdx, suffixState); 154 currentIndex = prefixLen; 155 } 156 157 while(--currentIndex >= 0) { 158 State state = getState(word.prefix(currentIndex)); 159 I sym = word.getSymbol(currentIndex); 160 int idx = inputAlphabet.getSymbolIndex(sym); 161 if(accepting) { 162 Acceptance lastAcc = last.getAcceptance(); 163 last = updateSignature(state, Acceptance.TRUE, idx, last); 164 if(state == last && lastAcc == Acceptance.TRUE) 165 break; 166 } 167 else { 168 last = updateSignature(state, idx, last); 169 if(state == last) 170 break; 171 } 172 } 173 } 174 175 /** 176 * Removes a state and all of its successors from the register. 177 * @param state the state to purge 178 */ 179 private void purge(State state) { 180 StateSignature sig = state.getSignature(); 181 if(register.remove(sig) == null) 182 return; 183 for(int i = 0; i < alphabetSize; i++) { 184 State succ = sig.successors[i]; 185 if(succ != null) 186 purge(succ); 187 sig.successors[i] = null; 188 } 189 } 190 191 /** 192 * Creates a suffix state sequence, i.e., a linear sequence of states connected by transitions 193 * labeled by the letters of the given suffix word. 194 * @param suffix the suffix word 195 * @param acc whether or not the final state should be accepting 196 * @return the first state in the sequence 197 */ 198 private State createSuffix(Word<I> suffix, boolean accepting) { 199 State last; 200 Acceptance intermediate; 201 if(!accepting) { 202 if(sink == null) 203 sink = new State(null); 204 last = sink; 205 intermediate = Acceptance.DONT_KNOW; 206 } 207 else { 208 StateSignature sig = new StateSignature(alphabetSize, Acceptance.TRUE); 209 last = replaceOrRegister(sig); 210 intermediate = Acceptance.TRUE; 211 } 212 213 int len = suffix.length(); 214 for(int i = len - 1; i >= 0; i--) { 215 StateSignature sig = new StateSignature(alphabetSize, intermediate); 216 I sym = suffix.getSymbol(i); 217 int idx = inputAlphabet.getSymbolIndex(sym); 218 sig.successors[idx] = last; 219 last = replaceOrRegister(sig); 220 } 221 222 return last; 223 } 224 225}