improved documentation

Author: stateMachinist

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/CoreRow.java

@@ -23,7 +23,8 @@
 import net.automatalib.word.Word;
 
 /**
- * Each core row represents some hypothesis state and stores its outputs for all table suffixes.
+ * Each core row represents some hypothesis state
+ * and stores its outputs for all table suffixes.
  */
 class CoreRow<S, I, O> extends Row<S, I, O> {
 
@@ -34,6 +35,7 @@ class CoreRow<S, I, O> extends Row<S, I, O> {
 
     /**
      * Index of this row in the core row list.
+     * Used as a unique address.
      */
     final int idx;
 
@@ -43,7 +45,8 @@ class CoreRow<S, I, O> extends Row<S, I, O> {
     final Map<Word<I>, Word<O>> sufToOut;
 
     /**
-     * Identifiers of all suffix-output pairs in this row, used for fast compatibility checking.
+     * Identifiers of all suffix-output pairs in this row,
+     * used for fast compatibility checking.
      */
     final Set<Integer> cellIds;
 
@@ -52,7 +55,7 @@ class CoreRow<S, I, O> extends Row<S, I, O> {
         this.state = state;
         this.idx = idx;
         sufToOut = new HashMap<>();
-        cellIds = new HashSet<>(); // use HashSet to enable fast containment checks
+        cellIds = new HashSet<>(); // use HashSet for fast containment checks
     }
 
     void addSuffix(Word<I> suf, Word<O> out, int cell) {

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/FringeRow.java

@@ -41,7 +41,7 @@ class FringeRow<S, I, O> extends Row<S, I, O> {
     final I transIn;
 
     /**
-     * Output symbol (determined dynamically).
+     * Output symbol (determined lazily).
      */
     O transOut;
 

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/GenericSparseLearner.java

@@ -48,12 +48,12 @@ class GenericSparseLearner<S, I, O> implements MealyLearner<I, O> {
     private final Deque<Word<I>> sufs;
 
     /**
-     * Core rows.
+     * List of core rows. Rows can be addressed by their index in this list.
      */
     private final List<CoreRow<S, I, O>> cRows;
 
     /**
-     * Fringe rows.
+     * Fringe rows (stored in a stack for LIFO iteration).
      */
     private final Deque<FringeRow<S, I, O>> fRows;
 
@@ -63,12 +63,13 @@ class GenericSparseLearner<S, I, O> implements MealyLearner<I, O> {
     private final Map<Word<I>, FringeRow<S, I, O>> prefToFringe;
 
     /**
-     * List of unique suffix-output cells.
+     * List of unique suffix-output pairs, addressable by index.
+     * Used for table compression: table entries only hold cell index.
      */
     private final List<Pair<Word<I>, Word<O>>> cells;
 
     /**
-     * Maps each suffix-output cell to its list index.
+     * Maps each suffix-output pair to its index (see {@link #cells}).
      */
     private final Map<Pair<Word<I>, Word<O>>, Integer> cellToIdx;
 
@@ -159,13 +160,14 @@ private void updateHypothesis() {
                 return;
             } else {
                 assert f.transOut != null;
+                assert f.leaf.cRow != null;
                 hyp.setTransition(f.srcState, f.transIn, f.leaf.cRow.state, f.transOut);
             }
         }
     }
 
     private void classifyFringePrefix(FringeRow<S, I, O> f) {
-        f.leaf.update(cRows, sufs.size());
+        f.leaf.update(cRows);
         if (f.leaf.isUnsplit()) {
             return;
         }
@@ -174,7 +176,7 @@ private void classifyFringePrefix(FringeRow<S, I, O> f) {
         if (sep != null) {
             followNode(f, sep);
         } else {
-            f.leaf.sep = new Separator<>(pickSuffix(f.leaf.remRows), f.leaf.remRows, f.leaf.cellsIds);
+            f.leaf.sep = new Separator<>(pickSuffix(f.leaf.remRows), f.leaf.remRows, f.leaf.cellIds);
             followNode(f, f.leaf.sep);
         }
     }
@@ -212,7 +214,7 @@ private Word<I> pickSuffix(BitSet remRows) {
     }
 
     private void followNode(FringeRow<S, I, O> f, Node<S, I, O> n) {
-        if (n instanceof Leaf) {
+        if (n instanceof Leaf) { // TODO simplify when switching to newer java
             final Leaf<S, I, O> l = (Leaf<S, I, O>) n;
             assert l.isUnsplit();
             f.leaf = l;
@@ -230,7 +232,7 @@ private void followNode(FringeRow<S, I, O> f, Node<S, I, O> n) {
 
         final BitSet remRows = new BitSet();
         sep.remRows.stream().filter(i -> cRows.get(i).cellIds.contains(cellIdx)).forEach(remRows::set);
-        final List<Integer> cellIds = new ArrayList<>(sep.cellsIds); // important: copy elements!
+        final List<Integer> cellIds = new ArrayList<>(sep.cellIds); // important: copy elements!
         cellIds.add(cellIdx);
         if (remRows.isEmpty()) {
             // no compatible core prefix
@@ -249,7 +251,7 @@ private void followNode(FringeRow<S, I, O> f, Node<S, I, O> n) {
 
     private Word<O> query(Row<S, I, O> r, Word<I> suf) {
         final Word<O> out = oracle.answerQuery(r.prefix.concat(suf));
-        if (r instanceof FringeRow) {
+        if (r instanceof FringeRow) { // TODO simplify when switching to newer java
             final FringeRow<S, I, O> f = (FringeRow<S, I, O>) r;
             f.transOut = out.prefix(f.prefix.length()).lastSymbol();
         }
@@ -301,6 +303,7 @@ private int moveToCore(FringeRow<S, I, O> f, List<Integer> cellIds) {
      * and returns a list containing the observations for all suffixes.
      */
     private List<Integer> completeRowObservations(FringeRow<S, I, O> f, List<Integer> cellIds) {
+        // TODO simplify collector calls when switching to newer java
         final List<Word<I>> sufsPresent = cellIds.stream().map(c -> this.cells.get(c).getFirst()).collect(Collectors.toList());
         final List<Word<I>> sufsMissing = sufs.stream().filter(s -> !sufsPresent.contains(s)).collect(Collectors.toList());
         final List<Integer> cellIdsFull = new ArrayList<>(cellIds); // important: copy elements!
@@ -325,8 +328,8 @@ private void identifyNewState(DefaultQuery<I, Word<O>> q) {
         final Word<I> u = accSeq.apply(cex.prefix(idxSym));
         final Word<I> ui = u.append(cex.getSymbol(idxSym));
         final FringeRow<S, I, O> f = prefToFringe.get(ui);
-        assert f.leaf.isUnsplit();
-        final int cRowIdx = moveToCore(f, f.leaf.cellsIds);
+        final int cRowIdx = moveToCore(f, f.leaf.cellIds);
+        assert f.leaf.cRow != null;
         if (f.leaf.cRow.cellIds.containsAll(cRows.get(cRowIdx).cellIds)) {
             // only add new suffix if the row is not yet distinguished
             addSuffixToTable(cex.subWord(idxSuf));

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Leaf.java

@@ -20,67 +20,85 @@
 
 import org.checkerframework.checker.nullness.qual.Nullable;
 
+/**
+ * Leaves can be split or unsplit.
+ * An unsplit leaf has a single compatible core row to which it points.
+ * As new core rows emerge, the observations of the leaf may not suffice
+ * anymore to uniquely assign it to some core row. Then, it becomes split.
+ * Split leaves cache suffix selection by reference to separators.
+ * Leaves remember how many core rows and suffixes existed at their last visit.
+ * This information is used as a logical timestamp to check
+ * if the separator is still known to be optimal
+ * or if it needs to be recomputed.
+ */
 class Leaf<S, I, O> extends Node<S, I, O> {
 
-    final @Nullable CoreRow<S, I, O> cRow;
-    private boolean split;
-    private int lastNumCRows;
-    private int lastNumSufs;
+    /**
+     * Core row associated with this leaf (null if split, see {@link Leaf}).
+     */
+    @Nullable CoreRow<S, I, O> cRow;
 
     /**
-     * Split leafs always remember how many core rows and suffixes the table contained
-     * at their last visit. This information is used as a logical timestamp to check
-     * if the separator is still guaranteed to be optimal or if it needs to be recomputed.
+     * Separator cached by this leaf (see {@link Leaf}).
      */
     @Nullable Separator<S, I, O> sep;
 
+    private int lastNumCRows;
+    private int lastNumSufs;
+
+    private Leaf(int numCRows, int numSufs, List<Integer> cellIds) {
+        super(cellIds);
+        this.lastNumCRows = numCRows;
+        this.lastNumSufs = numSufs;
+    }
+
     /**
-     * Creates split leaf without observations.
+     * Creates split leaf without observations (see {@link Leaf}).
      */
     Leaf() {
-        super(Collections.emptyList());
-        cRow = null;
-        split = true;
-        lastNumCRows = 0;
-        lastNumSufs = 0;
+        this(0, 0, Collections.emptyList());
         // timestamps will be updated automatically
+        cRow = null;
     }
 
     /**
-     * Creates unsplit leaf associated with the given core row and observations.
+     * Creates unsplit leaf associated with the given core row and observations
+     * (see {@link Leaf}).
      */
     Leaf(CoreRow<S, I, O> cRow, int numCRows, int numSufs, List<Integer> cellIds) {
-        super(cellIds);
+        this(numCRows, numSufs, cellIds);
         this.cRow = cRow;
         remRows.set(cRow.idx);
-        split = false;
-        lastNumCRows = numCRows;
-        lastNumSufs = numSufs;
     }
 
+    /**
+     * See {@link Leaf}.
+     */
     boolean isUnsplit() {
-        return !split;
+        return cRow != null;
     }
 
-    void update(List<CoreRow<S, I, O>> cRows, int numSufs) {
+    void update(List<CoreRow<S, I, O>> cRows) {
         assert lastNumCRows <= cRows.size();
         if (lastNumCRows == cRows.size()) {
-            assert lastNumSufs == numSufs;
             return;
-        } else if (numSufs > lastNumSufs) {
+        }
+
+        final int numSufs = cRows.get(0).sufToOut.size();
+        if (numSufs > lastNumSufs) {
             lastNumSufs = numSufs;
             sep = null;
         }
 
-        // Since suffixes and core rows grow monotonically,
+        // since suffixes and core rows grow monotonically,
         // the separator only needs to be recomputed whenever
-        // new compatible core prefixes emerge or the suffix set grows.
+        // new compatible core prefixes emerge or the suffix set grows
 
         for (int i = lastNumCRows; i < cRows.size(); i++) {
             final CoreRow<S, I, O> c = cRows.get(i);
-            if (c.cellIds.containsAll(cellsIds)) {
+            if (c.cellIds.containsAll(cellIds)) {
                 remRows.set(c.idx);
-                split = true;
+                cRow = null; // split leaf
                 sep = null;
             }
         }

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Node.java

@@ -18,25 +18,33 @@
 import java.util.BitSet;
 import java.util.List;
 
+/**
+ * For table compression and to cache suffix selection,
+ * fringe rows do not store observations, but instead map to some node.
+ * Each node is associated with a set of suffix-output pairs,
+ * potentially representing multiple rows with identical observations.
+ * Nodes are either leaves or separators.
+ */
 class Node<S, I, O> { // type parameters required for safe casting
 
     /**
-     * Suffix-output cell identifiers of the fringe rows that share this node.
+     * Identifiers of suffix-output pairs associated with this node.
      */
-    final List<Integer> cellsIds;
+    final List<Integer> cellIds;
 
     /**
-     * Bit vector indicating the core rows that remain compatible
-     * with the observations associated with this node.
+     * Bit vector encoding which core rows remain compatible
+     * with the observations at this node.
+     * Rows are represented by their index.
      */
     final BitSet remRows;
 
-    protected Node(List<Integer> cellsIds) {
-        this(cellsIds, new BitSet());
+    protected Node(List<Integer> cellIds) {
+        this(cellIds, new BitSet());
     }
 
-    protected Node(List<Integer> cellsIds, BitSet remRows) {
-        this.cellsIds = cellsIds;
+    protected Node(List<Integer> cellIds, BitSet remRows) {
+        this.cellIds = cellIds;
         this.remRows = remRows;
     }
 }

algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Separator.java

@@ -22,12 +22,18 @@
 
 import net.automatalib.word.Word;
 
+/**
+ * Separators guide the classification of fringe prefixes.
+ * A separator holds a suffix and a branch map.
+ * The map points to the next node,
+ * depending on the output produced by the suffix.
+ */
 class Separator<S, I, O> extends Node<S, I, O> {
     final Word<I> suffix;
     final Map<Word<O>, Node<S, I, O>> branchMap;
 
-    Separator(Word<I> suffix, BitSet remRows, List<Integer> cells) {
-        super(cells, remRows);
+    Separator(Word<I> suffix, BitSet remRows, List<Integer> cellIds) {
+        super(cellIds, remRows);
         this.suffix = suffix;
         branchMap = new HashMap<>();
     }