From cce1a70a078ffbed236955b93fb60b45c79b7a2a Mon Sep 17 00:00:00 2001 From: vito Date: Wed, 24 Jul 2024 15:33:54 +0200 Subject: [PATCH 01/15] short: - new AdaptiveQuery abstract class with adt and default query extensions - new adaptiveADTOracle classes with parallel interfaces and static implementation - adaptive membership oracle for preset adaptive queries - sleepySUL - changes in ADTLearner class for new Adaptive classes verbose: - added abstract class Adaptive Query in "de.learnlib.query" - added Adaptive_ADT_Query class in "de.learnlib.algorithm.adt.Adaptive" - (added ADTNode getSuccessor() in ADTResetNode ( in "de.learnlib.algorithm.adt.adt" ) for Adaptive_ADT_Query to work ) - added AdaptiveMembershipOracle interface in "de.learnlib.oracle" - added package Adaptive in "de/learnlib/algorithm/adt/Adaptive" - added Sul_Adaptive_Oracle class in "de.learnlib.algorithm.adt.Adaptive" - added Adaptive_DEF_Query class in "de.learnlib.algorithm.adt.Adaptive" - added A2M_Oracle class in "de.learnlib.algorithm.adt.Adaptive" - added ParallelAdaptiveOracle interface in "de.learnlib.oracle" - added StaticParallelAdaptiveOracle in "de.learnlib.oracle.parallelism" - added SleepySUL class in "de.learnlib.algorithm.adt.Adaptive" - modified ADTLearner class: - added constructor for adaptive membership oracle - added AdaptiveMembershipOracle attribute. - modified startLearning() to choose between oracles - added closeTransitionsLeon() method to use appropriate oracles --- .../algorithm/adt/Adaptive/A2M_Oracle.java | 34 +++ .../adt/Adaptive/Adaptive_ADT_Query.java | 240 ++++++++++++++++++ .../adt/Adaptive/Adaptive_DEF_Query.java | 71 ++++++ .../algorithm/adt/Adaptive/SleepySUL.java | 51 ++++ .../adt/Adaptive/Sul_Adaptive_Oracle.java | 55 ++++ .../algorithm/adt/adt/ADTResetNode.java | 4 + .../algorithm/adt/learner/ADTLearner.java | 152 ++++++++++- .../oracle/AdaptiveMembershipOracle.java | 16 ++ .../oracle/ParallelAdaptiveOracle.java | 6 + .../java/de/learnlib/query/AdaptiveQuery.java | 9 + .../StaticParallelAdaptiveOracle.java | 26 ++ 11 files changed, 652 insertions(+), 12 deletions(-) create mode 100644 algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/A2M_Oracle.java create mode 100644 algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_ADT_Query.java create mode 100644 algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_DEF_Query.java create mode 100644 algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/SleepySUL.java create mode 100644 algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Sul_Adaptive_Oracle.java create mode 100644 api/src/main/java/de/learnlib/oracle/AdaptiveMembershipOracle.java create mode 100644 api/src/main/java/de/learnlib/oracle/ParallelAdaptiveOracle.java create mode 100644 api/src/main/java/de/learnlib/query/AdaptiveQuery.java create mode 100644 oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/StaticParallelAdaptiveOracle.java diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/A2M_Oracle.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/A2M_Oracle.java new file mode 100644 index 0000000000..fe0d4a3834 --- /dev/null +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/A2M_Oracle.java @@ -0,0 +1,34 @@ +package de.learnlib.algorithm.adt.Adaptive; + +import de.learnlib.oracle.AdaptiveMembershipOracle; +import de.learnlib.oracle.MembershipOracle; +import de.learnlib.query.AdaptiveQuery; +import de.learnlib.query.Query; +import net.automatalib.word.Word; + +import java.util.ArrayList; +import java.util.Collection; + +public class A2M_Oracle implements MembershipOracle.MealyMembershipOracle { + + private final AdaptiveMembershipOracle oracle; + + public A2M_Oracle(AdaptiveMembershipOracle oracle) { + this.oracle = oracle; + } + + @Override + public void processQueries(Collection>> queries) { + + Collection> adaptiveQueries = new ArrayList<>(); + + for (Query> query : queries) { + Adaptive_DEF_Query adaptive_def_query = + new Adaptive_DEF_Query<>(query); + + adaptiveQueries.add(adaptive_def_query); + + } + this.oracle.processQueries(adaptiveQueries); + } +} diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_ADT_Query.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_ADT_Query.java new file mode 100644 index 0000000000..b668c4cd7a --- /dev/null +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_ADT_Query.java @@ -0,0 +1,240 @@ +package de.learnlib.algorithm.adt.Adaptive; + +import de.learnlib.algorithm.adt.adt.ADTNode; +import de.learnlib.algorithm.adt.adt.ADTResetNode; +import de.learnlib.algorithm.adt.adt.ADTSymbolNode; +import de.learnlib.algorithm.adt.automaton.ADTState; +import de.learnlib.algorithm.adt.automaton.ADTTransition; +import de.learnlib.algorithm.adt.util.ADTUtil; +import de.learnlib.query.AdaptiveQuery; +import net.automatalib.word.Word; + +public class Adaptive_ADT_Query extends AdaptiveQuery { + + //the current ADTNode + ADTNode, I, O> currentADTNode; + + //the transition to close. Will be closed by The Learner after the sifting is completed + ADTTransition transition; + + //the prefix of the target state with the one letter extension + Word longPrefix; + + //index of the current position in the longPrefix. + int lpIndex; + + //flag for initialization. + boolean needsInit; + + boolean needsReset; + + boolean isFinished; + + /* + temporary ADTNode: if an ADT node does not have a successor for some output, the ADT node gets written to + tempADTNode and the ouput gets written to tempOut. + + After sifting, the learner checks if any of these values are uninitialized for each query. + If not, the corresponding ADT entries need to be updated. + */ + + ADTNode, I, O> tempADTNode; + + //outputSymbol of The Node That didn't Have A Successor for this OutputSymbol + O tempOut; + + public Adaptive_ADT_Query(ADTTransition transition, ADTNode,I,O> root ) { + + this.transition = transition; + this.currentADTNode = root; + this.longPrefix = transition.getSource().getAccessSequence().append(transition.getInput()); + this.lpIndex = 0; + this.needsInit = true; + this.needsReset = true; + this.isFinished = false; + } + + @Override + public Boolean getIsFinished() { + return this.isFinished; + } + + @Override + public I getInput() { + return getInputFromCurrentADTNode(); + } + + @Override + public void processOutput( O out ) { + processOutputFromOracle( out ); + } + + + /* + + INPUT FUNTION + + gets the next input symbol from the current ADTNode depending on the node type + + Symbol node: get the Symbol from the Symbol node. + + Reset node: + current node reference stays on a reset node as long as the lp is not fully queried. + the needsReset flag indicates to the Oracle if the SUL still needs a reset. If so, null is + returned to and from the oracle. + Once the lp is queried, the current pointer gets set to the next symbol node after + the reset node + + Leaf node: return null and set the Finished flag + */ + public I getInputFromCurrentADTNode() { + + /* + at first, the transition output needs to be determined. + the lp gets queried, including the transition input ( last symbol of lp ). + + */ + if( this.needsInit ) { + return this.longPrefix.getSymbol(lpIndex); + } + + //if the current node is a symbol node return the associated symbol. + if(ADTUtil.isSymbolNode(currentADTNode)) { + return ((ADTSymbolNode,I,O>)currentADTNode).getSymbol(); + + } else if(ADTUtil.isResetNode(currentADTNode)) { + + if( this.needsReset ) { + this.needsReset = false; + return null; + } else { + I lpChar = this.longPrefix.getSymbol(lpIndex); + lpIndex++; + return lpChar; + } + } else if(ADTUtil.isLeafNode(currentADTNode)) { + + //tells the oracle to stop querying + this.isFinished = true; + return null; + + } else { + throw new IllegalStateException("Tried to access invalid Node Type"); + } + } + + + /* + + OUTPUT FUNCTION + + determines the next ADTNode by picking the child node reachable by the edge labeled with the Output symbol + provided by the oracle. + + the needsInit flag being true, signals that the query is still determining the transition output. + If true, actual sifting has not started yet. + + - accSeq of transition source gets queried + - transition in gets queried + - transitionOut gets set to Oracle answer of transition input. + + Index meaning: + send the symbol of the accSeq Word with index i, as long as i <= accSeq.len + if i is equal to accSeq len, process the transition input. + + for the output function: Oracle outputs before the transition input can be discarded + + */ + + public void processOutputFromOracle( O out ) { + + if( this.needsInit ) { + + if( this.lpIndex == this.transition.getSource().getAccessSequence().length()) { + //query is returned the transition output symbol of the sul + + //TODO: This will be done by the learner eventually + this.transition.setOutput(out); + this.needsInit = false; + this.lpIndex = 0; + + } else { + /* + query is returned null to signal that a character of the long prefix is processed properly. + the output is not relevant and can be discarded + */ + + lpIndex++; + } + + } else if(ADTUtil.isLeafNode(currentADTNode)) { + /* + If the current node is a leaf node, the sifting operation successfully determined a transition + target by reading the associated hypothesis state of the corresponding leaf node. + + There is no need anymore for a sifting operation. + */ + throw new IllegalStateException("there are no successors after final nodes"); + + } else if(ADTUtil.isSymbolNode(currentADTNode)) { + + //new state discovered while sifting + if(currentADTNode.getChildren().get(out) == null) { + + /* + save the ADT node and the output to let the learner fill the holes in the ADT. + This is done this way, to avoid errors with parallel read / write operations. + */ + this.tempOut = out; + this.tempADTNode = currentADTNode; + this.isFinished = true; + + } else { + + //the actual sifting takes place here. + this.currentADTNode = currentADTNode.getChildren().get(out); + + } + } else if(ADTUtil.isResetNode(currentADTNode)) { + + /* + + First we have to check if we are still querying the long prefix. + If so, don't set the current pointer to the next node. + Reset nodes, by definition, only have one successor, so we can just call it after querying the long prefix. + + */ + + if(this.lpIndex == this.longPrefix.length() ) { + this.currentADTNode = ((ADTResetNode)currentADTNode).getSuccessor(); + this.lpIndex = 0; + this.needsReset = true; + } + } else { + throw new IllegalStateException("Tried to access invalid Node Type"); + } + } + + //returns true if a new ADT node was discovered while sifting and the related properties have been set + public boolean needsPostProcessing() { + return (this.tempOut != null && this.tempADTNode != null ); + } + + public ADTNode,I,O> getCurrentADTNode () { + return this.currentADTNode; + } + + public O getTempOut() { + return this.tempOut; + } + + public ADTTransition getTransition() { + return transition; + } + + public Word getLongPrefix() { + return this.longPrefix; + } +} + + diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_DEF_Query.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_DEF_Query.java new file mode 100644 index 0000000000..1c34747557 --- /dev/null +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Adaptive_DEF_Query.java @@ -0,0 +1,71 @@ +package de.learnlib.algorithm.adt.Adaptive; + +import de.learnlib.query.AdaptiveQuery; +import de.learnlib.query.Query; +import net.automatalib.word.Word; +import net.automatalib.word.WordBuilder; + +public class Adaptive_DEF_Query extends AdaptiveQuery { + + private final Query> query; + + WordBuilder builder = new WordBuilder<>(); + + Word output; + + public boolean isFinished; + + int index = 0; + + public Adaptive_DEF_Query(Query> query) { + this.query = query; + this.isFinished = false; + } + + + @Override + public Boolean getIsFinished() { + return this.isFinished; + } + + @Override + public I getInput() { + + Word fullInput = query.getInput(); + + + if( index > fullInput.length() ) { + throw new IllegalStateException("index out of bounds for query"); + } + + if( fullInput.size() == 0 ) { + return null; + } + I inputSymbol = fullInput.getSymbol(index); + index ++; + return inputSymbol; + + } + + @Override + public void processOutput(O out) { + + if( out != null ) { + builder.add( out ); + } else { + query.answer(Word.epsilon()); + this.output = Word.epsilon(); + this.isFinished = true; + } + + if( index == query.getInput().length() && index != 0 ) { + + Word answer = builder.toWord(); + this.output = answer; + query.answer(answer); + + this.isFinished = true; + } + } +} + diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/SleepySUL.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/SleepySUL.java new file mode 100644 index 0000000000..17d28dd9af --- /dev/null +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/SleepySUL.java @@ -0,0 +1,51 @@ +package de.learnlib.algorithm.adt.Adaptive; + +import de.learnlib.sul.SUL; + +public class SleepySUL implements SUL{ + + private final long milis; + private final int nanos; + + private final SUL delegate; + + public SleepySUL(SUL delegate, long milis, int nanos ) { + this.milis = milis; + this.nanos = nanos; + + this.delegate = delegate; + } + + @Override + public void pre() { + + try { + Thread.sleep(milis,nanos); + } catch (InterruptedException e) { + throw new RuntimeException(e); + } + + delegate.pre(); + } + + @Override + public void post() { + delegate.post(); + } + + @Override + public O step(I i) { + return delegate.step( i ); + } + + @Override + public boolean canFork() { + return SUL.super.canFork(); + } + + @Override + public SUL fork() { + return new SleepySUL<>(delegate.fork(),this.milis,this.nanos); + } +} + diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Sul_Adaptive_Oracle.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Sul_Adaptive_Oracle.java new file mode 100644 index 0000000000..cfe322d7c4 --- /dev/null +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/Adaptive/Sul_Adaptive_Oracle.java @@ -0,0 +1,55 @@ +package de.learnlib.algorithm.adt.Adaptive; + +import de.learnlib.oracle.AdaptiveMembershipOracle; +import de.learnlib.query.AdaptiveQuery; +import de.learnlib.sul.SUL; + +import java.util.Collection; + + +/* + Adaptive oracle + - answers queries by means of SUL + - is indifferent to the query type ( default, ADT ) + + */ + +public class Sul_Adaptive_Oracle implements AdaptiveMembershipOracle { + private final SUL sul; + + public Sul_Adaptive_Oracle(SUL sul) { + this.sul = sul; + } + + @Override + public void processQueries(Collection> queries) { + for (AdaptiveQuery query : queries) { + processQuery(query); + } + } + + public void processQuery(AdaptiveQuery query ) { + sul.pre(); + + while (!query.getIsFinished()) { + + I in = query.getInput(); + if (in == null) { + //either reset node or final node + sul.post(); + + //if query is not finished, continue querying + if (!query.getIsFinished()) { + sul.pre(); + query.processOutput(null); + } + } else { + + //query the next symbol of the SUL + O out = sul.step(in); + query.processOutput(out); + } + } + } +} + diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java index c0de4b6eb6..fe2327bb9e 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java @@ -96,4 +96,8 @@ public NodeType getNodeType() { public String toString() { return "reset"; } + + public ADTNode getSuccessor() { + return this.successor; + } } diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java index ad4262044e..186c108fe2 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java @@ -15,21 +15,12 @@ */ package de.learnlib.algorithm.adt.learner; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Collections; -import java.util.Iterator; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Map; -import java.util.Optional; -import java.util.Queue; -import java.util.Set; +import java.util.*; import java.util.stream.Collectors; import de.learnlib.Resumable; import de.learnlib.algorithm.LearningAlgorithm; +import de.learnlib.algorithm.adt.Adaptive.Adaptive_ADT_Query; import de.learnlib.algorithm.adt.adt.ADT; import de.learnlib.algorithm.adt.adt.ADT.LCAInfo; import de.learnlib.algorithm.adt.adt.ADTLeafNode; @@ -52,6 +43,7 @@ import de.learnlib.algorithm.adt.util.SQOOTBridge; import de.learnlib.counterexample.LocalSuffixFinders; import de.learnlib.logging.Category; +import de.learnlib.oracle.AdaptiveMembershipOracle; import de.learnlib.oracle.SymbolQueryOracle; import de.learnlib.query.DefaultQuery; import de.learnlib.tooling.annotation.builder.GenerateBuilder; @@ -92,6 +84,8 @@ public class ADTLearner implements LearningAlgorithm.MealyLearner, private ADTHypothesis hypothesis; private ADT, I, O> adt; + private AdaptiveMembershipOracle adaptiveMembershipOracle; + public ADTLearner(Alphabet alphabet, SymbolQueryOracle oracle, LeafSplitter leafSplitter, @@ -123,6 +117,35 @@ public ADTLearner(Alphabet alphabet, this.adt = new ADT<>(); } + /* + For Integration tests: + - for now you have to give a SQO and an AdaptiveOracle so the stuff does not break. + */ + public ADTLearner(Alphabet alphabet, + SymbolQueryOracle oracle, + AdaptiveMembershipOracle adaptiveMembershipOracle, + LeafSplitter leafSplitter, + ADTExtender adtExtender, + SubtreeReplacer subtreeReplacer, + boolean useObservationTree) { + + this.alphabet = alphabet; + this.observationTree = new ObservationTree<>(this.alphabet); + + this.oracle = new SQOOTBridge<>(this.observationTree, oracle, useObservationTree); + this.adaptiveMembershipOracle = adaptiveMembershipOracle; + + this.leafSplitter = leafSplitter; + this.adtExtender = adtExtender; + this.subtreeReplacer = subtreeReplacer; + + this.hypothesis = new ADTHypothesis<>(this.alphabet); + this.openTransitions = new ArrayDeque<>(); + this.openCounterExamples = new ArrayDeque<>(); + this.allCounterExamples = new LinkedHashSet<>(); + this.adt = new ADT<>(); + } + @Override public void startLearning() { @@ -136,7 +159,12 @@ public void startLearning() { this.openTransitions.add(this.hypothesis.createOpenTransition(initialState, i, this.adt.getRoot())); } - this.closeTransitions(); + //if a parallelOracle is specified, use it to close transitions, otherwise use the old symbolQueryOracle. + if(this.adaptiveMembershipOracle == null ) { + this.closeTransitions(); + } else { + this.closeTransitionsLeon(); + } } @Override @@ -301,6 +329,106 @@ private void closeTransitions() { } } + private void closeTransitionsLeon() { + + while (!this.openTransitions.isEmpty()) { + + Collection> qs = new ArrayList<>(); + + //create a query object for every transition + for( ADTTransition transition : this.openTransitions ) { + + if(!transition.needsSifting()) {continue;} + + ADTNode,I,O> siftNode = transition.getSiftNode(); + + Adaptive_ADT_Query AAQ = new Adaptive_ADT_Query<>( + transition, + siftNode + ); + + qs.add(AAQ); + } + this.openTransitions.clear(); + + //decide which oracles are active and have to answer the queries + if (this.adaptiveMembershipOracle != null){ +// this.adaptiveMembershipOracle.processQueries(queries); + this.adaptiveMembershipOracle.processQueries(qs); + + } else { + throw new IllegalStateException("alle Orakeltypen sind null"); + } + + //fix the ADT Holes by inserting the new nodes here to avoid concurrent writing operations +// for( AdaptiveADTQuery query : queries ) { + + for( Adaptive_ADT_Query query : qs ) { + + if(!query.needsPostProcessing()) { + ADTTransition transition = query.getTransition(); + final ADTState targetState = query.getCurrentADTNode().getHypothesisState(); + transition.setTarget(targetState); + } else { + + ADTNode,I,O> node = query.getCurrentADTNode(); + O out = query.getTempOut(); + + //container for the target state + final ADTState targetState; + + /* + this will be true if this is the first time this pair of ADTNode + and output symbol is seen. Subsequent processing of this pair should + fail since the new ADT node already exists. + */ + if( node.getChildren().get(out) == null ) { + + //create new leaf node + final ADTNode, I, O> result = + new ADTLeafNode<>(node, null); + + //put the new leaf node as child to the parent + node.getChildren().put(out, result); + + //add new state to the hypothesis and set the accessSequence + targetState = this.hypothesis.addState(); + Word longPrefix = query.getLongPrefix(); + targetState.setAccessSequence(longPrefix); + + //set the transition target to the newly created hypothesis state + ADTTransition transition = query.getTransition(); + transition.setTarget(targetState); + + //tell the transition that it is important + transition.setIsSpanningTreeEdge(true); + + //set the hypothesis state of the newly created leaf node to the newly created + //hypothesis state + result.setHypothesisState(targetState); + + //add the observations to the observation tree + O transitionOutput = query.getTransition().getOutput(); + this.observationTree.addState(targetState, longPrefix, transitionOutput); + + for (I i : this.alphabet) { + this.openTransitions.add(this.hypothesis.createOpenTransition(targetState, i, this.adt.getRoot())); + } + } else { + + /* set the transition target to the newly created hypothesis state + this means, that a previous attempt at fixing the ADT holes already + processed this pair of node and output */ + + ADTTransition transition = query.getTransition(); + targetState = node.getChildren().get(out).getHypothesisState(); + transition.setTarget(targetState); + } + } + } + } + } + /** * Close the given transitions by means of sifting the associated long prefix through the ADT. * diff --git a/api/src/main/java/de/learnlib/oracle/AdaptiveMembershipOracle.java b/api/src/main/java/de/learnlib/oracle/AdaptiveMembershipOracle.java new file mode 100644 index 0000000000..c037c96579 --- /dev/null +++ b/api/src/main/java/de/learnlib/oracle/AdaptiveMembershipOracle.java @@ -0,0 +1,16 @@ +package de.learnlib.oracle; + +import de.learnlib.query.AdaptiveQuery; + +import java.util.Collection; + +public interface AdaptiveMembershipOracle extends BatchProcessor> { + + void processQueries(Collection> queries ); + + @Override + default void processBatch(Collection> batch) { + processQueries(batch); + } +} + diff --git a/api/src/main/java/de/learnlib/oracle/ParallelAdaptiveOracle.java b/api/src/main/java/de/learnlib/oracle/ParallelAdaptiveOracle.java new file mode 100644 index 0000000000..be3a45e2ba --- /dev/null +++ b/api/src/main/java/de/learnlib/oracle/ParallelAdaptiveOracle.java @@ -0,0 +1,6 @@ +package de.learnlib.oracle; + +import de.learnlib.oracle.AdaptiveMembershipOracle; + + +public interface ParallelAdaptiveOracle extends ThreadPool, AdaptiveMembershipOracle {} diff --git a/api/src/main/java/de/learnlib/query/AdaptiveQuery.java b/api/src/main/java/de/learnlib/query/AdaptiveQuery.java new file mode 100644 index 0000000000..ce4453207d --- /dev/null +++ b/api/src/main/java/de/learnlib/query/AdaptiveQuery.java @@ -0,0 +1,9 @@ +package de.learnlib.query; + +public abstract class AdaptiveQuery { + + public Boolean getIsFinished (){return false; } ; + public I getInput(){return null;} + + public void processOutput( O out ) {} +} diff --git a/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/StaticParallelAdaptiveOracle.java b/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/StaticParallelAdaptiveOracle.java new file mode 100644 index 0000000000..264942f63d --- /dev/null +++ b/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/StaticParallelAdaptiveOracle.java @@ -0,0 +1,26 @@ +package de.learnlib.oracle.parallelism; + +import de.learnlib.oracle.AdaptiveMembershipOracle; +import de.learnlib.oracle.MembershipOracle; +import de.learnlib.oracle.ParallelAdaptiveOracle; +import de.learnlib.query.AdaptiveQuery; +import de.learnlib.query.Query; +import net.automatalib.word.Word; +import org.checkerframework.checker.index.qual.NonNegative; + +import java.util.Collection; + +public class StaticParallelAdaptiveOracle extends AbstractStaticBatchProcessor, AdaptiveMembershipOracle> + implements ParallelAdaptiveOracle { + + public StaticParallelAdaptiveOracle(Collection> oracles, + @NonNegative int minBatchSize, + PoolPolicy policy) { + super(oracles, minBatchSize, policy); + } + + @Override + public void processQueries(Collection> queries ) { + processBatch(queries); + } +} From ee24333ce931e848cac6c3b08988b143c68d4c29 Mon Sep 17 00:00:00 2001 From: vito Date: Mon, 29 Jul 2024 14:55:55 +0200 Subject: [PATCH 02/15] added contact info to the parent pom.xml --- pom.xml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/pom.xml b/pom.xml index 6868f35c1a..a44381518c 100644 --- a/pom.xml +++ b/pom.xml @@ -137,6 +137,13 @@ limitations under the License. Developer + + Leon Vitorovic + leon.vitorovic@tu-dortmund.de + + Developer + + @{argLine} + --add-reads=de.learnlib.filter.cache=de.learnlib.common.util --add-reads=de.learnlib.filter.cache=de.learnlib.filter.statistic --add-reads=de.learnlib.filter.cache=de.learnlib.oracle.membership --add-reads=de.learnlib.filter.cache=de.learnlib.oracle.parallelism diff --git a/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java b/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java index 4431ade3ce..e8165c266c 100644 --- a/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java +++ b/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java @@ -39,7 +39,6 @@ import net.automatalib.util.automaton.equivalence.NearLinearEquivalenceTest; import net.automatalib.word.Word; import net.automatalib.word.WordBuilder; -import org.checkerframework.checker.nullness.qual.Nullable; /** * A cache for an {@link AdaptiveMembershipOracle}. Upon construction, it is provided with a delegate oracle. Queries @@ -50,7 +49,7 @@ *

* Note that due to the step-wise processing of {@link AdaptiveQuery adaptive queries}, duplicates within a single * {@link BatchProcessor#processBatch(Collection) batch} cannot be cached. If you want to maximize cache efficiency, you - * would have to give up potential parallelization and pose queries one by one. + * would have to give up on potential parallelization and pose queries one by one. * * @param * input symbol type @@ -133,22 +132,16 @@ public void processQueries(Collection> queries) { @Override public EquivalenceOracle, I, Word> createCacheConsistencyTest() { - return this::findCounterexample; - } - - private @Nullable DefaultQuery> findCounterexample(MealyMachine hypothesis, - Collection alphabet) { - /* - TODO: potential optimization: If the hypothesis has undefined transitions, but the cache doesn't, it is a clear - counterexample! - */ - final Word sepWord = NearLinearEquivalenceTest.findSeparatingWord(cache, hypothesis, alphabet, true); + return (hypothesis, alphabet) -> { + //TODO: If the hypothesis has undefined transitions, but the cache doesn't, it is a clear counterexample! + final Word sepWord = NearLinearEquivalenceTest.findSeparatingWord(cache, hypothesis, alphabet, true); - if (sepWord != null) { - return new DefaultQuery<>(sepWord, cache.computeOutput(sepWord)); - } + if (sepWord != null) { + return new DefaultQuery<>(sepWord, cache.computeOutput(sepWord)); + } - return null; + return null; + }; } @Override @@ -166,14 +159,42 @@ public void addAlphabetSymbol(I symbol) { this.cache.addAlphabetSymbol(symbol); } + /** + * Returns a (structural) view of the cache in form of a {@link MealyMachine}. + * + * @return a view of the cache + */ public MealyMachine getCache() { return this.cache; } + /** + * Inserts the given trace of input symbols and associates the trace of given output symbols with it. + * + * @param input + * the sequence of input symbols + * @param output + * the sequence of output symbols + * + * @return the identifier of the state reached by the input sequence + */ public Integer insert(Word input, Word output) { return insert(this.cache.getInitialState(), input, output); } + /** + * Inserts the given trace of input symbols at the given cache state and associates the trace of given output + * symbols with it. + * + * @param state + * the (cache) state at which the traces should be inserted + * @param input + * the sequence of input symbols + * @param output + * the sequence of output symbols + * + * @return the identifier of the state reached by the input sequence + */ public Integer insert(Integer state, Word input, Word output) { assert input.length() == output.length(); diff --git a/filters/cache/src/test/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCacheTest.java b/filters/cache/src/test/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCacheTest.java index b28861ff00..039c7d109f 100644 --- a/filters/cache/src/test/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCacheTest.java +++ b/filters/cache/src/test/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCacheTest.java @@ -28,8 +28,8 @@ import de.learnlib.oracle.EquivalenceOracle; import de.learnlib.oracle.membership.SULAdaptiveOracle; import de.learnlib.query.AdaptiveQuery; -import de.learnlib.query.PresetAdaptiveQuery; import de.learnlib.query.Query; +import de.learnlib.util.mealy.PresetAdaptiveQuery; import net.automatalib.alphabet.Alphabet; import net.automatalib.alphabet.SupportsGrowingAlphabet; import net.automatalib.alphabet.impl.GrowingMapAlphabet; diff --git a/oracles/membership-oracles/src/main/java/de/learnlib/oracle/membership/SULAdaptiveOracle.java b/oracles/membership-oracles/src/main/java/de/learnlib/oracle/membership/SULAdaptiveOracle.java index 1fe12173a2..e4e636c149 100644 --- a/oracles/membership-oracles/src/main/java/de/learnlib/oracle/membership/SULAdaptiveOracle.java +++ b/oracles/membership-oracles/src/main/java/de/learnlib/oracle/membership/SULAdaptiveOracle.java @@ -15,11 +15,22 @@ */ package de.learnlib.oracle.membership; +import de.learnlib.oracle.AdaptiveMembershipOracle; import de.learnlib.oracle.SingleAdaptiveMembershipOracle; import de.learnlib.query.AdaptiveQuery; import de.learnlib.query.AdaptiveQuery.Response; import de.learnlib.sul.SUL; +/** + * A wrapper that allows to use a {@link SUL} where a {@link AdaptiveMembershipOracle} is expected. + *

+ * This oracle is not thread-safe. + * + * @param + * input alphabet type + * @param + * output alphabet type + */ public class SULAdaptiveOracle implements SingleAdaptiveMembershipOracle { private final SUL sul; diff --git a/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/DynamicParallelAdaptiveOracle.java b/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/DynamicParallelAdaptiveOracle.java index db114d2105..92b5c0585a 100644 --- a/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/DynamicParallelAdaptiveOracle.java +++ b/oracles/parallelism/src/main/java/de/learnlib/oracle/parallelism/DynamicParallelAdaptiveOracle.java @@ -21,13 +21,12 @@ import de.learnlib.oracle.AdaptiveMembershipOracle; import de.learnlib.oracle.ParallelAdaptiveOracle; -import de.learnlib.oracle.ParallelOracle; import de.learnlib.query.AdaptiveQuery; import org.checkerframework.checker.index.qual.NonNegative; /** * A specialized {@link AbstractDynamicBatchProcessor} for {@link AdaptiveMembershipOracle}s that implements - * {@link ParallelOracle}. + * {@link ParallelAdaptiveOracle}. * * @param * input symbol type diff --git a/pom.xml b/pom.xml index a44381518c..da3617a7c6 100644 --- a/pom.xml +++ b/pom.xml @@ -129,17 +129,18 @@ limitations under the License. - Stephan Windmüller - stephan.windmueller@tu-dortmund.de + Leon Vitorovic TU Dortmund University, Chair of Programming Systems - http://ls5-www.cs.tu-dortmund.de/ + leon.vitorovic@tu-dortmund.de - Developer + Developer (Graduate) - Leon Vitorovic - leon.vitorovic@tu-dortmund.de + Stephan Windmüller + stephan.windmueller@tu-dortmund.de + TU Dortmund University, Chair of Programming Systems + http://ls5-www.cs.tu-dortmund.de/ Developer From 836a667a3da81b01fadb323995c218b2b7a9727b Mon Sep 17 00:00:00 2001 From: Markus Frohme Date: Tue, 20 Aug 2024 15:07:56 +0200 Subject: [PATCH 14/15] update CHANGELOG --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6508f5bceb..5a6d521523 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * LearnLib now supports JPMS modules. All artifacts now provide a `module-info` descriptor except of the distribution artifacts (for Maven-less environments) which only provide an `Automatic-Module-Name` due to non-modular dependencies. Note that while this is a Java 9+ feature, LearnLib still supports Java 8 byte code for the remaining class files. * Added an `InterningMembershipOracle` (including refinements) to the `learnlib-cache` artifact that interns query responses to reduce memory consumption of large data structures. This exports the internal concepts of the DHC learner (which no longer interns query responses automatically). +* The `ADTLearner` has been refactored to longer use the (now-removed) `SymbolQueryOracle` but a new `AdaptiveMembershipOracle` instead which supports answering queries in parallel (thanks to [Leon Vitorovic](https://github.com/leonthalee)). ### Changed @@ -30,6 +31,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * The `de.learnlib.tooling:learnlib-annotation-processor` artifact has been dropped. The functionality has been moved to a [standalone project](https://github.com/LearnLib/build-tools). * The `de.learnlib:learnlib-rpni-edsm` and `de.learnlib:learnlib-rpni-mdl` artifacts have been dropped. The code has been merged with the `de.learnlib:learnlib-rpni` artifact. * `PropertyOracle`s can no longer set a property. This value is now immutable and must be provided during instantiation. Previously, the internal state wasn't updated accordingly if a property was overridden. +* `SymbolQueryOracle`s (and related code such as the respective caches, counters, etc.) have been removed without replacement. Equivalent functionality on the basis of the new `AdaptiveMembershipOracle`s is available instead. ## [0.17.0] - 2023-11-15 From ce66855a5d4722f684c45aebe4af5d7ecd2fd94d Mon Sep 17 00:00:00 2001 From: Markus Frohme Date: Thu, 22 Aug 2024 11:10:11 +0200 Subject: [PATCH 15/15] remove obsolete method --- .../main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java index e33336d930..c4c2c9ec2f 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java @@ -83,8 +83,4 @@ public NodeType getNodeType() { public String toString() { return "reset"; } - - public ADTNode getSuccessor() { - return this.successor; - } }