3636import de .learnlib .datastructure .observationtable .OTLearner ;
3737import de .learnlib .datastructure .observationtable .ObservationTable ;
3838import de .learnlib .datastructure .observationtable .Row ;
39- import de .learnlib .filter .MutableSymbolFilter ;
39+ import de .learnlib .filter .RefutableSymbolFilter ;
4040import de .learnlib .filter .symbol .AcceptAllSymbolFilter ;
4141import de .learnlib .oracle .TimedQueryOracle ;
4242import de .learnlib .query .DefaultQuery ;
4949import net .automatalib .alphabet .Alphabet ;
5050import net .automatalib .alphabet .GrowingAlphabet ;
5151import net .automatalib .alphabet .impl .GrowingMapAlphabet ;
52+ import net .automatalib .automaton .DeterministicAutomaton .FullIntAbstraction ;
5253import net .automatalib .automaton .mmlt .MMLT ;
5354import net .automatalib .automaton .mmlt .TimerInfo ;
5455import net .automatalib .common .util .HashUtil ;
@@ -79,7 +80,7 @@ public class ExtensibleLStarMMLT<I, O>
7980 private final ClosingStrategy <? super TimedInput <I >, ? super Word <TimedOutput <O >>> closingStrategy ;
8081
8182 private final TimedQueryOracle <I , O > timeOracle ;
82- private final MutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter ;
83+ private final RefutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter ;
8384
8485 private final MMLTHypDataContainer <I , O > hypData ;
8586
@@ -93,7 +94,7 @@ public class ExtensibleLStarMMLT<I, O>
9394 * <p>
9495 * This is a convenience constructor for
9596 * {@link #ExtensibleLStarMMLT(Alphabet, MMLTModelParams, TimedQueryOracle, List, ClosingStrategy,
96- * MutableSymbolFilter , AcexAnalyzer)} which uses
97+ * RefutableSymbolFilter , AcexAnalyzer)} which uses
9798 * <ul>
9899 * <li>{@link Collections#emptyList()} for {@code initialSuffixes},</li>
99100 * <li>{@link ClosingStrategies#CLOSE_SHORTEST} for {@code closingStrategy},</li>
@@ -102,9 +103,9 @@ public class ExtensibleLStarMMLT<I, O>
102103 * </ul>
103104 *
104105 * @param alphabet
105- * alphabet (of non-delaying inputs)
106+ * the alphabet (of non-delaying inputs)
106107 * @param modelParams
107- * model parameters
108+ * the model parameters
108109 * @param timeOracle
109110 * the query oracle for MMLTs
110111 */
@@ -124,15 +125,15 @@ public ExtensibleLStarMMLT(Alphabet<I> alphabet,
124125 * Instantiates a new learner.
125126 *
126127 * @param alphabet
127- * alphabet (of non-delaying inputs)
128+ * the alphabet (of non-delaying inputs)
128129 * @param modelParams
129- * model parameters
130+ * the model parameters
130131 * @param timeOracle
131132 * the query oracle for MMLTs
132133 * @param initialSuffixes
133- * initial set of suffixes (may be empty)
134+ * the initial set of suffixes (may be empty)
134135 * @param closingStrategy
135- * closing strategy for the observation table.
136+ * the closing strategy for the observation table.
136137 * @param symbolFilter
137138 * the symbol filter
138139 * @param analyzer
@@ -144,7 +145,7 @@ public ExtensibleLStarMMLT(Alphabet<I> alphabet,
144145 TimedQueryOracle <I , O > timeOracle ,
145146 List <Word <TimedInput <I >>> initialSuffixes ,
146147 ClosingStrategy <? super TimedInput <I >, ? super Word <TimedOutput <O >>> closingStrategy ,
147- MutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter ,
148+ RefutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter ,
148149 AcexAnalyzer analyzer ) {
149150 this .closingStrategy = closingStrategy ;
150151 this .timeOracle = timeOracle ;
@@ -180,7 +181,7 @@ public ExtensibleLStarMMLT(Alphabet<I> alphabet,
180181 * @param sortedTimers
181182 * timers, sorted ascendingly by their initial value
182183 * @param maxInitialValue
183- * max. initial value to consider
184+ * the maximum initial value to consider
184185 * @param <O>
185186 * output type
186187 *
@@ -212,7 +213,7 @@ public static <O> int selectOneShotTimer(List<? extends TimerInfo<?, O>> sortedT
212213 }
213214 }
214215
215- throw new IllegalStateException ("Max. initial value is too low; must include at least one timer." );
216+ throw new IllegalStateException ("Maximum initial value is too low; must include at least one timer." );
216217 }
217218
218219 @ Override
@@ -237,10 +238,10 @@ private List<Row<TimedInput<I>>> selectClosingRows(List<List<Row<TimedInput<I>>>
237238
238239 private void updateOutputs () {
239240 // Query output of newly-added transitions:
240- MMLTObservationTable <I , O > ot = this .hypData .getTable ();
241+ MMLTObservationTable <I , O > table = this .hypData .getTable ();
241242 List <OutputQuery <I , O >> queries = new ArrayList <>();
242243
243- for (Row <TimedInput <I >> row : IterableUtil .concat (ot .getShortPrefixRows (), ot .getLongPrefixRows ())) {
244+ for (Row <TimedInput <I >> row : IterableUtil .concat (table .getShortPrefixRows (), table .getLongPrefixRows ())) {
244245 Word <TimedInput <I >> label = row .getLabel ();
245246
246247 if (label .isEmpty ()) {
@@ -401,7 +402,8 @@ private boolean refineHypothesisSingle(DefaultQuery<TimedInput<I>, Word<TimedOut
401402 }
402403
403404 private void handleMissingTimeoutChange (Row <TimedInput <I >> spRow , TimerInfo <?, O > timeout ) {
404- LocationTimerInfo <I , O > locationTimerInfo = hypData .getTable ().getLocationTimerInfo (spRow );
405+ MMLTObservationTable <I , O > table = hypData .getTable ();
406+ LocationTimerInfo <I , O > locationTimerInfo = table .getLocationTimerInfo (spRow );
405407 assert locationTimerInfo != null : "Location with missing one-shot timer must have timers." ;
406408
407409 // Only timer with highest initial value can be one-shot.
@@ -411,16 +413,16 @@ private void handleMissingTimeoutChange(Row<TimedInput<I>> spRow, TimerInfo<?, O
411413 assert lastTimer != null ;
412414 if (!lastTimer .periodic ()) {
413415 Word <TimedInput <I >> lastTimerTransPrefix = spRow .getLabel ().append (TimedInput .step (lastTimer .initial ()));
414- Row <TimedInput <I >> row = hypData . getTable () .getRow (lastTimerTransPrefix );
416+ Row <TimedInput <I >> row = table .getRow (lastTimerTransPrefix );
415417 assert row != null ;
416418 if (!row .isShortPrefixRow ()) {
417419 // Last timer is one-shot + has fringe prefix:
418- this . hypData . getTable () .removeLpRow (lastTimerTransPrefix );
420+ table .removeLpRow (lastTimerTransPrefix );
419421 }
420422 }
421423
422424 // Prefix for timeout-transition of new one-shot timer:
423- assert this . hypData . getTable () .getRow (spRow .getLabel ().append (TimedInput .step (timeout .initial ()))) == null :
425+ assert table .getRow (spRow .getLabel ().append (TimedInput .step (timeout .initial ()))) == null :
424426 "Timer already appears to be one-shot." ;
425427
426428 // Remove all timers with greater timeout (are now redundant):
@@ -434,8 +436,7 @@ private void handleMissingTimeoutChange(Row<TimedInput<I>> spRow, TimerInfo<?, O
434436 locationTimerInfo .setOneShotTimer (timeout .name ());
435437
436438 // Update fringe prefixes + close table:
437- List <List <Row <TimedInput <I >>>> unclosed =
438- this .hypData .getTable ().addTimerTransition (spRow , timeout , this .timeOracle );
439+ List <List <Row <TimedInput <I >>>> unclosed = table .addTimerTransition (spRow , timeout , this .timeOracle );
439440 this .completeConsistentTable (unclosed );
440441 }
441442
@@ -469,9 +470,12 @@ private void completeConsistentTable(List<List<Row<TimedInput<I>>>> unclosed) {
469470 */
470471 private static <I , O > MMLTHypothesis <I , O > constructHypothesis (MMLTHypDataContainer <I , O > hypData ) {
471472
473+ final MMLTObservationTable <I , O > table = hypData .getTable ();
474+ final MMLTModelParams <O > params = hypData .getModelParams ();
475+
472476 // 1. Create map that stores link between contentID and short-prefix row:
473477 final Map <Integer , Row <TimedInput <I >>> locationContentIdMap = new HashMap <>(); // contentId -> sp location
474- for (Row <TimedInput <I >> spRow : hypData . getTable () .getShortPrefixRows ()) {
478+ for (Row <TimedInput <I >> spRow : table .getShortPrefixRows ()) {
475479 // Multiple sp rows may have same contentID. Thus, assign each id only one location:
476480 locationContentIdMap .putIfAbsent (spRow .getRowContentId (), spRow );
477481 }
@@ -485,19 +489,19 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
485489 }
486490
487491 // 3. Prepare objects for automaton, timers and resets:
488- int numLocations = hypData . getTable () .numberOfShortPrefixRows ();
492+ int numLocations = table .numberOfShortPrefixRows ();
489493 final Map <Integer , Integer > stateMap =
490494 new HashMap <>(HashUtil .capacity (numLocations )); // row content id -> state id
491495 final Map <Integer , Word <TimedInput <I >>> prefixMap =
492496 new HashMap <>(HashUtil .capacity (numLocations )); // state id -> location prefix
493497 MMLTHypothesis <I , O > hypothesis = new MMLTHypothesis <>(alphabet ,
494498 numLocations ,
495- hypData . getModelParams () .silentOutput (),
496- hypData . getModelParams () .outputCombiner (),
499+ params .silentOutput (),
500+ params .outputCombiner (),
497501 prefixMap ); // we pass the prefix map as reference so that we can fill it later
498502
499503 // 4. Create one state per location:
500- for (Row <TimedInput <I >> row : hypData . getTable () .getShortPrefixRows ()) {
504+ for (Row <TimedInput <I >> row : table .getShortPrefixRows ()) {
501505 int newStateId = hypothesis .addState ();
502506 stateMap .putIfAbsent (row .getRowContentId (), newStateId );
503507 prefixMap .put (newStateId , row .getLabel ());
@@ -514,11 +518,13 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
514518 Integer rowContentId = e .getKey ();
515519 Row <TimedInput <I >> spLocation = locationContentIdMap .get (rowContentId );
516520
521+ assert spLocation != null ;
522+
517523 for (I symbol : alphabet ) {
518524 int symIdx = hypData .getAlphabet ().getSymbolIndex (TimedInput .input (symbol ));
519525
520526 TimedOutput <O > transOutput = hypData .getTransitionOutput (spLocation , symIdx );
521- O output = hypData . getModelParams () .silentOutput (); // silent by default
527+ O output = params .silentOutput (); // silent by default
522528 if (transOutput != null ) {
523529 output = transOutput .symbol ();
524530 }
@@ -532,7 +538,7 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
532538
533539 // Add transition to automaton:
534540 int sourceLocId = e .getValue ();
535- int successorLocId = stateMap .get (successorId );
541+ int successorLocId = stateMap .getOrDefault (successorId , FullIntAbstraction . INVALID_STATE );
536542 hypothesis .addTransition (sourceLocId , symbol , successorLocId , output );
537543
538544 // Check for local reset:
@@ -541,7 +547,6 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
541547 hypothesis .addLocalReset (sourceLocId , symbol );
542548 }
543549 }
544-
545550 }
546551
547552 // 6. Add timeout transitions:
@@ -551,7 +556,7 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
551556
552557 assert spLocation != null ;
553558
554- LocationTimerInfo <I , O > timerInfo = hypData . getTable () .getLocationTimerInfo (spLocation );
559+ LocationTimerInfo <I , O > timerInfo = table .getLocationTimerInfo (spLocation );
555560
556561 if (timerInfo != null ) {
557562 for (TimerInfo <?, O > timer : timerInfo .getLocalTimers ().values ()) {
@@ -568,7 +573,8 @@ private static <I, O> MMLTHypothesis<I, O> constructHypothesis(MMLTHypDataContai
568573 timer .name (),
569574 timer .initial (),
570575 timer .outputs (),
571- stateMap .get (successorId ));
576+ stateMap .getOrDefault (successorId ,
577+ FullIntAbstraction .INVALID_STATE ));
572578 }
573579 }
574580 }
@@ -629,7 +635,7 @@ static <I> List<Word<TimedInput<I>>> initialSuffixes() {
629635 return ClosingStrategies .CLOSE_SHORTEST ;
630636 }
631637
632- static <I > MutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter () {
638+ static <I > RefutableSymbolFilter <TimedInput <I >, InputSymbol <I >> symbolFilter () {
633639 return new AcceptAllSymbolFilter <>();
634640 }
635641
0 commit comments