diff --git a/CHANGELOG.md b/CHANGELOG.md index 1a3d68f22..9cf2b715a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +* Added the Ls active learning algorithm (thanks to [Wolffhardt Schwabe](https://github.com/stateMachinist)). * Added an `EarlyExitEQOracle` which for a given `AdaptiveMembershipOracle` and `TestWordGenerator` stops the evaluation of (potentially long) Mealy-based equivalence tests as soon as a mismatch with the hypothesis is detected, potentially improving the symbol performance of the given equivalence oracle. ### Changed diff --git a/README.md b/README.md index dd2610ed6..66f6bb6d2 100644 --- a/README.md +++ b/README.md @@ -24,6 +24,7 @@ Currently, the following learning algorithms with respective target models are s | DHC | `Mealy` | | | | | Kearns & Vazirani | `DFA` `Mealy` | | | | | Lambda | `DFA` `Mealy` | | | | +| Ls | `Mealy` | | | | | L# | `Mealy` | | | | | L* (incl. variants) | `DFA` `Mealy` `Moore` | | | | | NL* | `NFA` | | | | diff --git a/algorithms/active/pom.xml b/algorithms/active/pom.xml index 26f706662..7578c4742 100644 --- a/algorithms/active/pom.xml +++ b/algorithms/active/pom.xml @@ -43,6 +43,7 @@ limitations under the License. observation-pack observation-pack-vpa procedural + sparse ttt ttt-vpa diff --git a/algorithms/active/sparse/pom.xml b/algorithms/active/sparse/pom.xml new file mode 100644 index 000000000..65f3616e2 --- /dev/null +++ b/algorithms/active/sparse/pom.xml @@ -0,0 +1,77 @@ + + + + 4.0.0 + + + de.learnlib + learnlib-algorithms-active-parent + 0.19.0-SNAPSHOT + ../pom.xml + + + learnlib-sparse + + LearnLib :: Algorithms :: Sparse + + This artifact provides the implementation of the Sparse OT learning algorithm as described in the paper + "Learning Mealy Machines with Sparse Observation Tables" (https://doi.org/10.1007/978-3-032-05792-1_10) by + Wolffhardt Schwabe, Paul Kogel, and Sabine Glesner. + + + + + + de.learnlib + learnlib-api + + + de.learnlib + learnlib-counterexamples + + + de.learnlib + learnlib-util + + + + + net.automatalib + automata-api + + + net.automatalib + automata-commons-util + + + net.automatalib + automata-core + + + + org.checkerframework + checker-qual + + + + + de.learnlib.testsupport + learnlib-learner-it-support + + + diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/CoreRow.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/CoreRow.java new file mode 100644 index 000000000..cbd32de1a --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/CoreRow.java @@ -0,0 +1,65 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import net.automatalib.word.Word; + +/** + * Each core row represents some hypothesis state + * and stores its outputs for all table suffixes. + */ +class CoreRow extends Row { + + /** + * Hypothesis state associated with this row. + */ + final S state; + + /** + * Index of this row in the core row list. + * Used as a unique address. + */ + final int idx; + + /** + * Maps suffixes to their outputs. + */ + final Map, Word> sufToOut; + + /** + * Identifiers of all suffix-output pairs in this row, + * used for fast compatibility checking. + */ + final Set cellIds; + + CoreRow(Word prefix, S state, int idx) { + super(prefix); + this.state = state; + this.idx = idx; + sufToOut = new HashMap<>(); + cellIds = new HashSet<>(); // use HashSet for fast containment checks + } + + void addSuffix(Word suf, Word out, int cell) { + sufToOut.put(suf, out); + cellIds.add(cell); + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/FringeRow.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/FringeRow.java new file mode 100644 index 000000000..dcf88e56e --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/FringeRow.java @@ -0,0 +1,61 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import net.automatalib.word.Word; + +/** + * Each fringe row represents some hypothesis transition + * outside the spanning tree defined by the core prefixes. + * + * @param + * state type + * @param + * input symbol type + * @param + * output symbol type + */ +class FringeRow extends Row { + + /** + * Source state. + */ + final S srcState; + + /** + * Input symbol. + */ + final I transIn; + + /** + * Output symbol (determined lazily). + */ + O transOut; + + /** + * For compression, fringe rows do not store observations directly. + * Instead, they point to some leaf in a tree encoding their classification history. + * This trick avoids redundantly storing identical observations. + */ + Leaf leaf; + + FringeRow(Word prefix, S srcState, Leaf leaf) { + super(prefix); + this.srcState = srcState; + this.transIn = prefix.lastSymbol(); + this.leaf = leaf; + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/GenericSparseLearner.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/GenericSparseLearner.java new file mode 100644 index 000000000..f9c805ddf --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/GenericSparseLearner.java @@ -0,0 +1,372 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Collections; +import java.util.Deque; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.Function; +import java.util.stream.Collectors; + +import de.learnlib.algorithm.LearningAlgorithm.MealyLearner; +import de.learnlib.counterexample.LocalSuffixFinders; +import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle; +import de.learnlib.query.DefaultQuery; +import de.learnlib.util.mealy.MealyUtil; +import net.automatalib.alphabet.Alphabet; +import net.automatalib.automaton.transducer.MealyMachine; +import net.automatalib.automaton.transducer.MutableMealyMachine; +import net.automatalib.common.util.Pair; +import net.automatalib.word.Word; + +class GenericSparseLearner implements MealyLearner { + + private final Alphabet alphabet; + private final MealyMembershipOracle oracle; + + /** + * Suffixes. + */ + private final Deque> sufs; + + /** + * List of core rows. Rows can be addressed by their index in this list. + */ + private final List> cRows; + + /** + * Fringe rows (stored in a stack for LIFO iteration). + */ + private final Deque> fRows; + + /** + * Maps fringe prefixes to rows. + */ + private final Map, FringeRow> prefToFringe; + + /** + * List of unique suffix-output pairs, addressable by index. + * Used for table compression: table entries only hold cell index. + */ + private final List, Word>> cells; + + /** + * Maps each suffix-output pair to its index (see {@link #cells}). + */ + private final Map, Word>, Integer> cellToIdx; + + /** + * Hypothesis. + */ + private final MutableMealyMachine hyp; + + /** + * Maps each state to its core row prefix. + */ + private final Map> stateToPrefix; + + /** + * Computes access sequences. + */ + private final Function, Word> accSeq; + + /** + * For fast suffix ranking, this map stores the core row partitions created by each suffix. + */ + private final Map, List> sufToVecs; + + /** + * Helper map for efficiently constructing the suffix partition map (see {@link #sufToVecs}). + */ + private final Map, Map, Integer>> sufToOutToIdx; + + protected GenericSparseLearner(Alphabet alphabet, + MealyMembershipOracle oracle, + List> initialSuffixes, + MutableMealyMachine emptyMachine) { + this.alphabet = alphabet; + this.oracle = oracle; + sufs = new ArrayDeque<>(initialSuffixes); + cRows = new ArrayList<>(); + fRows = new ArrayDeque<>(); + prefToFringe = new HashMap<>(); + cells = new ArrayList<>(); + cellToIdx = new HashMap<>(); + hyp = emptyMachine; + stateToPrefix = new HashMap<>(); + accSeq = p -> stateToPrefix.get(hyp.getState(p)); + sufToVecs = new HashMap<>(); + sufToOutToIdx = new HashMap<>(); + } + + @Override + public MealyMachine getHypothesisModel() { + return hyp; + } + + @Override + public void startLearning() { + final S init = hyp.addInitialState(); + final CoreRow c = new CoreRow<>(Word.epsilon(), init, 0); + cRows.add(c); + sufs.forEach(s -> addSuffixToCoreRow(c, s)); + stateToPrefix.put(init, c.prefix); + extendFringe(c, init, new Leaf<>(c, 1, sufs.size(), Collections.emptyList())); + fRows.forEach(f -> query(f, Word.epsilon())); // query transition outputs + // initially, transition outputs must be queried manually, + // for later transitions, they derive from suffix queries + updateHypothesis(); + } + + @Override + public boolean refineHypothesis(DefaultQuery> q) { + final DefaultQuery> qs = MealyUtil.shortenCounterExample(hyp, q); + if (qs == null) { + return false; + } + + final int oldSize = hyp.size(); + identifyNewState(qs); + assert hyp.size() > oldSize; + updateHypothesis(); + assert hyp.size() == cRows.size(); + refineHypothesis(q); // recursively exhaust counterexample + return true; + } + + private void updateHypothesis() { + for (FringeRow f : fRows) { + classifyFringePrefix(f); + if (f.leaf == null) { + 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 f) { + f.leaf.update(cRows); + if (f.leaf.isUnsplit()) { + return; + } + + final Separator sep = f.leaf.sep; + if (sep != null) { + followNode(f, sep); + } else { + f.leaf.sep = new Separator<>(pickSuffix(f.leaf.remRows), f.leaf.remRows, f.leaf.cellIds); + followNode(f, f.leaf.sep); + } + } + + private Word pickSuffix(BitSet remRows) { + assert remRows.length() <= cRows.size(); + Word bestSuf = sufs.getFirst(); + int bestRank = Integer.MAX_VALUE; + final BitSet vec = new BitSet(); + for (Word s : sufs) { + int maxOccur = 0; + int sumOccur = 0; // checksum + for (BitSet rows : sufToVecs.get(s)) { + vec.or(remRows); + vec.and(rows); + final int occur = vec.cardinality(); + maxOccur = Math.max(maxOccur, occur); + sumOccur += occur; + } + + assert sumOccur == remRows.cardinality(); + if (maxOccur < bestRank) { + // among equally ranked suffixes, pick youngest + // (mind that suffixes are stored/iterated LIFO) + bestSuf = s; + bestRank = maxOccur; + if (bestRank == 1) { // optimization: no better suffix is possible + return bestSuf; + } + } + } + + assert bestRank < remRows.cardinality(); + return bestSuf; + } + + private void followNode(FringeRow f, Node n) { + if (n instanceof Leaf) { // TODO simplify when switching to newer java + final Leaf l = (Leaf) n; + assert l.isUnsplit(); + f.leaf = l; + return; + } + + final Separator sep = (Separator) n; + final Word out = query(f, sep.suffix); + final int cellIdx = getUniqueCellIdx(sep.suffix, out); + final Node next = sep.branchMap.get(out); + if (next != null) { + followNode(f, next); + return; + } + + final BitSet remRows = new BitSet(); + sep.remRows.stream().filter(i -> cRows.get(i).cellIds.contains(cellIdx)).forEach(remRows::set); + final List cellIds = new ArrayList<>(sep.cellIds); // important: copy elements! + cellIds.add(cellIdx); + if (remRows.isEmpty()) { + // no compatible core prefix + f.leaf = null; + moveToCore(f, cellIds); + } else if (remRows.cardinality() == 1) { + final Leaf l = new Leaf<>(cRows.get(remRows.nextSetBit(0)), cRows.size(), sufs.size(), cellIds); + sep.branchMap.put(out, l); + followNode(f, l); + } else { + final Separator s = new Separator<>(pickSuffix(remRows), remRows, cellIds); + sep.branchMap.put(out, s); + followNode(f, s); + } + } + + private Word query(Row r, Word suf) { + final Word out = oracle.answerQuery(r.prefix.concat(suf)); + if (r instanceof FringeRow) { // TODO simplify when switching to newer java + final FringeRow f = (FringeRow) r; + f.transOut = out.prefix(f.prefix.length()).lastSymbol(); + } + + return out.suffix(suf.length()); + } + + /** + * Adds suffix-output pair to index if not yet contained, + * and returns a unique identifier representing the pair. + */ + private int getUniqueCellIdx(Word suf, Word out) { + assert suf.length() == out.length(); + final Pair, Word> cell = Pair.of(suf, out); + final int idx = cellToIdx.computeIfAbsent(cell, c -> cellToIdx.size()); + if (idx == cells.size()) { + cells.add(cell); + } + + assert cellToIdx.size() == cells.size(); + return idx; + } + + /** + * Returns index of new core row. + */ + private int moveToCore(FringeRow f, List cellIds) { + final boolean removed = fRows.remove(f); + assert removed; + final S state = hyp.addState(); + final CoreRow c = new CoreRow<>(f.prefix, state, cRows.size()); + stateToPrefix.put(state, c.prefix); + assert f.transOut != null; + hyp.setTransition(f.srcState, f.transIn, state, f.transOut); + for (Integer cellIdx : completeRowObservations(f, cellIds)) { + final Pair, Word> cell = this.cells.get(cellIdx); + addCellToCoreRow(c, cell.getFirst(), cell.getSecond(), cellIdx); + } + + cRows.add(c); + extendFringe(c, state, new Leaf<>()); + assert c.cellIds.size() == sufs.size(); + assert c == cRows.get(c.idx); + return c.idx; + } + + /** + * Takes fringe row and its observations, queries the missing entries, + * and returns a list containing the observations for all suffixes. + */ + private List completeRowObservations(FringeRow f, List cellIds) { + // TODO simplify collector calls when switching to newer java + final List> sufsPresent = cellIds.stream().map(c -> this.cells.get(c).getFirst()).collect(Collectors.toList()); + final List> sufsMissing = sufs.stream().filter(s -> !sufsPresent.contains(s)).collect(Collectors.toList()); + final List cellIdsFull = new ArrayList<>(cellIds); // important: copy elements! + sufsMissing.forEach(s -> cellIdsFull.add(getUniqueCellIdx(s, query(f, s)))); + return cellIdsFull; + } + + private void extendFringe(CoreRow c, S state, Leaf leaf) { + for (I i : alphabet) { + // add missing fringe rows for new transitions + final Word prefix = c.prefix.append(i); + final FringeRow fRow = new FringeRow<>(prefix, state, leaf); + prefToFringe.put(prefix, fRow); + fRows.push(fRow); // prioritize new rows during classification + } + } + + private void identifyNewState(DefaultQuery> q) { + final Word cex = q.getInput(); + final int idxSuf = LocalSuffixFinders.findRivestSchapire(q, accSeq::apply, hyp, oracle); + final int idxSym = idxSuf - 1; + final Word u = accSeq.apply(cex.prefix(idxSym)); + final Word ui = u.append(cex.getSymbol(idxSym)); + final FringeRow f = prefToFringe.get(ui); + 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)); + } + } + + private void addSuffixToTable(Word suf) { + assert !sufs.contains(suf); + sufs.push(suf); + + // since core rows are prefix-closed, + // cache hit rate is maximized by LIFO iteration + for (int i = cRows.size() - 1; i >= 0; i--) { + addSuffixToCoreRow(cRows.get(i), suf); + } + } + + private void addSuffixToCoreRow(CoreRow c, Word suf) { + final Word out = query(c, suf); + final int cellIdx = getUniqueCellIdx(suf, out); + addCellToCoreRow(c, suf, out, cellIdx); + } + + private void addCellToCoreRow(CoreRow c, Word suf, Word out, Integer cellIdx) { + c.addSuffix(suf, out, cellIdx); + updatePartitionMap(c, suf, out); + } + + private void updatePartitionMap(CoreRow c, Word suf, Word out) { + final Map, Integer> outToIdx = sufToOutToIdx.computeIfAbsent(suf, s -> new HashMap<>()); + final int idx = outToIdx.computeIfAbsent(out, o -> outToIdx.size()); + final List vecs = sufToVecs.computeIfAbsent(suf, s -> new ArrayList<>()); + assert idx <= vecs.size(); + if (idx == vecs.size()) { + vecs.add(new BitSet()); + } + + vecs.get(idx).set(c.idx); + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Leaf.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Leaf.java new file mode 100644 index 000000000..8ccfba23d --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Leaf.java @@ -0,0 +1,108 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import java.util.Collections; +import java.util.List; + +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 extends Node { + + /** + * Core row associated with this leaf (null if split, see {@link Leaf}). + */ + @Nullable CoreRow cRow; + + /** + * Separator cached by this leaf (see {@link Leaf}). + */ + @Nullable Separator sep; + + private int lastNumCRows; + private int lastNumSufs; + + private Leaf(int numCRows, int numSufs, List cellIds) { + super(cellIds); + this.lastNumCRows = numCRows; + this.lastNumSufs = numSufs; + } + + /** + * Creates split leaf without observations (see {@link Leaf}). + */ + Leaf() { + this(0, 0, Collections.emptyList()); + // timestamps will be updated automatically + cRow = null; + } + + /** + * Creates unsplit leaf associated with the given core row and observations + * (see {@link Leaf}). + */ + Leaf(CoreRow cRow, int numCRows, int numSufs, List cellIds) { + this(numCRows, numSufs, cellIds); + this.cRow = cRow; + remRows.set(cRow.idx); + } + + /** + * See {@link Leaf}. + */ + boolean isUnsplit() { + return cRow != null; + } + + void update(List> cRows) { + assert lastNumCRows <= cRows.size(); + if (lastNumCRows == cRows.size()) { + return; + } + + final int numSufs = cRows.get(0).sufToOut.size(); + if (numSufs > lastNumSufs) { + lastNumSufs = numSufs; + sep = null; + } + + // 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 + + for (int i = lastNumCRows; i < cRows.size(); i++) { + final CoreRow c = cRows.get(i); + if (c.cellIds.containsAll(cellIds)) { + remRows.set(c.idx); + cRow = null; // split leaf + sep = null; + } + } + + lastNumCRows = cRows.size(); + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Node.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Node.java new file mode 100644 index 000000000..12ac68ba1 --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Node.java @@ -0,0 +1,50 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +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 { // type parameters required for safe casting + + /** + * Identifiers of suffix-output pairs associated with this node. + */ + final List cellIds; + + /** + * 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 cellIds) { + this(cellIds, new BitSet()); + } + + protected Node(List cellIds, BitSet remRows) { + this.cellIds = cellIds; + this.remRows = remRows; + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Row.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Row.java new file mode 100644 index 000000000..26ee62442 --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Row.java @@ -0,0 +1,26 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import net.automatalib.word.Word; + +class Row { // type parameters required for safe casting + final Word prefix; + + protected Row(Word prefix) { + this.prefix = prefix; + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Separator.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Separator.java new file mode 100644 index 000000000..d2a231f24 --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/Separator.java @@ -0,0 +1,40 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import java.util.BitSet; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +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 extends Node { + final Word suffix; + final Map, Node> branchMap; + + Separator(Word suffix, BitSet remRows, List cellIds) { + super(cellIds, remRows); + this.suffix = suffix; + branchMap = new HashMap<>(); + } +} diff --git a/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/SparseLearner.java b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/SparseLearner.java new file mode 100644 index 000000000..ec500d666 --- /dev/null +++ b/algorithms/active/sparse/src/main/java/de/learnlib/algorithm/sparse/SparseLearner.java @@ -0,0 +1,40 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse; + +import java.util.Collections; +import java.util.List; + +import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle; +import net.automatalib.alphabet.Alphabet; +import net.automatalib.automaton.transducer.impl.CompactMealy; +import net.automatalib.word.Word; + +/** + * Optimized implementation of the Ls learning algorithm, as described in the paper + * Learning Mealy Machines with Sparse Observation Tables + * by Wolffhardt Schwabe, Paul Kogel, and Sabine Glesner. + */ +public class SparseLearner extends GenericSparseLearner { + + public SparseLearner(Alphabet alphabet, MealyMembershipOracle oracle) { + this(alphabet, oracle, Collections.emptyList()); + } + + public SparseLearner(Alphabet alphabet, MealyMembershipOracle oracle, List> initialSuffixes) { + super(alphabet, oracle, initialSuffixes, new CompactMealy<>(alphabet)); + } +} diff --git a/algorithms/active/sparse/src/main/java/module-info.java b/algorithms/active/sparse/src/main/java/module-info.java new file mode 100644 index 000000000..308fe8fe7 --- /dev/null +++ b/algorithms/active/sparse/src/main/java/module-info.java @@ -0,0 +1,44 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +/** + * This module provides the implementation of the Sparse OT learning algorithm as described in the paper + * Learning Mealy Machines with Sparse Observation Tables + * by Wolffhardt Schwabe, Paul Kogel, and Sabine Glesner. + *

+ * This module is provided by the following Maven dependency: + * 

+ * <dependency>
+ *   <groupId>de.learnlib</groupId>
+ *   <artifactId>learnlib-sparse</artifactId>
+ *   <version>${version}</version>
+ * </dependency>
+ *
+ */ +open module de.learnlib.algorithm.sparse { + + requires de.learnlib.common.counterexample; + requires de.learnlib.common.util; + requires de.learnlib.api; + requires net.automatalib.core; + requires net.automatalib.api; + requires net.automatalib.common.util; + + // annotations are 'provided'-scoped and do not need to be loaded at runtime + requires static org.checkerframework.checker.qual; + + exports de.learnlib.algorithm.sparse; +} diff --git a/algorithms/active/sparse/src/test/java/de/learnlib/algorithm/sparse/it/SparseIT.java b/algorithms/active/sparse/src/test/java/de/learnlib/algorithm/sparse/it/SparseIT.java new file mode 100644 index 000000000..82129ba06 --- /dev/null +++ b/algorithms/active/sparse/src/test/java/de/learnlib/algorithm/sparse/it/SparseIT.java @@ -0,0 +1,33 @@ +/* Copyright (C) 2013-2025 TU Dortmund University + * This file is part of LearnLib . + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package de.learnlib.algorithm.sparse.it; + +import de.learnlib.algorithm.sparse.SparseLearner; +import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle; +import de.learnlib.testsupport.it.learner.AbstractMealyLearnerIT; +import de.learnlib.testsupport.it.learner.LearnerVariantList; +import net.automatalib.alphabet.Alphabet; + +public class SparseIT extends AbstractMealyLearnerIT { + + @Override + protected void addLearnerVariants(Alphabet alphabet, + int targetSize, + MealyMembershipOracle mqOracle, + LearnerVariantList.MealyLearnerVariantList variants) { + variants.addLearnerVariant("sparse", new SparseLearner<>(alphabet, mqOracle)); + } +} diff --git a/distribution/pom.xml b/distribution/pom.xml index aa0c421c8..7f41f7d72 100644 --- a/distribution/pom.xml +++ b/distribution/pom.xml @@ -102,6 +102,11 @@ limitations under the License. learnlib-procedural + + de.learnlib + learnlib-sparse + + de.learnlib learnlib-ttt @@ -354,6 +359,13 @@ limitations under the License. sources + + de.learnlib + learnlib-sparse + ${project.version} + sources + + de.learnlib learnlib-ttt diff --git a/pom.xml b/pom.xml index 6245bdfce..3fcf1f368 100644 --- a/pom.xml +++ b/pom.xml @@ -153,6 +153,15 @@ limitations under the License. Developer + + Wolffhardt Schwabe + schwabe@tu-berlin.de + TU Berlin, Software and Embedded Systems Engineering + https://tu.berlin/sese/ + + Developer + +