From d07714509ea38ecd1779b37ff15fa772faacff40 Mon Sep 17 00:00:00 2001 From: mtf90 Date: Tue, 26 Sep 2023 11:14:09 +0200 Subject: [PATCH] Re-integrate the work on procedural systems (#93) * initial import of SBAs and SPMMs * cleanups / refactorings * refactorings * adjust to Automatalib refactorings * add procedural W-method oracles * make SBA/SPMM learner add non-continuable symbols lazily * make counterexample analysis parameterizable * add adapters for OML and DHC * Only use DHC for testing Since the adapter does not provide any functionality, skip redundant adapter class. * adjust to AutomataLib refactorings * add documentation * add some assertions for convenience * add SBA-based palindrome learning example * cleanup (mostly docs) * cleanups + some more tests --- CHANGELOG.md | 2 +- README.md | 2 +- algorithms/active/pom.xml | 2 +- algorithms/active/{spa => procedural}/pom.xml | 29 +- .../algorithms/procedural/SymbolWrapper.java | 48 +++ .../dfa/DiscriminationTreeAdapterDFA.java} | 8 +- .../dfa/KearnsVaziraniAdapterDFA.java} | 8 +- .../adapter/dfa/LStarBaseAdapterDFA.java} | 8 +- .../adapter/dfa/OptimalTTTAdapterDFA.java | 49 +++ .../dfa/RivestSchapireAdapterDFA.java} | 8 +- .../adapter/dfa/TTTAdapterDFA.java} | 8 +- .../mealy/DiscriminationTreeAdapterMealy.java | 45 +++ .../mealy/KearnsVaziraniAdapterMealy.java | 53 +++ .../adapter/mealy/LStarBaseAdapterMealy.java | 69 ++++ .../adapter/mealy/OptimalTTTAdapterMealy.java | 51 +++ .../mealy/RivestSchapireAdapterMealy.java | 63 +++ .../adapter/mealy/TTTAdapterMealy.java | 50 +++ .../algorithms/procedural/sba/ATManager.java | 90 +++++ .../algorithms/procedural/sba/MappingSBA.java | 114 ++++++ .../sba/ProceduralMembershipOracle.java | 127 ++++++ .../algorithms/procedural/sba/SBALearner.java | 362 +++++++++++++++++ .../sba/manager/DefaultATManager.java | 101 +++++ .../sba/manager/OptimizingATManager.java | 255 ++++++++++++ .../algorithms/procedural/spa/ATRManager.java | 99 +++++ .../spa/ProceduralMembershipOracle.java | 19 +- .../procedural}/spa/SPALearner.java | 179 +++++---- .../spa/manager/DefaultATRManager.java | 25 +- .../spa/manager/OptimizingATRManager.java | 32 +- .../algorithms/procedural/spmm/ATManager.java | 93 +++++ .../procedural/spmm/MappingSPMM.java | 135 +++++++ .../spmm/ProceduralMembershipOracle.java | 163 ++++++++ .../procedural/spmm/SPMMLearner.java | 367 ++++++++++++++++++ .../spmm/manager/DefaultATManager.java | 112 ++++++ .../spmm/manager/OptimizingATManager.java | 272 +++++++++++++ .../procedural/sba/ATManagerTest.java | 62 +++ .../procedural/sba/OptimizationsTest.java | 70 ++++ .../algorithms/procedural/sba/it/SBAIT.java | 90 +++++ .../procedural}/spa/ATRManagerTest.java | 14 +- .../algorithms/procedural/spa/it/SPAIT.java | 92 +++++ .../procedural/spmm/ATManagerTest.java | 67 ++++ .../procedural/spmm/OptimizationsTest.java | 72 ++++ .../algorithms/procedural/spmm/it/SPMMIT.java | 97 +++++ .../learnlib/algorithms/spa/ATRManager.java | 40 -- .../de/learnlib/algorithms/spa/SPAIT.java | 80 ---- distribution/pom.xml | 4 +- .../equivalence/sba/SimulatorEQOracle.java | 57 +++ .../equivalence/sba/WMethodEQOracle.java | 110 ++++++ .../equivalence/spa/SimulatorEQOracle.java | 10 +- ...dSPAEQOracle.java => WMethodEQOracle.java} | 40 +- ...SPAEQOracle.java => WpMethodEQOracle.java} | 38 +- .../equivalence/spmm/SimulatorEQOracle.java | 58 +++ .../equivalence/spmm/WMethodEQOracle.java | 111 ++++++ .../equivalence/sba/WMethodEQOracleTest.java | 54 +++ ...acleTest.java => WMethodEQOracleTest.java} | 18 +- ...cleTest.java => WpMethodEQOracleTest.java} | 18 +- .../equivalence/spmm/WMethodEQOracleTest.java | 62 +++ pom.xml | 2 +- .../it/learner/AbstractSBALearnerIT.java | 77 ++++ .../it/learner/AbstractSPALearnerIT.java | 13 +- .../it/learner/AbstractSPMMLearnerIT.java | 79 ++++ .../testsupport/it/learner/LearnerITUtil.java | 40 +- .../it/learner/LearnerVariantList.java | 12 +- .../it/learner/LearnerVariantListImpl.java | 10 +- .../it/learner/SBALearnerITCase.java | 41 ++ .../it/learner/SPALearnerITCase.java | 2 +- .../it/learner/SPMMLearnerITCase.java | 41 ++ .../examples/DefaultLearningExample.java | 46 ++- .../de/learnlib/examples/LearningExample.java | 20 +- .../learnlib/examples/LearningExamples.java | 41 +- .../examples/sba/ExamplePalindrome.java | 106 +++++ .../examples/sba/ExampleRandomSBA.java | 37 ++ .../examples/spa/ExamplePalindrome.java | 14 +- .../examples/spa/ExampleRandomSPA.java | 10 +- .../examples/spmm/ExamplePalindrome.java | 107 +++++ .../examples/spmm/ExampleRandomSPMM.java | 38 ++ 75 files changed, 4674 insertions(+), 374 deletions(-) rename algorithms/active/{spa => procedural}/pom.xml (82%) create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/SymbolWrapper.java rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms/spa/adapter/DiscriminationTreeAdapter.java => procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/DiscriminationTreeAdapterDFA.java} (79%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms/spa/adapter/KearnsVaziraniAdapter.java => procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/KearnsVaziraniAdapterDFA.java} (82%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms/spa/adapter/LStarBaseAdapter.java => procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/LStarBaseAdapterDFA.java} (84%) create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/OptimalTTTAdapterDFA.java rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms/spa/adapter/RivestSchapireAdapter.java => procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/RivestSchapireAdapterDFA.java} (86%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms/spa/adapter/TTTAdapter.java => procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/TTTAdapterDFA.java} (82%) create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/DiscriminationTreeAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/KearnsVaziraniAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/LStarBaseAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/OptimalTTTAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/RivestSchapireAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/TTTAdapterMealy.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ATManager.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/MappingSBA.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ProceduralMembershipOracle.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/SBALearner.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/DefaultATManager.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/OptimizingATManager.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ATRManager.java rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms => procedural/src/main/java/de/learnlib/algorithms/procedural}/spa/ProceduralMembershipOracle.java (86%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms => procedural/src/main/java/de/learnlib/algorithms/procedural}/spa/SPALearner.java (69%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms => procedural/src/main/java/de/learnlib/algorithms/procedural}/spa/manager/DefaultATRManager.java (79%) rename algorithms/active/{spa/src/main/java/de/learnlib/algorithms => procedural/src/main/java/de/learnlib/algorithms/procedural}/spa/manager/OptimizingATRManager.java (88%) create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ATManager.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/MappingSPMM.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ProceduralMembershipOracle.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/SPMMLearner.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/DefaultATManager.java create mode 100644 algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/OptimizingATManager.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/ATManagerTest.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/OptimizationsTest.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/it/SBAIT.java rename algorithms/active/{spa/src/test/java/de/learnlib/algorithms => procedural/src/test/java/de/learnlib/algorithms/procedural}/spa/ATRManagerTest.java (83%) create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/it/SPAIT.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/ATManagerTest.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/OptimizationsTest.java create mode 100644 algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/it/SPMMIT.java delete mode 100644 algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ATRManager.java delete mode 100644 algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/SPAIT.java create mode 100644 oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/SimulatorEQOracle.java create mode 100644 oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracle.java rename oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/{WMethodSPAEQOracle.java => WMethodEQOracle.java} (68%) rename oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/{WpMethodSPAEQOracle.java => WpMethodEQOracle.java} (69%) create mode 100644 oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/SimulatorEQOracle.java create mode 100644 oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracle.java create mode 100644 oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracleTest.java rename oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/{WMethodSPAEQOracleTest.java => WMethodEQOracleTest.java} (75%) rename oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/{WpMethodSPAEQOracleTest.java => WpMethodEQOracleTest.java} (75%) create mode 100644 oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracleTest.java create mode 100644 test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSBALearnerIT.java create mode 100644 test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPMMLearnerIT.java create mode 100644 test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SBALearnerITCase.java create mode 100644 test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPMMLearnerITCase.java create mode 100644 test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExamplePalindrome.java create mode 100644 test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExampleRandomSBA.java create mode 100644 test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExamplePalindrome.java create mode 100644 test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExampleRandomSPMM.java diff --git a/CHANGELOG.md b/CHANGELOG.md index 84fdd1526b..ad242a0d7f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,7 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * Added the OSTIA passive learning algorithm, thanks to [Aleksander Mendoza-Drosik](https://github.com/aleksander-mendoza). * Added the OML (optimal-MAT-learner) active learning algorithm, thanks to [Falk Howar](https://github.com/fhowar). -* Added a new learning algorithm for systems of procedural automata (SPAs). +* Added a new learning algorithm for procedural systems (SPAs, SBAs, SPMMs). * Added Moore versions of the learners `DT`, `TTT`, `LStar`, thanks to [Mohamad Bayram](https://github.com/mohbayram). * Migrated the AAAR algorithm from the old closed-source LearnLib. diff --git a/README.md b/README.md index 5a46953dd3..4ff652e4f7 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ Kearns & Vazirani | `DFA` `Mealy` L* (incl. variants) | `DFA` `Mealy` `Moore` NL* | `NFA` OML | `DFA` `Mealy` -SPA | `SPA` +Procedural | `SPA` `SBA` `SPMM` TTT | `DFA` `Mealy` `Moore` `VPDA` diff --git a/algorithms/active/pom.xml b/algorithms/active/pom.xml index 75cb010d94..c72b59a0e6 100644 --- a/algorithms/active/pom.xml +++ b/algorithms/active/pom.xml @@ -41,7 +41,7 @@ limitations under the License. lstar nlstar oml - spa + procedural ttt ttt-vpda diff --git a/algorithms/active/spa/pom.xml b/algorithms/active/procedural/pom.xml similarity index 82% rename from algorithms/active/spa/pom.xml rename to algorithms/active/procedural/pom.xml index b9163181ca..166c301a52 100644 --- a/algorithms/active/spa/pom.xml +++ b/algorithms/active/procedural/pom.xml @@ -25,11 +25,11 @@ limitations under the License. ../pom.xml - learnlib-spa + learnlib-procedural - LearnLib :: Algorithms :: SPA + LearnLib :: Algorithms :: Procedural - An active learning algorithm for systems of procedural automata. Contains the base learning framework as well as adapters for orchestrating various regular learners of LearnLib to the context-free learning setup. + Active learning algorithms for procedural systems. Currently, contains learners for SPAs, SBAs, and SPMMs including adapters for integrating various regular learners of LearnLib in the context-free learning setup. @@ -48,11 +48,11 @@ limitations under the License. de.learnlib - learnlib-discrimination-tree + learnlib-datastructure-ot de.learnlib - learnlib-datastructure-ot + learnlib-discrimination-tree de.learnlib @@ -62,6 +62,10 @@ limitations under the License. de.learnlib learnlib-lstar + + de.learnlib + learnlib-oml + de.learnlib learnlib-ttt @@ -100,12 +104,27 @@ limitations under the License. buildergen + + org.checkerframework + checker-qual + + + + de.learnlib + learnlib-dhc + test + de.learnlib learnlib-drivers-simulator test + + de.learnlib + learnlib-equivalence-oracles + test + de.learnlib.testsupport learnlib-learner-it-support diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/SymbolWrapper.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/SymbolWrapper.java new file mode 100644 index 0000000000..ed40906016 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/SymbolWrapper.java @@ -0,0 +1,48 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural; + +/** + * A utility class to annotate an input symbol with a (boolean) continuable flag. + * + * @param + * input symbol type + * + * @author frohme + */ +public class SymbolWrapper { + + private final I delegate; + private final boolean continuable; + + public SymbolWrapper(I delegate, boolean continuable) { + this.delegate = delegate; + this.continuable = continuable; + } + + public I getDelegate() { + return delegate; + } + + public boolean isContinuable() { + return continuable; + } + + @Override + public String toString() { + return delegate + " (" + continuable + ')'; + } +} diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/DiscriminationTreeAdapter.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/DiscriminationTreeAdapterDFA.java similarity index 79% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/DiscriminationTreeAdapter.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/DiscriminationTreeAdapterDFA.java index c0917d4d25..3001360352 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/DiscriminationTreeAdapter.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/DiscriminationTreeAdapterDFA.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.adapter; +package de.learnlib.algorithms.procedural.adapter.dfa; import de.learnlib.algorithms.discriminationtree.dfa.DTLearnerDFA; import de.learnlib.api.AccessSequenceTransformer; @@ -23,16 +23,16 @@ import net.automatalib.words.Word; /** - * Adapter for using {@link DTLearnerDFA} as a sub-procedural learner. + * Adapter for using {@link DTLearnerDFA} as a procedural learner. * * @param * input symbol type * * @author frohme */ -public class DiscriminationTreeAdapter extends DTLearnerDFA implements AccessSequenceTransformer { +public class DiscriminationTreeAdapterDFA extends DTLearnerDFA implements AccessSequenceTransformer { - public DiscriminationTreeAdapter(Alphabet alphabet, MembershipOracle oracle) { + public DiscriminationTreeAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { super(alphabet, oracle, LocalSuffixFinders.RIVEST_SCHAPIRE, true, true); } diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/KearnsVaziraniAdapter.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/KearnsVaziraniAdapterDFA.java similarity index 82% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/KearnsVaziraniAdapter.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/KearnsVaziraniAdapterDFA.java index 7a56778bfb..0959a34ab1 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/KearnsVaziraniAdapter.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/KearnsVaziraniAdapterDFA.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.adapter; +package de.learnlib.algorithms.procedural.adapter.dfa; import de.learnlib.acex.analyzers.AcexAnalyzers; import de.learnlib.algorithms.kv.dfa.KearnsVaziraniDFA; @@ -24,16 +24,16 @@ import net.automatalib.words.Word; /** - * Adapter for using {@link KearnsVaziraniDFA} as a sub-procedural learner. + * Adapter for using {@link KearnsVaziraniDFA} as a procedural learner. * * @param * input symbol type * * @author frohme */ -public class KearnsVaziraniAdapter extends KearnsVaziraniDFA implements AccessSequenceTransformer { +public class KearnsVaziraniAdapterDFA extends KearnsVaziraniDFA implements AccessSequenceTransformer { - public KearnsVaziraniAdapter(Alphabet alphabet, MembershipOracle oracle) { + public KearnsVaziraniAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { super(alphabet, oracle, true, AcexAnalyzers.BINARY_SEARCH_FWD); } diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/LStarBaseAdapter.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/LStarBaseAdapterDFA.java similarity index 84% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/LStarBaseAdapter.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/LStarBaseAdapterDFA.java index 6d746788f5..b2ce924c2c 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/LStarBaseAdapter.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/LStarBaseAdapterDFA.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.adapter; +package de.learnlib.algorithms.procedural.adapter.dfa; import java.util.Objects; @@ -27,16 +27,16 @@ import net.automatalib.words.Word; /** - * Adapter for using {@link ClassicLStarDFA} as a sub-procedural learner. + * Adapter for using {@link ClassicLStarDFA} as a procedural learner. * * @param * input symbol type * * @author frohme */ -public class LStarBaseAdapter extends ClassicLStarDFA implements AccessSequenceTransformer, DFALearner { +public class LStarBaseAdapterDFA extends ClassicLStarDFA implements AccessSequenceTransformer, DFALearner { - public LStarBaseAdapter(Alphabet alphabet, MembershipOracle oracle) { + public LStarBaseAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { super(alphabet, oracle); } diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/OptimalTTTAdapterDFA.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/OptimalTTTAdapterDFA.java new file mode 100644 index 0000000000..aa7ec61e5d --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/OptimalTTTAdapterDFA.java @@ -0,0 +1,49 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.dfa; + +import java.util.List; + +import de.learnlib.algorithms.oml.ttt.dfa.OptimalTTTDFA; +import de.learnlib.algorithms.oml.ttt.pt.PTNode; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link OptimalTTTDFA} as a procedural learner. + * + * @param + * input symbol type + * + * @author frohme + */ +public class OptimalTTTAdapterDFA extends OptimalTTTDFA implements AccessSequenceTransformer { + + public OptimalTTTAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { + super(alphabet, oracle); + } + + @Override + public Word transformAccessSequence(Word word) { + final List> shortPrefixes = super.getState(word).getShortPrefixes(); + + assert shortPrefixes.size() == 1; + + return shortPrefixes.get(0).word(); + } +} diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/RivestSchapireAdapter.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/RivestSchapireAdapterDFA.java similarity index 86% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/RivestSchapireAdapter.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/RivestSchapireAdapterDFA.java index 48def54e33..b2c50376b1 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/RivestSchapireAdapter.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/RivestSchapireAdapterDFA.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.adapter; +package de.learnlib.algorithms.procedural.adapter.dfa; import java.util.Objects; @@ -27,17 +27,17 @@ import net.automatalib.words.Word; /** - * Adapter for using {@link RivestSchapireDFA} as a sub-procedural learner. + * Adapter for using {@link RivestSchapireDFA} as a procedural learner. * * @param * input symbol type * * @author frohme */ -public class RivestSchapireAdapter extends RivestSchapireDFA +public class RivestSchapireAdapterDFA extends RivestSchapireDFA implements AccessSequenceTransformer, DFALearner { - public RivestSchapireAdapter(Alphabet alphabet, MembershipOracle oracle) { + public RivestSchapireAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { super(alphabet, oracle); } diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/TTTAdapter.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/TTTAdapterDFA.java similarity index 82% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/TTTAdapter.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/TTTAdapterDFA.java index dca11306b8..d010c2090d 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/adapter/TTTAdapter.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/dfa/TTTAdapterDFA.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.adapter; +package de.learnlib.algorithms.procedural.adapter.dfa; import de.learnlib.acex.analyzers.AcexAnalyzers; import de.learnlib.algorithms.ttt.base.TTTState; @@ -24,16 +24,16 @@ import net.automatalib.words.Word; /** - * Adapter for using {@link TTTLearnerDFA} as a sub-procedural learner. + * Adapter for using {@link TTTLearnerDFA} as a procedural learner. * * @param * input symbol type * * @author frohme */ -public class TTTAdapter extends TTTLearnerDFA implements AccessSequenceTransformer { +public class TTTAdapterDFA extends TTTLearnerDFA implements AccessSequenceTransformer { - public TTTAdapter(Alphabet alphabet, MembershipOracle oracle) { + public TTTAdapterDFA(Alphabet alphabet, MembershipOracle oracle) { super(alphabet, oracle, AcexAnalyzers.BINARY_SEARCH_BWD); } diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/DiscriminationTreeAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/DiscriminationTreeAdapterMealy.java new file mode 100644 index 0000000000..2bcd460c43 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/DiscriminationTreeAdapterMealy.java @@ -0,0 +1,45 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import de.learnlib.algorithms.discriminationtree.mealy.DTLearnerMealy; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.counterexamples.LocalSuffixFinders; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link DTLearnerMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class DiscriminationTreeAdapterMealy extends DTLearnerMealy implements AccessSequenceTransformer { + + public DiscriminationTreeAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, oracle, LocalSuffixFinders.RIVEST_SCHAPIRE, true); + } + + @Override + public Word transformAccessSequence(Word word) { + return super.getHypothesisDS().transformAccessSequence(word); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/KearnsVaziraniAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/KearnsVaziraniAdapterMealy.java new file mode 100644 index 0000000000..b1add988b6 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/KearnsVaziraniAdapterMealy.java @@ -0,0 +1,53 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.algorithms.kv.mealy.KearnsVaziraniMealy; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link KearnsVaziraniMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class KearnsVaziraniAdapterMealy extends KearnsVaziraniMealy + implements AccessSequenceTransformer { + + public KearnsVaziraniAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, oracle, false, AcexAnalyzers.LINEAR_FWD); + } + + @Override + public Word transformAccessSequence(Word word) { + final int reachedState = getStateId(super.getHypothesisModel(), word); + return super.stateInfos.get(reachedState).accessSequence; + } + + private int getStateId(MealyMachine mealyMachine, Word word) { + final S s = mealyMachine.getState(word); + return mealyMachine.stateIDs().getStateId(s); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/LStarBaseAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/LStarBaseAdapterMealy.java new file mode 100644 index 0000000000..427ff5b695 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/LStarBaseAdapterMealy.java @@ -0,0 +1,69 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import java.util.Collections; +import java.util.Objects; + +import de.learnlib.algorithms.lstar.ce.ObservationTableCEXHandlers; +import de.learnlib.algorithms.lstar.closing.ClosingStrategies; +import de.learnlib.algorithms.lstar.mealy.ExtensibleLStarMealy; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.datastructure.observationtable.ObservationTable; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link ExtensibleLStarMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class LStarBaseAdapterMealy extends ExtensibleLStarMealy implements AccessSequenceTransformer { + + public LStarBaseAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, + oracle, + Collections.singletonList(Word.epsilon()), + ObservationTableCEXHandlers.CLASSIC_LSTAR, + ClosingStrategies.CLOSE_FIRST); + } + + @Override + public Word transformAccessSequence(Word word) { + final MealyMachine hypothesis = super.getHypothesisModel(); + final ObservationTable> observationTable = super.getObservationTable(); + + final Object reachedState = hypothesis.getState(word); + + for (Word shortPrefix : observationTable.getShortPrefixes()) { + final Object reachedSPState = hypothesis.getState(shortPrefix); + + if (Objects.equals(reachedState, reachedSPState)) { + return shortPrefix; + } + } + + throw new IllegalStateException("This should not have happened"); + } + +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/OptimalTTTAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/OptimalTTTAdapterMealy.java new file mode 100644 index 0000000000..3a6af56a47 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/OptimalTTTAdapterMealy.java @@ -0,0 +1,51 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import java.util.List; + +import de.learnlib.algorithms.oml.ttt.mealy.OptimalTTTMealy; +import de.learnlib.algorithms.oml.ttt.pt.PTNode; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link OptimalTTTMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class OptimalTTTAdapterMealy extends OptimalTTTMealy implements AccessSequenceTransformer { + + public OptimalTTTAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, oracle); + } + + @Override + public Word transformAccessSequence(Word word) { + final List>> shortPrefixes = super.getState(word).getShortPrefixes(); + + assert shortPrefixes.size() == 1; + + return shortPrefixes.get(0).word(); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/RivestSchapireAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/RivestSchapireAdapterMealy.java new file mode 100644 index 0000000000..a06a0a0f6f --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/RivestSchapireAdapterMealy.java @@ -0,0 +1,63 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import java.util.Objects; + +import de.learnlib.algorithms.rivestschapire.RivestSchapireMealy; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.datastructure.observationtable.ObservationTable; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link RivestSchapireMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class RivestSchapireAdapterMealy extends RivestSchapireMealy + implements AccessSequenceTransformer { + + public RivestSchapireAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, oracle); + } + + @Override + public Word transformAccessSequence(Word word) { + final MealyMachine hypothesis = super.getHypothesisModel(); + final ObservationTable> observationTable = super.getObservationTable(); + + final Object reachedState = hypothesis.getState(word); + + for (Word shortPrefix : observationTable.getShortPrefixes()) { + final Object reachedSPState = hypothesis.getState(shortPrefix); + + if (Objects.equals(reachedState, reachedSPState)) { + return shortPrefix; + } + } + + throw new IllegalStateException("This should not have happened"); + } + +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/TTTAdapterMealy.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/TTTAdapterMealy.java new file mode 100644 index 0000000000..9935d08218 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/adapter/mealy/TTTAdapterMealy.java @@ -0,0 +1,50 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.adapter.mealy; + +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.algorithms.ttt.base.TTTState; +import de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.oracle.MembershipOracle; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; + +/** + * Adapter for using {@link TTTLearnerMealy} as a procedural learner. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class TTTAdapterMealy extends TTTLearnerMealy implements AccessSequenceTransformer { + + public TTTAdapterMealy(Alphabet alphabet, MembershipOracle> oracle) { + super(alphabet, oracle, AcexAnalyzers.BINARY_SEARCH_BWD); + } + + @Override + public Word transformAccessSequence(Word word) { + final TTTState> s = super.getHypothesisDS().getState(word); + // we should only query defined paths + assert s != null; + return s.getAccessSequence(); + } + +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ATManager.java new file mode 100644 index 0000000000..7e9ef24b41 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ATManager.java @@ -0,0 +1,90 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import java.util.Collection; +import java.util.Map; +import java.util.Set; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.api.AccessSequenceTransformer; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.commons.util.Pair; +import net.automatalib.words.Word; + +/** + * A manager of access sequences and terminating sequences of {@link SBA}s during the learning process. + * + * @param + * input symbol type + * + * @author frohme + */ +public interface ATManager { + + /** + * Returns an access sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the access sequence for the given procedure + */ + Word getAccessSequence(I procedure); + + /** + * Returns a terminating sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the terminating sequence for the given procedure + */ + Word getTerminatingSequence(I procedure); + + /** + * Extracts from a positive counterexample (potentially new) access sequences and terminating sequences. + * + * @param counterexample + * the counterexample + * + * @return a {@link Pair} of {@link Set}s of procedures (identified by their respective call symbols) for which new + * access and terminating sequences could be extracted and for which previously none of the sequences were + * available. + */ + Pair, Set> scanPositiveCounterexample(Word counterexample); + + /** + * Scans a set of (hypothesis) procedures in order to potentially extract new access sequences and terminating + * sequences. + * + * @param procedures + * a {@link Map} from call symbols to the respective procedural (hypothesis) models + * @param providers + * a {@link Map} from call symbols to {@link AccessSequenceTransformer}s + * @param inputs + * a {@link Collection} of input symbols which should be used for finding new access sequences, terminating + * sequences, and return sequences + * + * @return a {@link Set} of procedures (identified by their respective call symbols) for which terminating sequences + * could be extracted and for which previously no such sequences were available. + */ + Set scanProcedures(Map>> procedures, + Map>> providers, + Collection> inputs); + +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/MappingSBA.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/MappingSBA.java new file mode 100644 index 0000000000..116551f785 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/MappingSBA.java @@ -0,0 +1,114 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import java.util.Collection; +import java.util.Map; +import java.util.Map.Entry; + +import com.google.common.collect.Maps; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.words.ProceduralInputAlphabet; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * @author frohme + */ +class MappingSBA implements SBA { + + private final ProceduralInputAlphabet alphabet; + private final Map> mapping; + private final SBA> delegate; + + private final Map> procedures; + + MappingSBA(ProceduralInputAlphabet alphabet, Map> mapping, SBA> delegate) { + this.alphabet = alphabet; + this.mapping = mapping; + this.delegate = delegate; + + final Map, DFA>> p = delegate.getProcedures(); + this.procedures = Maps.newHashMapWithExpectedSize(p.size()); + + for (Entry, DFA>> e : p.entrySet()) { + procedures.put(e.getKey().getDelegate(), new DFAView<>(e.getValue())); + } + } + + @Override + public @Nullable S getTransition(S state, I i) { + final SymbolWrapper w = this.mapping.get(i); + return w == null ? null : this.delegate.getTransition(state, w); + } + + @Override + public boolean isAccepting(S state) { + return this.delegate.isAccepting(state); + } + + @Override + public S getInitialState() { + return this.delegate.getInitialState(); + } + + @Override + public @Nullable I getInitialProcedure() { + final SymbolWrapper init = this.delegate.getInitialProcedure(); + return init == null ? null : init.getDelegate(); + } + + @Override + public ProceduralInputAlphabet getInputAlphabet() { + return this.alphabet; + } + + @Override + public Map> getProcedures() { + return this.procedures; + } + + private class DFAView implements DFA { + + private final DFA> delegate; + + DFAView(DFA> delegate) { + this.delegate = delegate; + } + + @Override + public Collection getStates() { + return delegate.getStates(); + } + + @Override + public @Nullable S2 getTransition(S2 s, I i) { + final SymbolWrapper w = mapping.get(i); + return w == null ? null : delegate.getTransition(s, w); + } + + @Override + public boolean isAccepting(S2 s) { + return delegate.isAccepting(s); + } + + @Override + public @Nullable S2 getInitialState() { + return delegate.getInitialState(); + } + } +} \ No newline at end of file diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ProceduralMembershipOracle.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ProceduralMembershipOracle.java new file mode 100644 index 0000000000..378289f39c --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/ProceduralMembershipOracle.java @@ -0,0 +1,127 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Iterator; +import java.util.List; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.api.query.Query; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; + +/** + * @author frohme + */ +class ProceduralMembershipOracle implements MembershipOracle, Boolean> { + + private final ProceduralInputAlphabet alphabet; + private final MembershipOracle delegate; + private final I procedure; + private final ATManager atManager; + + ProceduralMembershipOracle(ProceduralInputAlphabet alphabet, + MembershipOracle delegate, + I procedure, + ATManager atManager) { + this.alphabet = alphabet; + this.delegate = delegate; + this.procedure = procedure; + this.atManager = atManager; + } + + @Override + public void processQueries(Collection, Boolean>> collection) { + final List> transformedQueries = new ArrayList<>(collection.size()); + + for (Query, Boolean> q : collection) { + if (isWellDefined(q)) { + transformedQueries.add(new TransformedQuery(q)); + } else { + q.answer(false); + } + } + + this.delegate.processQueries(transformedQueries); + } + + private boolean isWellDefined(Query, Boolean> q) { + final Iterator> iter = q.getInput().iterator(); + + while (iter.hasNext()) { + final SymbolWrapper wrapper = iter.next(); + if (!wrapper.isContinuable()) { + return !iter.hasNext(); + } + } + + return true; + } + + private Word transformLocalQuery(Word> query) { + final WordBuilder builder = new WordBuilder<>(); + builder.append(atManager.getAccessSequence(this.procedure)); + + final Iterator> iter = query.iterator(); + while (iter.hasNext()) { + final SymbolWrapper w = iter.next(); + final I i = w.getDelegate(); + builder.append(i); + if (alphabet.isCallSymbol(i) && iter.hasNext()) { + assert w.isContinuable(); + builder.append(atManager.getTerminatingSequence(i)); + builder.append(alphabet.getReturnSymbol()); + } + } + + return builder.toWord(); + } + + private class TransformedQuery extends Query { + + private final Query, Boolean> originalQuery; + private final Word transformedQuery; + + TransformedQuery(Query, Boolean> originalQuery) { + this.originalQuery = originalQuery; + this.transformedQuery = transformLocalQuery(originalQuery.getInput()); + } + + @Override + public void answer(Boolean output) { + originalQuery.answer(output); + } + + @Override + public Word getPrefix() { + return Word.epsilon(); + } + + @Override + public Word getSuffix() { + return this.transformedQuery; + } + + @Override + public Word getInput() { + return this.transformedQuery; + } + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/SBALearner.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/SBALearner.java new file mode 100644 index 0000000000..93fcb3f96f --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/SBALearner.java @@ -0,0 +1,362 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; + +import com.google.common.collect.Maps; +import de.learnlib.acex.AcexAnalyzer; +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.acex.impl.AbstractBaseCounterexample; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.sba.manager.OptimizingATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.api.algorithm.LearningAlgorithm; +import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.api.query.DefaultQuery; +import de.learnlib.util.MQUtil; +import net.automatalib.SupportsGrowingAlphabet; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.automata.procedural.EmptySBA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.StackSBA; +import net.automatalib.commons.util.Pair; +import net.automatalib.commons.util.mappings.Mapping; +import net.automatalib.util.automata.Automata; +import net.automatalib.util.automata.procedural.SBAUtil; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import net.automatalib.words.impl.GrowingMapAlphabet; + +/** + * A learning algorithm for {@link SBA}s. + * + * @param + * input symbol type + * @param + * sub-learner type + * + * @author frohme + */ +public class SBALearner> & SupportsGrowingAlphabet> & AccessSequenceTransformer>> + implements LearningAlgorithm, I, Boolean> { + + private final ProceduralInputAlphabet alphabet; + private final MembershipOracle oracle; + private final Mapping, Boolean>> learnerConstructors; + private final AcexAnalyzer analyzer; + private final ATManager atManager; + + private final Map learners; + private I initialCallSymbol; + + private final Map> mapping; + + public SBALearner(ProceduralInputAlphabet alphabet, + MembershipOracle oracle, + LearnerConstructor, Boolean> learnerConstructor) { + this(alphabet, + oracle, + (i) -> learnerConstructor, + AcexAnalyzers.BINARY_SEARCH_BWD, + new OptimizingATManager<>(alphabet)); + } + + public SBALearner(ProceduralInputAlphabet alphabet, + MembershipOracle oracle, + Mapping, Boolean>> learnerConstructors, + AcexAnalyzer analyzer, + ATManager atManager) { + this.alphabet = alphabet; + this.oracle = oracle; + this.learnerConstructors = learnerConstructors; + this.analyzer = analyzer; + this.atManager = atManager; + + this.learners = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls()); + this.mapping = Maps.newHashMapWithExpectedSize(this.alphabet.size()); + + for (I i : this.alphabet.getInternalAlphabet()) { + final SymbolWrapper wrapper = new SymbolWrapper<>(i, true); + this.mapping.put(i, wrapper); + } + + final SymbolWrapper wrapper = new SymbolWrapper<>(this.alphabet.getReturnSymbol(), false); + this.mapping.put(this.alphabet.getReturnSymbol(), wrapper); + } + + @Override + public void startLearning() { + // do nothing, as we have to wait for evidence that the potential main procedure actually terminates + } + + @Override + public boolean refineHypothesis(DefaultQuery defaultQuery) { + + assert this.alphabet.isReturnMatched(defaultQuery.getInput()); + + boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery); + + while (refineHypothesisInternal(defaultQuery)) { + changed = true; + } + + ensureCallAndReturnClosure(); + + assert SBAUtil.isValid(this.getHypothesisModel()); + + return changed; + } + + private boolean refineHypothesisInternal(DefaultQuery defaultQuery) { + + final SBA hypothesis = this.getHypothesisModel(); + + if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) { + return false; + } + + final Word input = defaultQuery.getInput(); + final int mismatchIdx = analyzer.analyzeAbstractCounterexample(new Acex<>(input, + defaultQuery.getOutput() ? + hypothesis::accepts : + this.oracle::answerQuery)); + + // extract local ce + final int callIdx = this.alphabet.findCallIndex(input, mismatchIdx); + final I procedure = input.getSymbol(callIdx); + + final Word localTrace = + this.alphabet.project(input.subWord(callIdx + 1, mismatchIdx), 0).append(input.getSymbol(mismatchIdx)); + final DefaultQuery, Boolean> localCE = constructLocalCE(localTrace, defaultQuery.getOutput()); + + boolean localRefinement = this.learners.get(procedure).refineHypothesis(localCE); + assert localRefinement; + + return true; + } + + @Override + public SBA getHypothesisModel() { + + if (this.learners.isEmpty()) { + return new EmptySBA<>(this.alphabet); + } + + final Alphabet> internalAlphabet = new GrowingMapAlphabet<>(); + final Alphabet> callAlphabet = new GrowingMapAlphabet<>(); + final SymbolWrapper returnSymbol; + + final Map>> procedures = getSubModels(); + final Map, DFA>> mappedProcedures = + Maps.newHashMapWithExpectedSize(procedures.size()); + + for (Entry>> e : procedures.entrySet()) { + final SymbolWrapper w = this.mapping.get(e.getKey()); + assert w != null; + mappedProcedures.put(w, e.getValue()); + callAlphabet.add(w); + } + + for (I i : this.alphabet.getInternalAlphabet()) { + final SymbolWrapper w = this.mapping.get(i); + assert w != null; + internalAlphabet.add(w); + } + + returnSymbol = this.mapping.get(alphabet.getReturnSymbol()); + assert returnSymbol != null; + + final ProceduralInputAlphabet> mappedAlphabet = + new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); + + final StackSBA> delegate = + new StackSBA<>(mappedAlphabet, this.mapping.get(initialCallSymbol), mappedProcedures); + + return new MappingSBA<>(alphabet, mapping, delegate); + } + + private boolean extractUsefulInformationFromCounterExample(DefaultQuery defaultQuery) { + + if (!defaultQuery.getOutput()) { + return false; + } + + boolean update = false; + final Word input = defaultQuery.getInput(); + + // positive CEs should always be rooted at the main procedure + this.initialCallSymbol = input.firstSymbol(); + + final Pair, Set> newSeqs = atManager.scanPositiveCounterexample(input); + final Set newCalls = newSeqs.getFirst(); + final Set newTerms = newSeqs.getSecond(); + + for (I call : newTerms) { + final SymbolWrapper sym = new SymbolWrapper<>(call, true); + this.mapping.put(call, sym); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(sym); + update = true; + } + } + + for (I sym : newCalls) { + update = true; + final L newLearner = learnerConstructors.get(sym) + .constructLearner(new GrowingMapAlphabet<>(this.mapping.values()), + new ProceduralMembershipOracle<>(alphabet, + oracle, + sym, + atManager)); + + newLearner.startLearning(); + + // add new learner here, so that we have an AccessSequenceTransformer available when scanning for shorter ts + this.learners.put(sym, newLearner); + + // try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses + final Set newTS = + this.atManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()), + learners, + mapping.values()); + + for (I call : newTS) { + final SymbolWrapper wrapper = new SymbolWrapper<>(call, true); + this.mapping.put(call, wrapper); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(wrapper); + } + } + + // add non-terminating version for new call + if (!this.mapping.containsKey(sym)) { + final SymbolWrapper wrapper = new SymbolWrapper<>(sym, false); + this.mapping.put(sym, wrapper); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(wrapper); + } + } + } + + return update; + } + + private Map>> getSubModels() { + final Map>> subModels = Maps.newHashMapWithExpectedSize(this.learners.size()); + + for (Map.Entry entry : this.learners.entrySet()) { + subModels.put(entry.getKey(), entry.getValue().getHypothesisModel()); + } + + return subModels; + } + + private DefaultQuery, Boolean> constructLocalCE(Word input, boolean output) { + + final WordBuilder> wb = new WordBuilder<>(input.length()); + for (I i : input) { + wb.append(mapping.get(i)); + } + + return new DefaultQuery<>(wb.toWord(), output); + } + + private void ensureCallAndReturnClosure() { + + final Set> nonContinuableSymbols = new HashSet<>(); + for (SymbolWrapper mapped : mapping.values()) { + if (!mapped.isContinuable()) { + nonContinuableSymbols.add(mapped); + } + } + + for (L learner : this.learners.values()) { + boolean stable = false; + + while (!stable) { + stable = ensureCallAndReturnClosure(learner.getHypothesisModel(), nonContinuableSymbols, learner); + } + } + } + + private boolean ensureCallAndReturnClosure(DFA> hyp, + Collection> nonContinuableSymbols, + L learner) { + + final Set>> cover = new HashSet<>(); + for (Word> sc : Automata.stateCover(hyp, mapping.values())) { + cover.add(learner.transformAccessSequence(sc)); + } + + for (Word> cov : cover) { + final S state = hyp.getState(cov); + + for (SymbolWrapper i : nonContinuableSymbols) { + final S succ = hyp.getSuccessor(state, i); + + for (SymbolWrapper next : mapping.values()) { + + if (hyp.isAccepting(hyp.getSuccessor(succ, next))) { // closure is violated + + final DefaultQuery, Boolean> ce = + new DefaultQuery<>(cov.append(i).append(next), false); + final boolean refined = learner.refineHypothesis(ce); + + assert refined; + return false; + } + } + } + } + + return true; + } + + private static class Acex extends AbstractBaseCounterexample { + + private final Word input; + private final Predicate> oracle; + + Acex(Word input, Predicate> oracle) { + super(input.size() + 1); + this.input = input; + this.oracle = oracle; + } + + @Override + protected Boolean computeEffect(int index) { + return oracle.test(input.prefix(index)); + } + + @Override + public boolean checkEffects(Boolean eff1, Boolean eff2) { + return Objects.equals(eff1, eff2); + } + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/DefaultATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/DefaultATManager.java new file mode 100644 index 0000000000..5ab84eac3e --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/DefaultATManager.java @@ -0,0 +1,101 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba.manager; + +import java.util.Collection; +import java.util.Collections; +import java.util.Map; +import java.util.Set; + +import com.google.common.collect.Maps; +import com.google.common.collect.Sets; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.sba.ATManager; +import de.learnlib.api.AccessSequenceTransformer; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.commons.util.Pair; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; + +/** + * A default {@link ATManager} that only extracts initial access sequences and terminating sequences from positive + * counterexamples. + * + * @param + * input symbol type + * + * @author frohme + */ +public class DefaultATManager implements ATManager { + + private final Map> accessSequences; + private final Map> terminatingSequences; + + private final ProceduralInputAlphabet alphabet; + + public DefaultATManager(ProceduralInputAlphabet alphabet) { + this.alphabet = alphabet; + + this.accessSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); + this.terminatingSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); + } + + @Override + public Word getAccessSequence(I procedure) { + assert this.accessSequences.containsKey(procedure); + return this.accessSequences.get(procedure); + } + + @Override + public Word getTerminatingSequence(I procedure) { + assert this.terminatingSequences.containsKey(procedure); + return this.terminatingSequences.get(procedure); + } + + @Override + public Pair, Set> scanPositiveCounterexample(Word input) { + final Set newCalls = Sets.newHashSetWithExpectedSize(alphabet.getNumCalls() - accessSequences.size()); + final Set newTerms = Sets.newHashSetWithExpectedSize(alphabet.getNumCalls() - terminatingSequences.size()); + + for (int i = 0; i < input.size(); i++) { + final I sym = input.getSymbol(i); + + if (this.alphabet.isCallSymbol(sym)) { + + if (!this.accessSequences.containsKey(sym)) { + this.accessSequences.put(sym, input.prefix(i + 1)); + newCalls.add(sym); + } + + final int returnIdx = this.alphabet.findReturnIndex(input, i + 1); + + if (returnIdx > 0 && !this.terminatingSequences.containsKey(sym)) { + this.terminatingSequences.put(sym, input.subWord(i + 1, returnIdx)); + newTerms.add(sym); + } + } + } + + return Pair.of(newCalls, newTerms); + } + + @Override + public Set scanProcedures(Map>> procedures, + Map>> providers, + Collection> inputs) { + return Collections.emptySet(); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/OptimizingATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/OptimizingATManager.java new file mode 100644 index 0000000000..9531ec495c --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/sba/manager/OptimizingATManager.java @@ -0,0 +1,255 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba.manager; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; + +import com.google.common.collect.Maps; +import com.google.common.collect.Sets; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.sba.ATManager; +import de.learnlib.api.AccessSequenceTransformer; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.commons.util.Pair; +import net.automatalib.util.automata.cover.Covers; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * An optimizing {@link ATManager} that continuously scans positive counterexamples and procedural models in order to + * find shorter access sequences and terminating sequences. + * + * @param + * input symbol type + * + * @author frohme + */ + +public class OptimizingATManager implements ATManager { + + private final Map> accessSequences; + private final Map> terminatingSequences; + + private final ProceduralInputAlphabet alphabet; + + public OptimizingATManager(ProceduralInputAlphabet alphabet) { + this.alphabet = alphabet; + + this.accessSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); + this.terminatingSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); + } + + @Override + public Word getAccessSequence(I procedure) { + assert this.accessSequences.containsKey(procedure); + return this.accessSequences.get(procedure); + } + + @Override + public Word getTerminatingSequence(I procedure) { + assert this.terminatingSequences.containsKey(procedure); + return this.terminatingSequences.get(procedure); + } + + @Override + public Pair, Set> scanPositiveCounterexample(Word counterexample) { + final Set newCalls = + Sets.newHashSetWithExpectedSize(this.alphabet.getNumCalls() - this.accessSequences.size()); + final Set newTerms = + Sets.newHashSetWithExpectedSize(this.alphabet.getNumCalls() - this.terminatingSequences.size()); + + this.extractPotentialTerminatingSequences(counterexample, newTerms); + this.extractPotentialAccessSequences(counterexample, newCalls); + + return Pair.of(newCalls, newTerms); + } + + @Override + public Set scanProcedures(Map>> procedures, + Map>> providers, + Collection> inputs) { + + final Set newTS = Sets.newHashSetWithExpectedSize(procedures.size()); + if (!procedures.isEmpty()) { + + final SymbolWrapper returnSymbol = inputs.stream() + .filter(i -> Objects.equals(i.getDelegate(), + alphabet.getReturnSymbol())) + .findAny() + .orElseThrow(IllegalArgumentException::new); + boolean foundImprovements = false; + boolean stable = false; + + while (!stable) { + stable = true; + for (Map.Entry>> entry : procedures.entrySet()) { + final I i = entry.getKey(); + final DFA> automaton = entry.getValue(); + final Word currentTS = terminatingSequences.get(i); + assert providers.containsKey(i); + final Word hypTS = getShortestHypothesisTS(automaton, providers.get(i), inputs, returnSymbol); + + if (hypTS != null && (currentTS == null || hypTS.size() < currentTS.size())) { + + if (currentTS == null) { + newTS.add(i); + } + + terminatingSequences.put(i, hypTS); + stable = false; + foundImprovements = true; + } + } + } + + if (foundImprovements) { + optimizeSequences(this.accessSequences); + optimizeSequences(this.terminatingSequences); + } + } + + return newTS; + } + + private @Nullable Word getShortestHypothesisTS(DFA> hyp, + AccessSequenceTransformer> asTransformer, + Collection> inputs, + SymbolWrapper returnSymbol) { + final Iterator>> iter = Covers.stateCoverIterator(hyp, inputs); + Word result = null; + + while (iter.hasNext()) { + final Word> cover = iter.next(); + final Word> as = asTransformer.transformAccessSequence(cover); + if (hyp.accepts(as.append(returnSymbol))) { + final Word ts = + this.alphabet.expand(as.transform(SymbolWrapper::getDelegate), terminatingSequences::get); + if (result == null || result.size() > ts.size()) { + result = ts; + } + + } + } + + return result; + } + + private void optimizeSequences(Map> sequences) { + for (Map.Entry> entry : sequences.entrySet()) { + final Word currentSequence = entry.getValue(); + final Word minimized = minifyWellMatched(currentSequence); + + if (minimized.size() < currentSequence.size()) { + sequences.put(entry.getKey(), minimized); + } + } + } + + private void extractPotentialTerminatingSequences(Word input, Set newProcedures) { + for (int i = 0; i < input.size(); i++) { + final I sym = input.getSymbol(i); + + if (this.alphabet.isCallSymbol(sym)) { + + final int returnIdx = this.alphabet.findReturnIndex(input, i + 1); + + if (returnIdx > 0) { + final Word potentialTermSeq = input.subWord(i + 1, returnIdx); + final Word currentTermSeq = this.terminatingSequences.get(sym); + + if (currentTermSeq == null) { + newProcedures.add(sym); + this.terminatingSequences.put(sym, potentialTermSeq); + } else if (potentialTermSeq.size() < currentTermSeq.size()) { + this.terminatingSequences.put(sym, potentialTermSeq); + } + } + } + } + } + + private void extractPotentialAccessSequences(Word input, Set newCalls) { + + final List asBuilder = new ArrayList<>(input.size()); + + for (int i = 0; i < input.size(); i++) { + + final I sym = input.getSymbol(i); + + asBuilder.add(sym); + + if (this.alphabet.isCallSymbol(sym)) { + + final Word currentAccSeq = this.accessSequences.get(sym); + + if (currentAccSeq == null) { + newCalls.add(sym); + this.accessSequences.put(sym, Word.fromList(asBuilder)); + } else if (asBuilder.size() < currentAccSeq.size()) { + this.accessSequences.put(sym, Word.fromList(asBuilder)); + } + } else if (this.alphabet.isReturnSymbol(sym)) { + // update asBuilder + final int callIdx = alphabet.findCallIndex(asBuilder, asBuilder.size() - 1); + final I procedure = asBuilder.get(callIdx); + final Word ts = terminatingSequences.get(procedure); + + assert ts != null; + + asBuilder.subList(callIdx + 1, asBuilder.size()).clear(); + asBuilder.addAll(ts.asList()); + asBuilder.add(alphabet.getReturnSymbol()); + } + } + } + + @SuppressWarnings("PMD.AvoidReassigningLoopVariables") // we want to skip ahead here + private Word minifyWellMatched(Word input) { + + if (input.isEmpty()) { + return Word.epsilon(); + } + + final WordBuilder wb = new WordBuilder<>(input.size()); + + for (int i = 0; i < input.size(); i++) { + + final I sym = input.getSymbol(i); + + wb.append(sym); + + if (this.alphabet.isCallSymbol(sym)) { + final int returnIdx = this.alphabet.findReturnIndex(input, i + 1); + + if (returnIdx > -1) { + wb.append(terminatingSequences.get(sym)); + wb.append(alphabet.getReturnSymbol()); + i = returnIdx; // next loop iteration starts _after_ the return symbol + } + } + } + + return wb.toWord(); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ATRManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ATRManager.java new file mode 100644 index 0000000000..adb7a527a5 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ATRManager.java @@ -0,0 +1,99 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spa; + +import java.util.Collection; +import java.util.Map; +import java.util.Set; + +import de.learnlib.api.AccessSequenceTransformer; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.words.Word; + +/** + * A manager of access sequences, terminating sequences, and return sequences of {@link SPA}s during the learning + * process. + * + * @param + * input symbol type + * + * @author frohme + */ +public interface ATRManager { + + /** + * Returns an access sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the access sequence for the given procedure + */ + Word getAccessSequence(I procedure); + + /** + * Returns a terminating sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the terminating sequence for the given procedure + */ + Word getTerminatingSequence(I procedure); + + /** + * Returns a return sequence for the given procedure. Note that the sequence must match the + * {@link #getAccessSequence(Object) access sequence} in order to provide an admissible context for query + * expansion. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the return sequence for the given procedure + */ + Word getReturnSequence(I procedure); + + /** + * Extracts from a positive counterexample (potentially new) access sequences, terminating sequences, and return + * sequences. + * + * @param counterexample + * the counterexample + * + * @return a {@link Set} of procedures (identified by their respective call symbols) for which new access, + * terminating, and return sequences could be extracted and for which previously none of the sequences were + * available. + */ + Set scanPositiveCounterexample(Word counterexample); + + /** + * Scans a set of (hypothesis) procedures in order to potentially extract new access sequences, terminating + * sequences, and return sequences. + * + * @param procedures + * a {@link Map} from call symbols to the respective procedural (hypothesis) models + * @param providers + * a {@link Map} from call symbols to {@link AccessSequenceTransformer}s + * @param inputs + * a {@link Collection} of input symbols which should be used for finding new access sequences, terminating + * sequences, and return sequences + */ + void scanProcedures(Map> procedures, + Map> providers, + Collection inputs); + +} diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ProceduralMembershipOracle.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ProceduralMembershipOracle.java similarity index 86% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ProceduralMembershipOracle.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ProceduralMembershipOracle.java index f83bf46dbb..69b61bc593 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ProceduralMembershipOracle.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/ProceduralMembershipOracle.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa; +package de.learnlib.algorithms.procedural.spa; import java.util.ArrayList; import java.util.Collection; @@ -21,21 +21,24 @@ import de.learnlib.api.oracle.MembershipOracle; import de.learnlib.api.query.Query; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.WordBuilder; -final class ProceduralMembershipOracle implements MembershipOracle { +/** + * @author frohme + */ +class ProceduralMembershipOracle implements MembershipOracle { - private final SPAAlphabet alphabet; + private final ProceduralInputAlphabet alphabet; private final MembershipOracle delegate; private final I procedure; private final ATRManager atrManager; - ProceduralMembershipOracle(SPAAlphabet alphabet, - MembershipOracle delegate, - I procedure, - ATRManager atrManager) { + ProceduralMembershipOracle(ProceduralInputAlphabet alphabet, + MembershipOracle delegate, + I procedure, + ATRManager atrManager) { this.alphabet = alphabet; this.delegate = delegate; this.procedure = procedure; diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/SPALearner.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/SPALearner.java similarity index 69% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/SPALearner.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/SPALearner.java index 6f65b546e2..2724d3e19c 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/SPALearner.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/SPALearner.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa; +package de.learnlib.algorithms.procedural.spa; import java.util.ArrayDeque; import java.util.ArrayList; @@ -21,12 +21,16 @@ import java.util.Deque; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Set; import java.util.function.Predicate; import com.google.common.collect.Maps; import com.google.common.collect.Sets; -import de.learnlib.algorithms.spa.manager.OptimizingATRManager; +import de.learnlib.acex.AcexAnalyzer; +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.acex.impl.AbstractBaseCounterexample; +import de.learnlib.algorithms.procedural.spa.manager.OptimizingATRManager; import de.learnlib.api.AccessSequenceTransformer; import de.learnlib.api.algorithm.LearnerConstructor; import de.learnlib.api.algorithm.LearningAlgorithm; @@ -36,18 +40,18 @@ import de.learnlib.util.MQUtil; import net.automatalib.SupportsGrowingAlphabet; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.EmptySPA; -import net.automatalib.automata.spa.SPA; -import net.automatalib.automata.spa.StackSPA; +import net.automatalib.automata.procedural.EmptySPA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.StackSPA; import net.automatalib.commons.util.mappings.Mapping; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.WordBuilder; import net.automatalib.words.impl.GrowingMapAlphabet; import org.checkerframework.checker.nullness.qual.NonNull; /** - * The learning algorithm for {@link StackSPA}s. + * A learning algorithm for {@link SPA}s. * * @param * input symbol type @@ -59,34 +63,35 @@ public class SPALearner & SupportsGrowingAlphabet & AccessSequenceTransformer> implements LearningAlgorithm, I, Boolean> { - private final SPAAlphabet alphabet; + private final ProceduralInputAlphabet alphabet; private final MembershipOracle oracle; private final Mapping> learnerConstructors; + private final AcexAnalyzer analyzer; private final ATRManager atrManager; private final Map subLearners; private final Set activeAlphabet; private I initialCallSymbol; - public SPALearner(SPAAlphabet alphabet, + public SPALearner(ProceduralInputAlphabet alphabet, MembershipOracle oracle, LearnerConstructor learnerConstructor) { - this(alphabet, oracle, (i) -> learnerConstructor); + this(alphabet, + oracle, + (i) -> learnerConstructor, + AcexAnalyzers.BINARY_SEARCH_FWD, + new OptimizingATRManager<>(alphabet)); } - public SPALearner(SPAAlphabet alphabet, - MembershipOracle oracle, - Mapping> learnerConstructors) { - this(alphabet, oracle, learnerConstructors, new OptimizingATRManager<>(alphabet)); - } - - public SPALearner(SPAAlphabet alphabet, + public SPALearner(ProceduralInputAlphabet alphabet, MembershipOracle oracle, Mapping> learnerConstructors, + AcexAnalyzer analyzer, ATRManager atrManager) { this.alphabet = alphabet; this.oracle = oracle; this.learnerConstructors = learnerConstructors; + this.analyzer = analyzer; this.atrManager = atrManager; this.subLearners = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls()); @@ -102,6 +107,8 @@ public void startLearning() { @Override public boolean refineHypothesis(DefaultQuery defaultQuery) { + assert this.alphabet.isWellMatched(defaultQuery.getInput()); + boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery); while (refineHypothesisInternal(defaultQuery)) { @@ -119,24 +126,27 @@ private boolean refineHypothesisInternal(DefaultQuery defaultQuery) return false; } - final Word input = defaultQuery.getInput(); - // look for better sequences and ensure TS conformance prior to CE analysis boolean localRefinement = updateATRAndCheckTSConformance(hypothesis); - final int returnIdx; - - if (defaultQuery.getOutput()) { - returnIdx = detectRejectingProcedure(getHypothesisModel()::accepts, input); - } else { - returnIdx = detectRejectingProcedure(this.oracle::answerQuery, input); + if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) { + return localRefinement; } + final Word input = defaultQuery.getInput(); + final List returnIndices = determineReturnIndices(input); + final int idx = analyzer.analyzeAbstractCounterexample(new Acex(input, + defaultQuery.getOutput() ? + hypothesis::accepts : + this.oracle::answerQuery, + returnIndices)); + final int returnIdx = returnIndices.get(idx); + // extract local ce final int callIdx = this.alphabet.findCallIndex(input, returnIdx); final I procedure = input.getSymbol(callIdx); - final Word localTrace = this.alphabet.normalize(input.subWord(callIdx + 1, returnIdx), 0); + final Word localTrace = this.alphabet.project(input.subWord(callIdx + 1, returnIdx), 0); final DefaultQuery localCE = new DefaultQuery<>(localTrace, defaultQuery.getOutput()); localRefinement |= this.subLearners.get(procedure).refineHypothesis(localCE); @@ -186,9 +196,9 @@ private boolean extractUsefulInformationFromCounterExample(DefaultQuery hypothesis) { while (checkAndEnsureTSConformance(subModels)) { refinement = true; subModels = getSubModels(); - this.atrManager.scanRefinedProcedures(subModels, subLearners, activeAlphabet); + this.atrManager.scanProcedures(subModels, subLearners, activeAlphabet); } return refinement; } - private int detectRejectingProcedure(Predicate> rejectingSystem, Word input) { + private List determineReturnIndices(Word input) { final List returnIndices = new ArrayList<>(); @@ -238,64 +248,7 @@ private int detectRejectingProcedure(Predicate> rejectingSystem, Word } } - // skip last index, because we know its accepting - int returnIdxPos = findLowestAcceptingReturnIndex(rejectingSystem, - input, - returnIndices.subList(0, returnIndices.size() - 1)); - - // if everything is rejecting the error happens at the main procedure - if (returnIdxPos == -1) { - returnIdxPos = returnIndices.size() - 1; - } - - return returnIndices.get(returnIdxPos); - } - - private int findLowestAcceptingReturnIndex(Predicate> system, - Word input, - List returnIndices) { - - int lower = 0; - int upper = returnIndices.size() - 1; - int result = -1; - - while (upper - lower > -1) { - final int mid = lower + ((upper - lower) / 2); - final int returnIdx = returnIndices.get(mid); - - final boolean answer = acceptsDecomposition(system, input, returnIdx + 1); - - if (answer) { - result = mid; - upper = mid - 1; - } else { - lower = mid + 1; - } - } - - return result; - } - - private boolean acceptsDecomposition(Predicate> system, Word input, int idxAfterReturn) { - final Deque> wordStack = new ArrayDeque<>(); - int idx = idxAfterReturn; - - while (idx > 0) { - final int callIdx = this.alphabet.findCallIndex(input, idx); - final I callSymbol = input.getSymbol(callIdx); - final Word normalized = this.alphabet.normalize(input.subWord(callIdx + 1, idx), 0); - final Word expanded = this.alphabet.expand(normalized, this.atrManager::getTerminatingSequence); - - wordStack.push(expanded.prepend(callSymbol)); - - idx = callIdx; - } - - final WordBuilder builder = new WordBuilder<>(); - wordStack.forEach(builder::append); - builder.append(input.subWord(idxAfterReturn)); - - return system.test(builder.toWord()); + return returnIndices; } private boolean checkAndEnsureTSConformance(Map> subModels) { @@ -321,7 +274,7 @@ private boolean checkSingleTerminatingSequence(Word input, Map> if (this.alphabet.isCallSymbol(sym)) { final int returnIdx = this.alphabet.findReturnIndex(input, i + 1); - final Word projectedRun = this.alphabet.normalize(input.subWord(i + 1, returnIdx), 0); + final Word projectedRun = this.alphabet.project(input.subWord(i + 1, returnIdx), 0); // whenever we extract a terminating sequence, we can also instantiate a learner. // Therefore the existence of the hypothesis is guaranteed. @SuppressWarnings("assignment.type.incompatible") @@ -337,4 +290,48 @@ private boolean checkSingleTerminatingSequence(Word input, Map> return refinement; } + private class Acex extends AbstractBaseCounterexample { + + private final Word input; + private final Predicate> oracle; + private final List returnIndices; + + Acex(Word input, Predicate> oracle, List returnIndices) { + super(returnIndices.size() + 1); + this.input = input; + this.oracle = oracle; + this.returnIndices = returnIndices; + + setEffect(returnIndices.size(), true); + setEffect(0, false); + } + + @Override + protected Boolean computeEffect(int index) { + final Deque> wordStack = new ArrayDeque<>(); + int idx = this.returnIndices.get(index); + + while (idx > 0) { + final int callIdx = alphabet.findCallIndex(input, idx); + final I callSymbol = input.getSymbol(callIdx); + final Word normalized = alphabet.project(input.subWord(callIdx + 1, idx), 0); + final Word expanded = alphabet.expand(normalized, atrManager::getTerminatingSequence); + + wordStack.push(expanded.prepend(callSymbol)); + + idx = callIdx; + } + + final WordBuilder builder = new WordBuilder<>(); + wordStack.forEach(builder::append); + builder.append(input.subWord(this.returnIndices.get(index))); + + return oracle.test(builder.toWord()); + } + + @Override + public boolean checkEffects(Boolean eff1, Boolean eff2) { + return Objects.equals(eff1, eff2); + } + } } diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/DefaultATRManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/DefaultATRManager.java similarity index 79% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/DefaultATRManager.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/DefaultATRManager.java index 31a8b010fd..2f865d5e5f 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/DefaultATRManager.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/DefaultATRManager.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.manager; +package de.learnlib.algorithms.procedural.spa.manager; import java.util.Collection; import java.util.Map; @@ -21,21 +21,30 @@ import com.google.common.collect.Maps; import com.google.common.collect.Sets; -import de.learnlib.algorithms.spa.ATRManager; +import de.learnlib.algorithms.procedural.spa.ATRManager; import de.learnlib.api.AccessSequenceTransformer; import net.automatalib.automata.fsa.DFA; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; +/** + * A default {@link ATRManager} that only extracts initial access sequences, terminating sequences, and return sequences + * from positive counterexamples. + * + * @param + * input symbol type + * + * @author frohme + */ public class DefaultATRManager implements ATRManager { private final Map> accessSequences; private final Map> returnSequences; private final Map> terminatingSequences; - private final SPAAlphabet alphabet; + private final ProceduralInputAlphabet alphabet; - public DefaultATRManager(SPAAlphabet alphabet) { + public DefaultATRManager(ProceduralInputAlphabet alphabet) { this.alphabet = alphabet; this.accessSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); @@ -84,9 +93,9 @@ public Set scanPositiveCounterexample(Word input) { } @Override - public void scanRefinedProcedures(Map> procedures, - Map> providers, - Collection inputs) { + public void scanProcedures(Map> procedures, + Map> providers, + Collection inputs) { // do nothing } } diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/OptimizingATRManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/OptimizingATRManager.java similarity index 88% rename from algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/OptimizingATRManager.java rename to algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/OptimizingATRManager.java index 82ff321d10..98439d2e57 100644 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/manager/OptimizingATRManager.java +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spa/manager/OptimizingATRManager.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa.manager; +package de.learnlib.algorithms.procedural.spa.manager; import java.util.ArrayList; import java.util.Collection; @@ -25,23 +25,33 @@ import com.google.common.collect.Maps; import com.google.common.collect.Sets; import com.google.common.collect.Streams; -import de.learnlib.algorithms.spa.ATRManager; +import de.learnlib.algorithms.procedural.spa.ATRManager; import de.learnlib.api.AccessSequenceTransformer; import net.automatalib.automata.fsa.DFA; import net.automatalib.util.automata.cover.Covers; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.WordBuilder; +import org.checkerframework.checker.nullness.qual.Nullable; +/** + * An optimizing {@link ATRManager} that continuously scans positive counterexamples and procedural models in order to + * find shorter access sequences, terminating sequences, and return sequences. + * + * @param + * input symbol type + * + * @author frohme + */ public class OptimizingATRManager implements ATRManager { private final Map> accessSequences; private final Map> returnSequences; private final Map> terminatingSequences; - private final SPAAlphabet alphabet; + private final ProceduralInputAlphabet alphabet; - public OptimizingATRManager(SPAAlphabet alphabet) { + public OptimizingATRManager(ProceduralInputAlphabet alphabet) { this.alphabet = alphabet; this.accessSequences = Maps.newHashMapWithExpectedSize(alphabet.getNumCalls()); @@ -79,9 +89,9 @@ public Set scanPositiveCounterexample(Word input) { } @Override - public void scanRefinedProcedures(Map> procedures, - Map> providers, - Collection inputs) { + public void scanProcedures(Map> procedures, + Map> providers, + Collection inputs) { if (!procedures.isEmpty()) { boolean foundImprovements = false; @@ -112,9 +122,9 @@ public void scanRefinedProcedures(Map> procedures, } } - private Word getShortestHypothesisTS(DFA hyp, - AccessSequenceTransformer asTransformer, - Collection inputs) { + private @Nullable Word getShortestHypothesisTS(DFA hyp, + AccessSequenceTransformer asTransformer, + Collection inputs) { return Streams.stream(Covers.stateCoverIterator(hyp, inputs)) .filter(hyp::accepts) .map(asTransformer::transformAccessSequence) diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ATManager.java new file mode 100644 index 0000000000..97db2773c5 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ATManager.java @@ -0,0 +1,93 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import java.util.Collection; +import java.util.Map; +import java.util.Set; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.commons.util.Pair; +import net.automatalib.words.Word; + +/** + * A manager of access sequences and terminating sequences of {@link SPMM}s during the learning process. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public interface ATManager { + + /** + * Returns an access sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the access sequence for the given procedure + */ + Word getAccessSequence(I procedure); + + /** + * Returns a terminating sequence for the given procedure. + * + * @param procedure + * the call symbol that identifies the procedure + * + * @return the terminating sequence for the given procedure + */ + Word getTerminatingSequence(I procedure); + + /** + * Extracts from a positive counterexample (potentially new) access sequences and terminating sequences. + * + * @param counterexample + * the counterexample + * + * @return a {@link Pair} of {@link Set}s of procedures (identified by their respective call symbols) for which new + * access and terminating sequences could be extracted and for which previously none of the sequences were + * available. + */ + Pair, Set> scanCounterexample(DefaultQuery> counterexample); + + /** + * Scans a set of (hypothesis) procedures in order to potentially extract new access sequences and terminating + * sequences. + * + * @param procedures + * a {@link Map} from call symbols to the respective procedural (hypothesis) models + * @param providers + * a {@link Map} from call symbols to {@link AccessSequenceTransformer}s + * @param inputs + * a {@link Collection} of input symbols which should be used for finding new access sequences, terminating + * sequences, and return sequences + * + * @return a {@link Set} of procedures (identified by their respective call symbols) for which terminating sequences + * could be extracted and for which previously no such sequences were available. + */ + Set scanProcedures(Map, ?, O>> procedures, + Map>> providers, + Collection> inputs); + +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/MappingSPMM.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/MappingSPMM.java new file mode 100644 index 0000000000..764332c4d5 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/MappingSPMM.java @@ -0,0 +1,135 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import java.util.Collection; +import java.util.Map; +import java.util.Map.Entry; + +import com.google.common.collect.Maps; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.words.ProceduralInputAlphabet; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * @author frohme + */ +class MappingSPMM implements SPMM { + + private final ProceduralInputAlphabet alphabet; + private final O errorOutput; + private final Map> mapping; + private final SPMM, T, O> delegate; + + private final Map> procedures; + + MappingSPMM(ProceduralInputAlphabet alphabet, + O errorOutput, + Map> mapping, + SPMM, T, O> delegate) { + this.alphabet = alphabet; + this.errorOutput = errorOutput; + this.mapping = mapping; + this.delegate = delegate; + + final Map, MealyMachine, ?, O>> p = delegate.getProcedures(); + this.procedures = Maps.newHashMapWithExpectedSize(p.size()); + + for (Entry, MealyMachine, ?, O>> e : p.entrySet()) { + procedures.put(e.getKey().getDelegate(), new MealyView<>(e.getValue())); + } + } + + @Override + public @Nullable T getTransition(S state, I i) { + final SymbolWrapper w = this.mapping.get(i); + return w == null ? null : this.delegate.getTransition(state, w); + } + + @Override + public S getInitialState() { + return this.delegate.getInitialState(); + } + + @Override + public @Nullable I getInitialProcedure() { + final SymbolWrapper init = this.delegate.getInitialProcedure(); + return init == null ? null : init.getDelegate(); + } + + @Override + public ProceduralInputAlphabet getInputAlphabet() { + return this.alphabet; + } + + @Override + public O getErrorOutput() { + return this.errorOutput; + } + + @Override + public O getTransitionOutput(T transition) { + return this.delegate.getTransitionOutput(transition); + } + + @Override + public S getSuccessor(T transition) { + return this.delegate.getSuccessor(transition); + } + + @Override + public Map> getProcedures() { + return this.procedures; + } + + private class MealyView implements MealyMachine { + + private final MealyMachine, T2, O> delegate; + + MealyView(MealyMachine, T2, O> delegate) { + this.delegate = delegate; + } + + @Override + public Collection getStates() { + return this.delegate.getStates(); + } + + @Override + public O getTransitionOutput(T2 t2) { + return this.delegate.getTransitionOutput(t2); + } + + @Override + public @Nullable T2 getTransition(S2 s2, I i) { + final SymbolWrapper w = mapping.get(i); + return w == null ? null : delegate.getTransition(s2, w); + } + + @Override + public S2 getSuccessor(T2 t2) { + return this.delegate.getSuccessor(t2); + } + + @Override + public @Nullable S2 getInitialState() { + return this.delegate.getInitialState(); + } + } + +} \ No newline at end of file diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ProceduralMembershipOracle.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ProceduralMembershipOracle.java new file mode 100644 index 0000000000..d7ffc6accc --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/ProceduralMembershipOracle.java @@ -0,0 +1,163 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Collection; +import java.util.Collections; +import java.util.List; +import java.util.stream.Collectors; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.api.query.Query; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; + +/** + * @author frohme + */ +class ProceduralMembershipOracle implements MembershipOracle, Word> { + + private final ProceduralInputAlphabet alphabet; + private final MembershipOracle> delegate; + private final I procedure; + private final O errorSymbol; + private final ATManager atManager; + + ProceduralMembershipOracle(ProceduralInputAlphabet alphabet, + MembershipOracle> delegate, + I procedure, + O errorSymbol, + ATManager atManager) { + this.alphabet = alphabet; + this.delegate = delegate; + this.procedure = procedure; + this.errorSymbol = errorSymbol; + this.atManager = atManager; + } + + @Override + public void processQueries(Collection, Word>> collection) { + final List>> transformedQueries = new ArrayList<>(collection.size()); + + for (Query, Word> q : collection) { + if (hasErrorInPrefix(q.getPrefix())) { + q.answer(Word.fromList(Collections.nCopies(q.getSuffix().length(), errorSymbol))); + } else { + transformedQueries.add(new TransformedQuery(q)); + } + } + + this.delegate.processQueries(transformedQueries); + } + + private Word transformPrefix(Word> query) { + final WordBuilder builder = new WordBuilder<>(); + builder.append(atManager.getAccessSequence(this.procedure)); + + for (SymbolWrapper wrapper : query) { + final I i = wrapper.getDelegate(); + if (alphabet.isInternalSymbol(i)) { + builder.append(i); + } else if (alphabet.isCallSymbol(i)) { + builder.append(i); + builder.append(atManager.getTerminatingSequence(i)); + builder.append(alphabet.getReturnSymbol()); + } else { // return symbol + throw new IllegalStateException("Prefixes should not contain return symbol"); + } + } + + return builder.toWord(); + } + + private Word transformSuffix(Word> query, BitSet indices) { + final WordBuilder builder = new WordBuilder<>(); + + for (SymbolWrapper wrapper : query) { + final I i = wrapper.getDelegate(); + indices.set(builder.size()); + if (alphabet.isInternalSymbol(i)) { + builder.append(i); + } else if (alphabet.isCallSymbol(i)) { + builder.append(i); + if (wrapper.isContinuable()) { + builder.append(atManager.getTerminatingSequence(i)); + builder.append(alphabet.getReturnSymbol()); + } else { + return builder.toWord(); + } + } else { // return symbol + builder.append(i); + return builder.toWord(); + } + } + + return builder.toWord(); + } + + private boolean hasErrorInPrefix(Word> prefix) { + + for (SymbolWrapper wrapper : prefix) { + if (!wrapper.isContinuable()) { + return true; + } + } + + return false; + } + + private class TransformedQuery extends Query> { + + private final Query, Word> originalQuery; + private final Word transformedPrefix; + private final Word transformedSuffix; + private final BitSet outputIndices; + + TransformedQuery(Query, Word> originalQuery) { + this.originalQuery = originalQuery; + this.outputIndices = new BitSet(); + + this.transformedPrefix = transformPrefix(originalQuery.getPrefix()); + this.transformedSuffix = transformSuffix(originalQuery.getSuffix(), outputIndices); + } + + @Override + public void answer(Word output) { + final List out = outputIndices.stream().mapToObj(output::getSymbol).collect(Collectors.toList()); + + // fill up with skipped symbols + for (int i = out.size(); i < originalQuery.getSuffix().size(); i++) { + out.add(errorSymbol); + } + + this.originalQuery.answer(Word.fromList(out)); + } + + @Override + public Word getPrefix() { + return this.transformedPrefix; + } + + @Override + public Word getSuffix() { + return this.transformedSuffix; + } + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/SPMMLearner.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/SPMMLearner.java new file mode 100644 index 0000000000..81452c3ba4 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/SPMMLearner.java @@ -0,0 +1,367 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; + +import com.google.common.collect.Maps; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.spmm.manager.OptimizingATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.api.algorithm.LearningAlgorithm; +import de.learnlib.api.algorithm.LearningAlgorithm.MealyLearner; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.api.query.DefaultQuery; +import de.learnlib.util.MQUtil; +import net.automatalib.SupportsGrowingAlphabet; +import net.automatalib.automata.procedural.EmptySPMM; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.automata.procedural.StackSPMM; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.commons.util.Pair; +import net.automatalib.commons.util.mappings.Mapping; +import net.automatalib.util.automata.Automata; +import net.automatalib.util.automata.procedural.SPMMUtil; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import net.automatalib.words.impl.GrowingMapAlphabet; + +/** + * A learning algorithm for {@link SPMM}s. + * + * @param + * input symbol type + * @param + * output symbol type + * @param + * sub-learner type + * + * @author frohme + */ +public class SPMMLearner, O> & SupportsGrowingAlphabet> & AccessSequenceTransformer>> + implements LearningAlgorithm, I, Word> { + + private final ProceduralInputAlphabet alphabet; + private final O errorOutput; + private final MembershipOracle> oracle; + private final Mapping, Word>> learnerConstructors; + private final ATManager atManager; + + private final Map learners; + private I initialCallSymbol; + private O initialOutputSymbol; + + private final Map> mapping; + + public SPMMLearner(ProceduralInputAlphabet alphabet, + O errorOutput, + MembershipOracle> oracle, + LearnerConstructor, Word> learnerConstructor) { + this(alphabet, + errorOutput, + oracle, + (i) -> learnerConstructor, + new OptimizingATManager<>(alphabet, errorOutput)); + } + + public SPMMLearner(ProceduralInputAlphabet alphabet, + O errorOutput, + MembershipOracle> oracle, + Mapping, Word>> learnerConstructors, + ATManager atManager) { + this.alphabet = alphabet; + this.errorOutput = errorOutput; + this.oracle = oracle; + this.learnerConstructors = learnerConstructors; + this.atManager = atManager; + + this.learners = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls()); + this.mapping = Maps.newHashMapWithExpectedSize(this.alphabet.size()); + + for (I i : this.alphabet.getInternalAlphabet()) { + final SymbolWrapper wrapper = new SymbolWrapper<>(i, true); + this.mapping.put(i, wrapper); + } + + final SymbolWrapper wrapper = new SymbolWrapper<>(this.alphabet.getReturnSymbol(), false); + this.mapping.put(this.alphabet.getReturnSymbol(), wrapper); + } + + @Override + public void startLearning() { + // do nothing, as we have to wait for evidence that the potential main procedure actually terminates + } + + @Override + public boolean refineHypothesis(DefaultQuery> defaultQuery) { + + assert this.alphabet.isReturnMatched(defaultQuery.getInput()); + + boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery); + + while (refineHypothesisInternal(defaultQuery)) { + changed = true; + } + + ensureReturnClosure(); + + assert SPMMUtil.isValid(getHypothesisModel()); + + return changed; + } + + private boolean refineHypothesisInternal(DefaultQuery> defaultQuery) { + + final SPMM hypothesis = this.getHypothesisModel(); + + if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) { + return false; + } + + final Word input = defaultQuery.getInput(); + final Word output = defaultQuery.getOutput(); + + final int mismatchIdx = detectMismatchingIdx(hypothesis, input, output); + + // extract local ce + final int callIdx = alphabet.findCallIndex(input, mismatchIdx); + final I procedure = input.getSymbol(callIdx); + + final Pair, Word> localTraces = alphabet.project(input.subWord(callIdx + 1, mismatchIdx + 1), + output.subWord(callIdx + 1, mismatchIdx + 1), + 0); + final DefaultQuery, Word> localCE = + constructLocalCE(localTraces.getFirst(), localTraces.getSecond()); + final boolean localRefinement = this.learners.get(procedure).refineHypothesis(localCE); + assert localRefinement; + + return true; + } + + @Override + public SPMM getHypothesisModel() { + + if (this.learners.isEmpty()) { + return new EmptySPMM<>(this.alphabet, errorOutput); + } + + final Alphabet> internalAlphabet = new GrowingMapAlphabet<>(); + final Alphabet> callAlphabet = new GrowingMapAlphabet<>(); + final SymbolWrapper returnSymbol; + + final Map, ?, O>> procedures = getSubModels(); + final Map, MealyMachine, ?, O>> mappedProcedures = + Maps.newHashMapWithExpectedSize(procedures.size()); + + for (Entry, ?, O>> e : procedures.entrySet()) { + final SymbolWrapper w = this.mapping.get(e.getKey()); + assert w != null; + mappedProcedures.put(w, e.getValue()); + callAlphabet.add(w); + } + + for (I i : this.alphabet.getInternalAlphabet()) { + final SymbolWrapper w = this.mapping.get(i); + assert w != null; + internalAlphabet.add(w); + } + + returnSymbol = this.mapping.get(alphabet.getReturnSymbol()); + assert returnSymbol != null; + + final ProceduralInputAlphabet> mappedAlphabet = + new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); + + final StackSPMM, ?, O> delegate = new StackSPMM<>(mappedAlphabet, + this.mapping.get(initialCallSymbol), + initialOutputSymbol, + errorOutput, + mappedProcedures); + + return new MappingSPMM<>(alphabet, errorOutput, mapping, delegate); + } + + private boolean extractUsefulInformationFromCounterExample(DefaultQuery> defaultQuery) { + + final Word input = defaultQuery.getInput(); + final Word output = defaultQuery.getOutput(); + + // CEs should always be rooted at the main procedure + this.initialCallSymbol = input.firstSymbol(); + this.initialOutputSymbol = output.firstSymbol(); + + final Pair, Set> newSeqs = atManager.scanCounterexample(defaultQuery); + final Set newCalls = newSeqs.getFirst(); + final Set newTerms = newSeqs.getSecond(); + + boolean update = false; + + for (I call : newTerms) { + final SymbolWrapper sym = new SymbolWrapper<>(call, true); + this.mapping.put(call, sym); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(sym); + update = true; + } + } + + for (I sym : newCalls) { + update = true; + final L newLearner = learnerConstructors.get(sym) + .constructLearner(new GrowingMapAlphabet<>(this.mapping.values()), + new ProceduralMembershipOracle<>(alphabet, + oracle, + sym, + errorOutput, + atManager)); + + newLearner.startLearning(); + + // add new learner here, so that we have an AccessSequenceTransformer available when scanning for shorter ts + this.learners.put(sym, newLearner); + + // try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses + final Set newTS = + this.atManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()), + learners, + mapping.values()); + + for (I call : newTS) { + final SymbolWrapper wrapper = new SymbolWrapper<>(call, true); + this.mapping.put(call, wrapper); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(wrapper); + } + } + + // add non-terminating version for new call + if (!this.mapping.containsKey(sym)) { + final SymbolWrapper wrapper = new SymbolWrapper<>(sym, false); + this.mapping.put(sym, wrapper); + for (L learner : this.learners.values()) { + learner.addAlphabetSymbol(wrapper); + } + } + } + + return update; + } + + private Map, ?, O>> getSubModels() { + final Map, ?, O>> subModels = + Maps.newHashMapWithExpectedSize(this.learners.size()); + + for (Map.Entry entry : this.learners.entrySet()) { + subModels.put(entry.getKey(), entry.getValue().getHypothesisModel()); + } + + return subModels; + } + + private DefaultQuery, Word> constructLocalCE(Word input, Word output) { + + final WordBuilder> wb = new WordBuilder<>(input.length()); + for (I i : input) { + wb.append(mapping.get(i)); + } + + return new DefaultQuery<>(wb.toWord(), output); + } + + private void ensureReturnClosure() { + for (L learner : this.learners.values()) { + boolean stable = false; + + while (!stable) { + stable = ensureReturnClosure(learner.getHypothesisModel(), mapping.values(), learner); + } + } + } + + private boolean ensureReturnClosure(MealyMachine, T, O> hyp, + Collection> inputs, + L learner) { + + final Set>> cover = new HashSet<>(); + for (Word> sc : Automata.stateCover(hyp, inputs)) { + cover.add(learner.transformAccessSequence(sc)); + } + + for (Word> cov : cover) { + final S state = hyp.getState(cov); + + for (SymbolWrapper i : inputs) { + if (Objects.equals(i.getDelegate(), alphabet.getReturnSymbol())) { + + final S succ = hyp.getSuccessor(state, i); + + for (SymbolWrapper next : inputs) { + final O succOut = hyp.getOutput(succ, next); + + if (!Objects.equals(errorOutput, succOut)) { // error closure is violated + // TODO split prefix/suffix? Issue with learners? + final Word> lp = cov.append(i); + final DefaultQuery, Word> ce = new DefaultQuery<>(Word.epsilon(), + lp.append(next), + hyp.computeOutput(lp) + .append(errorOutput)); + final boolean refined = learner.refineHypothesis(ce); + assert refined; + return false; + } + } + } + } + } + + return true; + } + + private int detectMismatchingIdx(SPMM spmm, Word input, Word output) { + + final Iterator inIter = input.iterator(); + final Iterator outIter = output.iterator(); + + S stateIter = spmm.getInitialState(); + int idx = 0; + + while (inIter.hasNext() && outIter.hasNext()) { + final I i = inIter.next(); + final O o = outIter.next(); + + T t = spmm.getTransition(stateIter, i); + + if (t == null || !Objects.equals(o, spmm.getTransitionOutput(t))) { + return idx; + } + stateIter = spmm.getSuccessor(t); + idx++; + } + + throw new IllegalArgumentException("Non-counterexamples shouldn't be scanned for a mis-match"); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/DefaultATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/DefaultATManager.java new file mode 100644 index 0000000000..932d6d2a65 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/DefaultATManager.java @@ -0,0 +1,112 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm.manager; + +import java.util.Collection; +import java.util.Collections; +import java.util.Map; +import java.util.Objects; +import java.util.Set; + +import com.google.common.collect.Maps; +import com.google.common.collect.Sets; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.spmm.ATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.commons.util.Pair; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; + +/** + * A default {@link ATManager} that only extracts initial access sequences and terminating sequences from positive + * counterexamples. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class DefaultATManager implements ATManager { + + private final Map> accessSequences; + private final Map> terminatingSequences; + + private final ProceduralInputAlphabet inputAlphabet; + private final O errorOutput; + + public DefaultATManager(ProceduralInputAlphabet inputAlphabet, O errorOutput) { + this.inputAlphabet = inputAlphabet; + this.errorOutput = errorOutput; + + this.accessSequences = Maps.newHashMapWithExpectedSize(inputAlphabet.getNumCalls()); + this.terminatingSequences = Maps.newHashMapWithExpectedSize(inputAlphabet.getNumCalls()); + } + + @Override + public Word getAccessSequence(I procedure) { + assert this.accessSequences.containsKey(procedure); + return this.accessSequences.get(procedure); + } + + @Override + public Word getTerminatingSequence(I procedure) { + assert this.terminatingSequences.containsKey(procedure); + return this.terminatingSequences.get(procedure); + } + + @Override + public Pair, Set> scanCounterexample(DefaultQuery> counterexample) { + final Set newCalls = Sets.newHashSetWithExpectedSize(inputAlphabet.getNumCalls() - accessSequences.size()); + final Set newTerms = + Sets.newHashSetWithExpectedSize(inputAlphabet.getNumCalls() - terminatingSequences.size()); + + final Word input = counterexample.getInput(); + final Word output = counterexample.getOutput(); + + for (int i = 0; i < input.size(); i++) { + final I sym = input.getSymbol(i); + + if (this.inputAlphabet.isCallSymbol(sym)) { + + if (!this.accessSequences.containsKey(sym)) { + this.accessSequences.put(sym, input.prefix(i + 1)); + newCalls.add(sym); + } + + final int returnIdx = inputAlphabet.findReturnIndex(input, i + 1); + + if (returnIdx > 0 && !this.terminatingSequences.containsKey(sym) && + !Objects.equals(this.errorOutput, output.getSymbol(returnIdx))) { + this.terminatingSequences.put(sym, input.subWord(i + 1, returnIdx)); + newTerms.add(sym); + } + } + } + + return Pair.of(newCalls, newTerms); + } + + @Override + public Set scanProcedures(Map, ?, O>> procedures, + Map>> providers, + Collection> inputs) { + return Collections.emptySet(); + } +} diff --git a/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/OptimizingATManager.java b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/OptimizingATManager.java new file mode 100644 index 0000000000..b3932553b4 --- /dev/null +++ b/algorithms/active/procedural/src/main/java/de/learnlib/algorithms/procedural/spmm/manager/OptimizingATManager.java @@ -0,0 +1,272 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm.manager; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; + +import com.google.common.collect.Maps; +import com.google.common.collect.Sets; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.spmm.ATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.commons.util.Pair; +import net.automatalib.util.automata.cover.Covers; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.WordBuilder; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * An optimizing {@link ATManager} that continuously scans positive counterexamples and procedural models in order to + * find shorter access sequences and terminating sequences sequences. + * + * @param + * input symbol type + * @param + * output symbol type + * + * @author frohme + */ +public class OptimizingATManager implements ATManager { + + private final Map> accessSequences; + private final Map> terminatingSequences; + + private final ProceduralInputAlphabet inputAlphabet; + private final O errorOutput; + + public OptimizingATManager(ProceduralInputAlphabet inputAlphabet, O errorOutput) { + this.inputAlphabet = inputAlphabet; + this.errorOutput = errorOutput; + + this.accessSequences = Maps.newHashMapWithExpectedSize(inputAlphabet.getNumCalls()); + this.terminatingSequences = Maps.newHashMapWithExpectedSize(inputAlphabet.getNumCalls()); + } + + @Override + public Word getAccessSequence(I procedure) { + assert this.accessSequences.containsKey(procedure); + return this.accessSequences.get(procedure); + } + + @Override + public Word getTerminatingSequence(I procedure) { + assert this.terminatingSequences.containsKey(procedure); + return this.terminatingSequences.get(procedure); + } + + @Override + public Pair, Set> scanCounterexample(DefaultQuery> counterexample) { + final Set newCalls = + Sets.newHashSetWithExpectedSize(this.inputAlphabet.getNumCalls() - this.accessSequences.size()); + final Set newTerms = + Sets.newHashSetWithExpectedSize(this.inputAlphabet.getNumCalls() - this.terminatingSequences.size()); + + this.extractPotentialTerminatingSequences(counterexample, newTerms); + this.extractPotentialAccessSequences(counterexample, newCalls); + + return Pair.of(newCalls, newTerms); + } + + @Override + public Set scanProcedures(Map, ?, O>> procedures, + Map>> providers, + Collection> inputs) { + + final Set newTS = Sets.newHashSetWithExpectedSize(procedures.size()); + if (!procedures.isEmpty()) { + + final SymbolWrapper returnSymbol = inputs.stream() + .filter(i -> Objects.equals(i.getDelegate(), + inputAlphabet.getReturnSymbol())) + .findAny() + .orElseThrow(IllegalArgumentException::new); + boolean foundImprovements = false; + boolean stable = false; + + while (!stable) { + stable = true; + for (Entry, ?, O>> entry : procedures.entrySet()) { + final I i = entry.getKey(); + final MealyMachine, ?, O> automaton = entry.getValue(); + final Word currentTS = terminatingSequences.get(i); + assert providers.containsKey(i); + final Word hypTS = getShortestHypothesisTS(automaton, providers.get(i), inputs, returnSymbol); + + if (hypTS != null && (currentTS == null || hypTS.size() < currentTS.size())) { + + if (currentTS == null) { + newTS.add(i); + } + + terminatingSequences.put(i, hypTS); + stable = false; + foundImprovements = true; + } + } + } + + if (foundImprovements) { + optimizeSequences(this.accessSequences); + optimizeSequences(this.terminatingSequences); + } + } + + return newTS; + } + + private @Nullable Word getShortestHypothesisTS(MealyMachine, ?, O> hyp, + AccessSequenceTransformer> asTransformer, + Collection> inputs, + SymbolWrapper returnSymbol) { + final Iterator>> iter = Covers.stateCoverIterator(hyp, inputs); + Word result = null; + + while (iter.hasNext()) { + final Word> cover = iter.next(); + final Word> as = asTransformer.transformAccessSequence(cover); + final Word> asReturn = as.append(returnSymbol); + + if (!Objects.equals(this.errorOutput, hyp.computeOutput(asReturn).lastSymbol())) { + final Word ts = + this.inputAlphabet.expand(as.transform(SymbolWrapper::getDelegate), terminatingSequences::get); + if (result == null || result.size() > ts.size()) { + result = ts; + } + } + } + + return result; + } + + private void optimizeSequences(Map> sequences) { + for (Entry> entry : sequences.entrySet()) { + final Word currentSequence = entry.getValue(); + final Word minimized = minifyWellMatched(currentSequence); + + if (minimized.size() < currentSequence.size()) { + sequences.put(entry.getKey(), minimized); + } + } + } + + private void extractPotentialTerminatingSequences(DefaultQuery> counterexample, Set newProcedures) { + + final Word input = counterexample.getInput(); + final Word output = counterexample.getOutput(); + + for (int i = 0; i < input.size(); i++) { + final I sym = input.getSymbol(i); + + if (this.inputAlphabet.isCallSymbol(sym)) { + + final int returnIdx = inputAlphabet.findReturnIndex(input, i + 1); + + if (returnIdx > 0 && !Objects.equals(this.errorOutput, output.getSymbol(returnIdx))) { + final Word potentialTermSeq = input.subWord(i + 1, returnIdx); + final Word currentTermSeq = this.terminatingSequences.get(sym); + + if (currentTermSeq == null) { + newProcedures.add(sym); + this.terminatingSequences.put(sym, potentialTermSeq); + } else if (potentialTermSeq.size() < currentTermSeq.size()) { + this.terminatingSequences.put(sym, potentialTermSeq); + } + } + } + } + } + + private void extractPotentialAccessSequences(DefaultQuery> counterexample, Set newCalls) { + + final Word input = counterexample.getInput(); + final Word output = counterexample.getOutput(); + final List asBuilder = new ArrayList<>(input.size()); + + for (int i = 0; i < input.size(); i++) { + + final I sym = input.getSymbol(i); + + asBuilder.add(sym); + + if (this.inputAlphabet.isCallSymbol(sym)) { + + if (Objects.equals(this.errorOutput, output.getSymbol(i))) { + return; + } + + final Word currentAccSeq = this.accessSequences.get(sym); + + if (currentAccSeq == null) { + newCalls.add(sym); + this.accessSequences.put(sym, Word.fromList(asBuilder)); + } else if (asBuilder.size() < currentAccSeq.size()) { + this.accessSequences.put(sym, Word.fromList(asBuilder)); + } + } else if (this.inputAlphabet.isReturnSymbol(sym)) { + // update asBuilder + final int callIdx = inputAlphabet.findCallIndex(asBuilder, asBuilder.size() - 1); + final I procedure = asBuilder.get(callIdx); + final Word ts = terminatingSequences.get(procedure); + + assert ts != null; + + asBuilder.subList(callIdx + 1, asBuilder.size()).clear(); + asBuilder.addAll(ts.asList()); + asBuilder.add(inputAlphabet.getReturnSymbol()); + } + } + } + + @SuppressWarnings("PMD.AvoidReassigningLoopVariables") // we want to skip ahead here + private Word minifyWellMatched(Word input) { + + if (input.isEmpty()) { + return Word.epsilon(); + } + + final WordBuilder wb = new WordBuilder<>(input.size()); + + for (int i = 0; i < input.size(); i++) { + + final I sym = input.getSymbol(i); + + wb.append(sym); + + if (this.inputAlphabet.isCallSymbol(sym)) { + final int returnIdx = inputAlphabet.findReturnIndex(input, i + 1); + + if (returnIdx > -1) { + wb.append(terminatingSequences.get(sym)); + wb.append(inputAlphabet.getReturnSymbol()); + i = returnIdx; // next loop iteration starts _after_ the return symbol + } + } + } + + return wb.toWord(); + } + +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/ATManagerTest.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/ATManagerTest.java new file mode 100644 index 0000000000..8148bc4a07 --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/ATManagerTest.java @@ -0,0 +1,62 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import de.learnlib.algorithms.procedural.sba.manager.DefaultATManager; +import de.learnlib.algorithms.procedural.sba.manager.OptimizingATManager; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import org.testng.Assert; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +public class ATManagerTest { + + private static final ProceduralInputAlphabet ALPHABET; + + static { + final Alphabet callAlphabet = Alphabets.characters('A', 'C'); + final Alphabet internalAlphabet = Alphabets.characters('a', 'b'); + final char returnSymbol = 'R'; + + ALPHABET = new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); + } + + @DataProvider + public static Object[] atManager() { + return new Object[] {new DefaultATManager<>(ALPHABET), new OptimizingATManager<>(ALPHABET)}; + } + + @Test(dataProvider = "atManager") + public void testScanning(ATManager manager) { + + final Word word = Word.fromCharSequence("ABaRCbRR"); + + manager.scanPositiveCounterexample(word); + + Assert.assertEquals(manager.getAccessSequence('A'), Word.fromCharSequence("A")); + Assert.assertEquals(manager.getAccessSequence('B'), Word.fromCharSequence("AB")); + Assert.assertEquals(manager.getAccessSequence('C'), Word.fromCharSequence("ABaRC")); + + Assert.assertEquals(manager.getTerminatingSequence('A'), Word.fromCharSequence("BaRCbR")); + Assert.assertEquals(manager.getTerminatingSequence('B'), Word.fromCharSequence("a")); + Assert.assertEquals(manager.getTerminatingSequence('C'), Word.fromCharSequence("b")); + } + +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/OptimizationsTest.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/OptimizationsTest.java new file mode 100644 index 0000000000..6b7c1fe9ab --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/OptimizationsTest.java @@ -0,0 +1,70 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba; + +import java.util.Arrays; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.adapter.dfa.TTTAdapterDFA; +import de.learnlib.algorithms.procedural.sba.manager.OptimizingATManager; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.examples.sba.ExamplePalindrome; +import de.learnlib.oracle.equivalence.EQOracleChain; +import de.learnlib.oracle.equivalence.SampleSetEQOracle; +import de.learnlib.oracle.equivalence.sba.SimulatorEQOracle; +import de.learnlib.oracle.membership.SimulatorOracle; +import de.learnlib.util.Experiment; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import org.testng.Assert; +import org.testng.annotations.Test; + +/** + * A test for checking the optimizations performed by the {@link OptimizingATManager}. This test provides the + * {@link SBALearner} with a long, non-optimal counterexample first, so that following analysis steps should extract + * optimized sequences. + * + * @author frohme + */ +public class OptimizationsTest { + + @Test + public void testOptimizations() { + + final ExamplePalindrome example = ExamplePalindrome.createExample(); + final SBA sba = example.getReferenceAutomaton(); + final ProceduralInputAlphabet alphabet = example.getAlphabet(); + + final SimulatorOracle mqo = new SimulatorOracle<>(sba); + + final SampleSetEQOracle eqo1 = new SampleSetEQOracle<>(false); + eqo1.addAll(mqo, Word.fromString("STcTSaSaRaRRcRR")); + final SimulatorEQOracle eqo2 = new SimulatorEQOracle<>(sba); + final EQOracleChain, Character, Boolean> eqo = new EQOracleChain<>(Arrays.asList(eqo1, eqo2)); + + final LearnerConstructor>, SymbolWrapper, Boolean> cons = + TTTAdapterDFA::new; + final SBALearner learner = new SBALearner<>(alphabet, mqo, cons); + + final Experiment> experiment = new Experiment<>(learner, eqo, alphabet); + + experiment.run(); + + Assert.assertTrue(Automata.testEquivalence(sba, experiment.getFinalHypothesis(), alphabet)); + } +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/it/SBAIT.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/it/SBAIT.java new file mode 100644 index 0000000000..79fc6c45de --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/sba/it/SBAIT.java @@ -0,0 +1,90 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.sba.it; + +import java.util.Arrays; +import java.util.List; +import java.util.function.Function; + +import de.learnlib.acex.analyzers.AbstractNamedAcexAnalyzer; +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.adapter.dfa.DiscriminationTreeAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.KearnsVaziraniAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.LStarBaseAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.OptimalTTTAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.RivestSchapireAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.TTTAdapterDFA; +import de.learnlib.algorithms.procedural.sba.ATManager; +import de.learnlib.algorithms.procedural.sba.SBALearner; +import de.learnlib.algorithms.procedural.sba.manager.DefaultATManager; +import de.learnlib.algorithms.procedural.sba.manager.OptimizingATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.testsupport.it.learner.AbstractSBALearnerIT; +import de.learnlib.testsupport.it.learner.LearnerVariantList.SBALearnerVariantList; +import net.automatalib.SupportsGrowingAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; + +public class SBAIT extends AbstractSBALearnerIT { + + @Override + protected void addLearnerVariants(ProceduralInputAlphabet alphabet, + MembershipOracle mqOracle, + SBALearnerVariantList variants) { + + final Builder builder = new Builder<>(alphabet, mqOracle, variants); + + builder.addLearnerVariant(DiscriminationTreeAdapterDFA::new); + builder.addLearnerVariant(KearnsVaziraniAdapterDFA::new); + builder.addLearnerVariant(LStarBaseAdapterDFA::new); + builder.addLearnerVariant(OptimalTTTAdapterDFA::new); + builder.addLearnerVariant(RivestSchapireAdapterDFA::new); + builder.addLearnerVariant(TTTAdapterDFA::new); + } + + private static class Builder { + + private final ProceduralInputAlphabet alphabet; + private final MembershipOracle mqOracle; + private final SBALearnerVariantList variants; + private final List, ATManager>> atProviders; + + Builder(ProceduralInputAlphabet alphabet, MembershipOracle mqOracle, SBALearnerVariantList variants) { + this.alphabet = alphabet; + this.mqOracle = mqOracle; + this.variants = variants; + this.atProviders = Arrays.asList(DefaultATManager::new, OptimizingATManager::new); + } + + > & SupportsGrowingAlphabet> & AccessSequenceTransformer>> void addLearnerVariant( + LearnerConstructor, Boolean> provider) { + + for (AbstractNamedAcexAnalyzer analyzer : AcexAnalyzers.getAllAnalyzers()) { + for (Function, ATManager> atProvider : atProviders) { + final SBALearner learner = + new SBALearner<>(alphabet, mqOracle, (i) -> provider, analyzer, atProvider.apply(alphabet)); + final String name = + String.format("adapter=%s,analyzer=%s,manager=%s", provider, analyzer, atProvider); + variants.addLearnerVariant(name, learner); + } + } + } + } + +} diff --git a/algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/ATRManagerTest.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/ATRManagerTest.java similarity index 83% rename from algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/ATRManagerTest.java rename to algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/ATRManagerTest.java index 1542ad0618..8987fc796b 100644 --- a/algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/ATRManagerTest.java +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/ATRManagerTest.java @@ -13,29 +13,29 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package de.learnlib.algorithms.spa; +package de.learnlib.algorithms.procedural.spa; -import de.learnlib.algorithms.spa.manager.DefaultATRManager; -import de.learnlib.algorithms.spa.manager.OptimizingATRManager; +import de.learnlib.algorithms.procedural.spa.manager.DefaultATRManager; +import de.learnlib.algorithms.procedural.spa.manager.OptimizingATRManager; import net.automatalib.words.Alphabet; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.impl.Alphabets; -import net.automatalib.words.impl.DefaultSPAAlphabet; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; import org.testng.Assert; import org.testng.annotations.DataProvider; import org.testng.annotations.Test; public class ATRManagerTest { - private static final SPAAlphabet ALPHABET; + private static final ProceduralInputAlphabet ALPHABET; static { final Alphabet callAlphabet = Alphabets.characters('A', 'C'); final Alphabet internalAlphabet = Alphabets.characters('a', 'b'); final char returnSymbol = 'R'; - ALPHABET = new DefaultSPAAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); + ALPHABET = new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); } @DataProvider diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/it/SPAIT.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/it/SPAIT.java new file mode 100644 index 0000000000..9033ef76e3 --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spa/it/SPAIT.java @@ -0,0 +1,92 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spa.it; + +import java.util.Arrays; +import java.util.List; +import java.util.function.Function; + +import de.learnlib.acex.analyzers.AbstractNamedAcexAnalyzer; +import de.learnlib.acex.analyzers.AcexAnalyzers; +import de.learnlib.algorithms.procedural.adapter.dfa.DiscriminationTreeAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.KearnsVaziraniAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.LStarBaseAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.OptimalTTTAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.RivestSchapireAdapterDFA; +import de.learnlib.algorithms.procedural.adapter.dfa.TTTAdapterDFA; +import de.learnlib.algorithms.procedural.spa.ATRManager; +import de.learnlib.algorithms.procedural.spa.SPALearner; +import de.learnlib.algorithms.procedural.spa.manager.DefaultATRManager; +import de.learnlib.algorithms.procedural.spa.manager.OptimizingATRManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.testsupport.it.learner.AbstractSPALearnerIT; +import de.learnlib.testsupport.it.learner.LearnerVariantList.SPALearnerVariantList; +import net.automatalib.SupportsGrowingAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; + +public class SPAIT extends AbstractSPALearnerIT { + + @Override + protected void addLearnerVariants(ProceduralInputAlphabet alphabet, + MembershipOracle mqOracle, + SPALearnerVariantList variants) { + + final Builder builder = new Builder<>(alphabet, mqOracle, variants); + + builder.addLearnerVariant(DiscriminationTreeAdapterDFA::new); + builder.addLearnerVariant(KearnsVaziraniAdapterDFA::new); + builder.addLearnerVariant(LStarBaseAdapterDFA::new); + builder.addLearnerVariant(OptimalTTTAdapterDFA::new); + builder.addLearnerVariant(RivestSchapireAdapterDFA::new); + builder.addLearnerVariant(TTTAdapterDFA::new); + } + + private static class Builder { + + private final ProceduralInputAlphabet alphabet; + private final MembershipOracle mqOracle; + private final SPALearnerVariantList variants; + private final List, ATRManager>> atrProviders; + + Builder(ProceduralInputAlphabet alphabet, MembershipOracle mqOracle, SPALearnerVariantList variants) { + this.alphabet = alphabet; + this.mqOracle = mqOracle; + this.variants = variants; + this.atrProviders = Arrays.asList(DefaultATRManager::new, OptimizingATRManager::new); + } + + & SupportsGrowingAlphabet & AccessSequenceTransformer> void addLearnerVariant( + LearnerConstructor provider) { + + for (AbstractNamedAcexAnalyzer analyzer : AcexAnalyzers.getAllAnalyzers()) { + for (Function, ATRManager> atrProvider : atrProviders) { + final SPALearner learner = new SPALearner<>(alphabet, + mqOracle, + (i) -> provider, + analyzer, + atrProvider.apply(alphabet)); + final String name = + String.format("adapter=%s,analyzer=%s,manager=%s", provider, analyzer, atrProvider); + variants.addLearnerVariant(name, learner); + } + } + } + } + +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/ATManagerTest.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/ATManagerTest.java new file mode 100644 index 0000000000..c75af71820 --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/ATManagerTest.java @@ -0,0 +1,67 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import de.learnlib.algorithms.procedural.spmm.manager.DefaultATManager; +import de.learnlib.algorithms.procedural.spmm.manager.OptimizingATManager; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import org.testng.Assert; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +public class ATManagerTest { + + private static final ProceduralInputAlphabet ALPHABET; + private static final Character ERROR_OUTPUT; + + static { + final Alphabet callAlphabet = Alphabets.characters('A', 'C'); + final Alphabet internalAlphabet = Alphabets.characters('a', 'b'); + final char returnSymbol = 'R'; + + ALPHABET = new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol); + ERROR_OUTPUT = '✗'; + } + + @DataProvider + public static Object[] atManager() { + return new Object[] {new DefaultATManager<>(ALPHABET, ERROR_OUTPUT), + new OptimizingATManager<>(ALPHABET, ERROR_OUTPUT)}; + } + + @Test(dataProvider = "atManager") + public void testScanning(ATManager manager) { + + final Word inputWord = Word.fromCharSequence("ABaRCbRR"); + final Word outputWord = Word.fromCharSequence("✓✓x✓✓y✓✓"); + + manager.scanCounterexample(new DefaultQuery<>(Word.epsilon(), inputWord, outputWord)); + + Assert.assertEquals(manager.getAccessSequence('A'), Word.fromCharSequence("A")); + Assert.assertEquals(manager.getAccessSequence('B'), Word.fromCharSequence("AB")); + Assert.assertEquals(manager.getAccessSequence('C'), Word.fromCharSequence("ABaRC")); + + Assert.assertEquals(manager.getTerminatingSequence('A'), Word.fromCharSequence("BaRCbR")); + Assert.assertEquals(manager.getTerminatingSequence('B'), Word.fromCharSequence("a")); + Assert.assertEquals(manager.getTerminatingSequence('C'), Word.fromCharSequence("b")); + } + +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/OptimizationsTest.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/OptimizationsTest.java new file mode 100644 index 0000000000..1b7ca491db --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/OptimizationsTest.java @@ -0,0 +1,72 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm; + +import java.util.Arrays; + +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.adapter.mealy.TTTAdapterMealy; +import de.learnlib.algorithms.procedural.spmm.manager.OptimizingATManager; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.examples.spmm.ExamplePalindrome; +import de.learnlib.oracle.equivalence.EQOracleChain; +import de.learnlib.oracle.equivalence.SampleSetEQOracle; +import de.learnlib.oracle.equivalence.spmm.SimulatorEQOracle; +import de.learnlib.oracle.membership.SimulatorOracle; +import de.learnlib.util.Experiment; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import org.testng.Assert; +import org.testng.annotations.Test; + +/** + * A test for checking the optimizations performed by the {@link OptimizingATManager}. This test provides the + * {@link SPMMLearner} with a long, non-optimal counterexample first, so that following analysis steps should extract + * optimized sequences. + * + * @author frohme + */ +public class OptimizationsTest { + + @Test + public void testOptimizations() { + + final ExamplePalindrome example = ExamplePalindrome.createExample(); + final SPMM spmm = example.getReferenceAutomaton(); + final ProceduralInputAlphabet alphabet = example.getAlphabet(); + + final SimulatorOracle> mqo = new SimulatorOracle<>(spmm); + + final SampleSetEQOracle> eqo1 = new SampleSetEQOracle<>(false); + eqo1.addAll(mqo, Word.fromString("STcTSaSaRaRRcRR")); + final SimulatorEQOracle eqo2 = new SimulatorEQOracle<>(spmm); + final EQOracleChain, Character, Word> eqo = + new EQOracleChain<>(Arrays.asList(eqo1, eqo2)); + + final LearnerConstructor, Character>, SymbolWrapper, Word> + cons = TTTAdapterMealy::new; + final SPMMLearner, Character>> learner = + new SPMMLearner<>(alphabet, spmm.getErrorOutput(), mqo, cons); + + final Experiment> experiment = new Experiment<>(learner, eqo, alphabet); + + experiment.run(); + + Assert.assertTrue(Automata.testEquivalence(spmm, experiment.getFinalHypothesis(), alphabet)); + } +} diff --git a/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/it/SPMMIT.java b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/it/SPMMIT.java new file mode 100644 index 0000000000..82d81c5562 --- /dev/null +++ b/algorithms/active/procedural/src/test/java/de/learnlib/algorithms/procedural/spmm/it/SPMMIT.java @@ -0,0 +1,97 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.algorithms.procedural.spmm.it; + +import java.util.Arrays; +import java.util.List; +import java.util.function.BiFunction; + +import de.learnlib.algorithms.dhc.mealy.MealyDHC; +import de.learnlib.algorithms.procedural.SymbolWrapper; +import de.learnlib.algorithms.procedural.adapter.mealy.DiscriminationTreeAdapterMealy; +import de.learnlib.algorithms.procedural.adapter.mealy.KearnsVaziraniAdapterMealy; +import de.learnlib.algorithms.procedural.adapter.mealy.LStarBaseAdapterMealy; +import de.learnlib.algorithms.procedural.adapter.mealy.OptimalTTTAdapterMealy; +import de.learnlib.algorithms.procedural.adapter.mealy.RivestSchapireAdapterMealy; +import de.learnlib.algorithms.procedural.adapter.mealy.TTTAdapterMealy; +import de.learnlib.algorithms.procedural.spmm.ATManager; +import de.learnlib.algorithms.procedural.spmm.SPMMLearner; +import de.learnlib.algorithms.procedural.spmm.manager.DefaultATManager; +import de.learnlib.algorithms.procedural.spmm.manager.OptimizingATManager; +import de.learnlib.api.AccessSequenceTransformer; +import de.learnlib.api.algorithm.LearnerConstructor; +import de.learnlib.api.algorithm.LearningAlgorithm.MealyLearner; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.testsupport.it.learner.AbstractSPMMLearnerIT; +import de.learnlib.testsupport.it.learner.LearnerVariantList.SPMMLearnerVariantList; +import net.automatalib.SupportsGrowingAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; + +public class SPMMIT extends AbstractSPMMLearnerIT { + + @Override + protected void addLearnerVariants(ProceduralInputAlphabet alphabet, + O errorOutput, + MembershipOracle> mqOracle, + SPMMLearnerVariantList variants) { + + final Builder builder = new Builder<>(alphabet, errorOutput, mqOracle, variants); + + builder.addLearnerVariant(DiscriminationTreeAdapterMealy::new); + builder.addLearnerVariant(MealyDHC::new); + builder.addLearnerVariant(KearnsVaziraniAdapterMealy::new); + builder.addLearnerVariant(LStarBaseAdapterMealy::new); + builder.addLearnerVariant(OptimalTTTAdapterMealy::new); + builder.addLearnerVariant(RivestSchapireAdapterMealy::new); + builder.addLearnerVariant(TTTAdapterMealy::new); + } + + private static class Builder { + + private final ProceduralInputAlphabet alphabet; + private final O errorOutput; + private final MembershipOracle> mqOracle; + private final SPMMLearnerVariantList variants; + private final List, O, ATManager>> atProviders; + + Builder(ProceduralInputAlphabet alphabet, + O errorOutput, + MembershipOracle> mqOracle, + SPMMLearnerVariantList variants) { + this.alphabet = alphabet; + this.errorOutput = errorOutput; + this.mqOracle = mqOracle; + this.variants = variants; + this.atProviders = Arrays.asList(DefaultATManager::new, OptimizingATManager::new); + } + + , O> & SupportsGrowingAlphabet> & AccessSequenceTransformer>> void addLearnerVariant( + LearnerConstructor, Word> provider) { + + for (BiFunction, O, ATManager> atProvider : atProviders) { + final SPMMLearner learner = new SPMMLearner<>(alphabet, + errorOutput, + mqOracle, + (i) -> provider, + atProvider.apply(alphabet, errorOutput)); + final String name = String.format("adapter=%s,manager=%s", provider, atProvider); + variants.addLearnerVariant(name, learner); + } + } + } + +} diff --git a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ATRManager.java b/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ATRManager.java deleted file mode 100644 index ea55eb406a..0000000000 --- a/algorithms/active/spa/src/main/java/de/learnlib/algorithms/spa/ATRManager.java +++ /dev/null @@ -1,40 +0,0 @@ -/* Copyright (C) 2013-2023 TU Dortmund - * This file is part of LearnLib, http://www.learnlib.de/. - * - * 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.algorithms.spa; - -import java.util.Collection; -import java.util.Map; -import java.util.Set; - -import de.learnlib.api.AccessSequenceTransformer; -import net.automatalib.automata.fsa.DFA; -import net.automatalib.words.Word; - -public interface ATRManager { - - Word getAccessSequence(I procedure); - - Word getTerminatingSequence(I procedure); - - Word getReturnSequence(I procedure); - - Set scanPositiveCounterexample(Word counterexample); - - void scanRefinedProcedures(Map> procedures, - Map> providers, - Collection inputs); - -} diff --git a/algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/SPAIT.java b/algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/SPAIT.java deleted file mode 100644 index 4c643e57ce..0000000000 --- a/algorithms/active/spa/src/test/java/de/learnlib/algorithms/spa/SPAIT.java +++ /dev/null @@ -1,80 +0,0 @@ -/* Copyright (C) 2013-2023 TU Dortmund - * This file is part of LearnLib, http://www.learnlib.de/. - * - * 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.algorithms.spa; - -import java.util.Arrays; -import java.util.List; -import java.util.function.Function; - -import de.learnlib.algorithms.spa.adapter.DiscriminationTreeAdapter; -import de.learnlib.algorithms.spa.adapter.KearnsVaziraniAdapter; -import de.learnlib.algorithms.spa.adapter.LStarBaseAdapter; -import de.learnlib.algorithms.spa.adapter.RivestSchapireAdapter; -import de.learnlib.algorithms.spa.adapter.TTTAdapter; -import de.learnlib.algorithms.spa.manager.DefaultATRManager; -import de.learnlib.algorithms.spa.manager.OptimizingATRManager; -import de.learnlib.api.AccessSequenceTransformer; -import de.learnlib.api.algorithm.LearnerConstructor; -import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner; -import de.learnlib.api.oracle.MembershipOracle; -import de.learnlib.testsupport.it.learner.AbstractSPALearnerIT; -import de.learnlib.testsupport.it.learner.LearnerVariantList.SPALearnerVariantList; -import net.automatalib.SupportsGrowingAlphabet; -import net.automatalib.words.SPAAlphabet; - -public class SPAIT extends AbstractSPALearnerIT { - - @Override - protected void addLearnerVariants(SPAAlphabet alphabet, - MembershipOracle mqOracle, - SPALearnerVariantList variants) { - - final Builder builder = new Builder<>(alphabet, mqOracle, variants); - - builder.addLearnerVariant(DiscriminationTreeAdapter::new); - builder.addLearnerVariant(KearnsVaziraniAdapter::new); - builder.addLearnerVariant(LStarBaseAdapter::new); - builder.addLearnerVariant(RivestSchapireAdapter::new); - builder.addLearnerVariant(TTTAdapter::new); - } - - private static class Builder { - - private final SPAAlphabet alphabet; - private final MembershipOracle mqOracle; - private final SPALearnerVariantList variants; - private final List, ATRManager>> atrProviders; - - Builder(SPAAlphabet alphabet, MembershipOracle mqOracle, SPALearnerVariantList variants) { - this.alphabet = alphabet; - this.mqOracle = mqOracle; - this.variants = variants; - this.atrProviders = Arrays.asList(DefaultATRManager::new, OptimizingATRManager::new); - } - - & SupportsGrowingAlphabet & AccessSequenceTransformer> void addLearnerVariant( - LearnerConstructor provider) { - - for (Function, ATRManager> atrProvider : atrProviders) { - final SPALearner learner = - new SPALearner<>(alphabet, mqOracle, (i) -> provider, atrProvider.apply(alphabet)); - final String name = String.format("adapter=%s,provider=%s", provider, atrProvider); - variants.addLearnerVariant(name, learner); - } - } - } - -} diff --git a/distribution/pom.xml b/distribution/pom.xml index ef968fb1eb..6358afc164 100644 --- a/distribution/pom.xml +++ b/distribution/pom.xml @@ -94,7 +94,7 @@ limitations under the License. de.learnlib - learnlib-spa + learnlib-procedural @@ -351,7 +351,7 @@ limitations under the License. de.learnlib - learnlib-spa + learnlib-procedural ${project.version} sources diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/SimulatorEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/SimulatorEQOracle.java new file mode 100644 index 0000000000..de198a4620 --- /dev/null +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/SimulatorEQOracle.java @@ -0,0 +1,57 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.sba; + +import java.util.Collection; + +import de.learnlib.api.oracle.EquivalenceOracle; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * @author frohme + */ +public class SimulatorEQOracle implements EquivalenceOracle, I, Boolean> { + + private final SBA sba; + + public SimulatorEQOracle(SBA sba) { + this.sba = sba; + } + + @Override + public @Nullable DefaultQuery findCounterExample(SBA hypothesis, Collection inputs) { + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not an SPA alphabet"); + } + + @SuppressWarnings("unchecked") + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; + + final Word sep = Automata.findSeparatingWord(sba, hypothesis, alphabet); + + if (sep == null) { + return null; + } + + return new DefaultQuery<>(sep, sba.computeOutput(sep)); + } +} + diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracle.java new file mode 100644 index 0000000000..79313b86c4 --- /dev/null +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracle.java @@ -0,0 +1,110 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.sba; + +import java.util.Collection; +import java.util.stream.Stream; + +import com.google.common.collect.Streams; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.oracle.equivalence.AbstractTestWordEQOracle; +import net.automatalib.automata.concepts.FiniteRepresentation; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.util.automata.conformance.SBAWMethodTestsIterator; +import net.automatalib.util.automata.conformance.WMethodTestsIterator; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; + +/** + * An {@link SBA} version of {@link de.learnlib.oracle.equivalence.WMethodEQOracle} which generates test sequences based + * on the {@link SBAWMethodTestsIterator W-method} for each procedure. + * + * @param + * input symbol type + * + * @author frohme + */ +public class WMethodEQOracle extends AbstractTestWordEQOracle, I, Boolean> { + + private final int lookahead; + private final int expectedSize; + + /** + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int)} that sets + * {@code expectedSize} to 0. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the maximum length of the "middle" part of the test cases + */ + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead) { + this(sulOracle, lookahead, 0); + } + + /** + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int, int)} that sets + * {@code batchSize} to 1. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the (minimal) maximum length of the "middle" part of the test cases + * @param expectedSize + * the expected size of the system under learning + */ + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize) { + this(sulOracle, lookahead, expectedSize, 1); + } + + /** + * Constructor. Uses + * {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link FiniteRepresentation#size() + * hypothesis.size()}{@code )} to determine the maximum length of sequences, that should be appended to the + * transition-cover part of the test sequence to account for the fact that the system under learning may have more + * states than the current hypothesis. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the (minimal) maximum length of the "middle" part of the test cases + * @param expectedSize + * the expected size of the system under learning + * @param batchSize + * size of the batches sent to the membership oracle + * + * @see WMethodTestsIterator + */ + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize, int batchSize) { + super(sulOracle, batchSize); + this.lookahead = lookahead; + this.expectedSize = expectedSize; + } + + @Override + protected Stream> generateTestWords(SBA hypothesis, Collection inputs) { + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not a procedural alphabet"); + } + + @SuppressWarnings("unchecked") + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; + + return Streams.stream(new SBAWMethodTestsIterator<>(hypothesis, + alphabet, + Math.max(lookahead, expectedSize - hypothesis.size()))); + } +} \ No newline at end of file diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/SimulatorEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/SimulatorEQOracle.java index a09438e55a..9d1591b7b4 100644 --- a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/SimulatorEQOracle.java +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/SimulatorEQOracle.java @@ -19,9 +19,9 @@ import de.learnlib.api.oracle.EquivalenceOracle; import de.learnlib.api.query.DefaultQuery; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.Automata; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import org.checkerframework.checker.nullness.qual.Nullable; @@ -35,12 +35,12 @@ public SimulatorEQOracle(SPA spa) { @Override public @Nullable DefaultQuery findCounterExample(SPA hypothesis, Collection inputs) { - if (!(inputs instanceof SPAAlphabet)) { - throw new IllegalArgumentException("Inputs are not an SPA alphabet"); + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not a procedural alphabet"); } @SuppressWarnings("unchecked") - final SPAAlphabet alphabet = (SPAAlphabet) inputs; + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; final Word sep = Automata.findSeparatingWord(spa, hypothesis, alphabet); diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracle.java similarity index 68% rename from oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracle.java rename to oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracle.java index 085383ca8b..f5679ca4a9 100644 --- a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracle.java +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracle.java @@ -21,44 +21,43 @@ import com.google.common.collect.Streams; import de.learnlib.api.oracle.MembershipOracle; import de.learnlib.oracle.equivalence.AbstractTestWordEQOracle; -import de.learnlib.oracle.equivalence.WMethodEQOracle; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.conformance.SPATestsIterator; import net.automatalib.util.automata.conformance.WMethodTestsIterator; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; /** - * An {@link SPA} version of {@link WMethodEQOracle} which generates test sequences based on the W-method for each - * procedure. + * An {@link SPA} version of {@link de.learnlib.oracle.equivalence.WMethodEQOracle} which generates test sequences based + * on the W-method for each procedure. * * @param * input symbol type * * @author frohme */ -public class WMethodSPAEQOracle extends AbstractTestWordEQOracle, I, Boolean> { +public class WMethodEQOracle extends AbstractTestWordEQOracle, I, Boolean> { private final int lookahead; private final int expectedSize; /** - * Constructor. Convenience method for {@link #WMethodSPAEQOracle(MembershipOracle, int, int)} that sets {@code - * expectedSize} to 0. + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int)} that sets + * {@code expectedSize} to 0. * * @param sulOracle * interface to the system under learning * @param lookahead * the maximum length of the "middle" part of the test cases */ - public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead) { + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead) { this(sulOracle, lookahead, 0); } /** - * Constructor. Convenience method for {@link #WMethodSPAEQOracle(MembershipOracle, int, int, int)} that sets {@code - * batchSize} to 1. + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int, int)} that sets + * {@code batchSize} to 1. * * @param sulOracle * interface to the system under learning @@ -67,15 +66,16 @@ public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead) * @param expectedSize * the expected size of the system under learning */ - public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize) { + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize) { this(sulOracle, lookahead, expectedSize, 1); } /** - * Constructor. Uses {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link DFA#size() - * hypothesis.size()}{@code )} (for each procedural {@code hypothesis}) to determine the maximum length of - * sequences, that should be appended to the transition-cover part of the test sequence to account for the fact that - * the system under learning may have more states than the current hypothesis. + * Constructor. Uses + * {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link DFA#size() hypothesis.size()}{@code + * )} (for each procedural {@code hypothesis}) to determine the maximum length of sequences, that should be appended + * to the transition-cover part of the test sequence to account for the fact that the system under learning may have + * more states than the current hypothesis. * * @param sulOracle * interface to the system under learning @@ -88,7 +88,7 @@ public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, * * @see WMethodTestsIterator */ - public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize, int batchSize) { + public WMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize, int batchSize) { super(sulOracle, batchSize); this.lookahead = lookahead; this.expectedSize = expectedSize; @@ -96,12 +96,12 @@ public WMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, @Override protected Stream> generateTestWords(SPA hypothesis, Collection inputs) { - if (!(inputs instanceof SPAAlphabet)) { - throw new IllegalArgumentException("Inputs are not an SPA alphabet"); + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not a procedural alphabet"); } @SuppressWarnings("unchecked") - final SPAAlphabet alphabet = (SPAAlphabet) inputs; + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; return Streams.stream(new SPATestsIterator<>(hypothesis, alphabet, diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracle.java similarity index 69% rename from oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracle.java rename to oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracle.java index 6d733df988..cb21d7557b 100644 --- a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracle.java +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracle.java @@ -21,44 +21,43 @@ import com.google.common.collect.Streams; import de.learnlib.api.oracle.MembershipOracle; import de.learnlib.oracle.equivalence.AbstractTestWordEQOracle; -import de.learnlib.oracle.equivalence.WpMethodEQOracle; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.conformance.SPATestsIterator; import net.automatalib.util.automata.conformance.WMethodTestsIterator; import net.automatalib.util.automata.conformance.WpMethodTestsIterator; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; /** - * An {@link SPA} version of {@link WpMethodEQOracle} which generates test sequences based on the partial W-method for - * each procedure. + * An {@link SPA} version of {@link de.learnlib.oracle.equivalence.WpMethodEQOracle} which generates test sequences + * based on the partial W-method for each procedure. * * @param * input symbol type * * @author frohme */ -public class WpMethodSPAEQOracle extends AbstractTestWordEQOracle, I, Boolean> { +public class WpMethodEQOracle extends AbstractTestWordEQOracle, I, Boolean> { private final int lookahead; private final int expectedSize; /** - * Constructor. Convenience method for {@link #WpMethodSPAEQOracle(MembershipOracle, int, int)} that sets {@code - * expectedSize} to 0. + * Constructor. Convenience method for {@link #WpMethodEQOracle(MembershipOracle, int, int)} that sets + * {@code expectedSize} to 0. * * @param sulOracle * interface to the system under learning * @param lookahead * the maximum length of the "middle" part of the test cases */ - public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead) { + public WpMethodEQOracle(MembershipOracle sulOracle, int lookahead) { this(sulOracle, lookahead, 0); } /** - * Constructor. Convenience method for {@link #WpMethodSPAEQOracle(MembershipOracle, int, int, int)} that sets + * Constructor. Convenience method for {@link #WpMethodEQOracle(MembershipOracle, int, int, int)} that sets * {@code batchSize} to 1. * * @param sulOracle @@ -68,15 +67,16 @@ public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead * @param expectedSize * the expected size of the system under learning */ - public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize) { + public WpMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize) { this(sulOracle, lookahead, expectedSize, 1); } /** - * Constructor. Uses {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link DFA#size() - * hypothesis.size()}{@code )} (for each procedural {@code hypothesis}) to determine the maximum length of - * sequences, that should be appended to the transition-cover part of the test sequence to account for the fact that - * the system under learning may have more states than the current hypothesis. + * Constructor. Uses + * {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link DFA#size() hypothesis.size()}{@code + * )} (for each procedural {@code hypothesis}) to determine the maximum length of sequences, that should be appended + * to the transition-cover part of the test sequence to account for the fact that the system under learning may have + * more states than the current hypothesis. * * @param sulOracle * interface to the system under learning @@ -89,7 +89,7 @@ public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead * * @see WMethodTestsIterator */ - public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize, int batchSize) { + public WpMethodEQOracle(MembershipOracle sulOracle, int lookahead, int expectedSize, int batchSize) { super(sulOracle, batchSize); this.lookahead = lookahead; this.expectedSize = expectedSize; @@ -97,12 +97,12 @@ public WpMethodSPAEQOracle(MembershipOracle sulOracle, int lookahead @Override protected Stream> generateTestWords(SPA hypothesis, Collection inputs) { - if (!(inputs instanceof SPAAlphabet)) { - throw new IllegalArgumentException("Inputs are not an SPA alphabet"); + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not a procedural alphabet"); } @SuppressWarnings("unchecked") - final SPAAlphabet alphabet = (SPAAlphabet) inputs; + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; return Streams.stream(new SPATestsIterator<>(hypothesis, alphabet, diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/SimulatorEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/SimulatorEQOracle.java new file mode 100644 index 0000000000..c44d3329be --- /dev/null +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/SimulatorEQOracle.java @@ -0,0 +1,58 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.spmm; + +import java.util.Collection; + +import de.learnlib.api.oracle.EquivalenceOracle; +import de.learnlib.api.query.DefaultQuery; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * @author frohme + */ +public class SimulatorEQOracle implements EquivalenceOracle, I, Word> { + + private final SPMM spmm; + + public SimulatorEQOracle(SPMM spmm) { + this.spmm = spmm; + } + + @Override + public @Nullable DefaultQuery> findCounterExample(SPMM hypothesis, + Collection inputs) { + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not an SPA alphabet"); + } + + @SuppressWarnings("unchecked") + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; + + final Word sep = Automata.findSeparatingWord(spmm, hypothesis, alphabet); + + if (sep == null) { + return null; + } + + return new DefaultQuery<>(sep, spmm.computeOutput(sep)); + } +} + diff --git a/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracle.java b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracle.java new file mode 100644 index 0000000000..e5090f4eff --- /dev/null +++ b/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracle.java @@ -0,0 +1,111 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.spmm; + +import java.util.Collection; +import java.util.stream.Stream; + +import com.google.common.collect.Streams; +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.oracle.equivalence.AbstractTestWordEQOracle; +import net.automatalib.automata.concepts.FiniteRepresentation; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.util.automata.conformance.SPMMWMethodTestsIterator; +import net.automatalib.util.automata.conformance.WMethodTestsIterator; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; + +/** + * Implements an equivalence test by applying the W-method test on the procedures of the given hypothesis {@link SBA}, + * as described in "Testing software design modeled by finite state machines" by T.S. Chow. + * + * @param + * input symbol type + * + * @author frohme + */ +public class WMethodEQOracle extends AbstractTestWordEQOracle, I, Word> { + + private final int lookahead; + private final int expectedSize; + + /** + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int)} that sets + * {@code expectedSize} to 0. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the maximum length of the "middle" part of the test cases + */ + public WMethodEQOracle(MembershipOracle> sulOracle, int lookahead) { + this(sulOracle, lookahead, 0); + } + + /** + * Constructor. Convenience method for {@link #WMethodEQOracle(MembershipOracle, int, int, int)} that sets + * {@code batchSize} to 1. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the (minimal) maximum length of the "middle" part of the test cases + * @param expectedSize + * the expected size of the system under learning + */ + public WMethodEQOracle(MembershipOracle> sulOracle, int lookahead, int expectedSize) { + this(sulOracle, lookahead, expectedSize, 1); + } + + /** + * Constructor. Uses + * {@link Math#max(int, int) Math.max}{@code (lookahead, expectedSize - }{@link FiniteRepresentation#size() + * hypothesis.size()}{@code )} to determine the maximum length of sequences, that should be appended to the + * transition-cover part of the test sequence to account for the fact that the system under learning may have more + * states than the current hypothesis. + * + * @param sulOracle + * interface to the system under learning + * @param lookahead + * the (minimal) maximum length of the "middle" part of the test cases + * @param expectedSize + * the expected size of the system under learning + * @param batchSize + * size of the batches sent to the membership oracle + * + * @see WMethodTestsIterator + */ + public WMethodEQOracle(MembershipOracle> sulOracle, int lookahead, int expectedSize, int batchSize) { + super(sulOracle, batchSize); + this.lookahead = lookahead; + this.expectedSize = expectedSize; + } + + @Override + protected Stream> generateTestWords(SPMM hypothesis, Collection inputs) { + if (!(inputs instanceof ProceduralInputAlphabet)) { + throw new IllegalArgumentException("Inputs are not a procedural alphabet"); + } + + @SuppressWarnings("unchecked") + final ProceduralInputAlphabet alphabet = (ProceduralInputAlphabet) inputs; + + return Streams.stream(new SPMMWMethodTestsIterator<>(hypothesis, + alphabet, + Math.max(lookahead, expectedSize - hypothesis.size()))); + } +} \ No newline at end of file diff --git a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracleTest.java b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracleTest.java new file mode 100644 index 0000000000..fcd4301003 --- /dev/null +++ b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/sba/WMethodEQOracleTest.java @@ -0,0 +1,54 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.sba; + +import java.util.List; +import java.util.Random; +import java.util.stream.Collectors; + +import com.google.common.collect.Streams; +import de.learnlib.oracle.membership.SimulatorOracle; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.util.automata.conformance.SBAWMethodTestsIterator; +import net.automatalib.util.automata.random.RandomAutomata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import org.testng.Assert; +import org.testng.annotations.Test; + +public class WMethodEQOracleTest { + + @Test + public void testOracle() { + final Random random = new Random(42); + final ProceduralInputAlphabet alphabet = + new DefaultProceduralInputAlphabet<>(Alphabets.characters('x', 'z'), + Alphabets.characters('A', 'C'), + 'R'); + final SBA sba = RandomAutomata.randomSBA(random, alphabet, 4); + final int lookahead = 2; + + final WMethodEQOracle oracle = new WMethodEQOracle<>(new SimulatorOracle<>(sba), lookahead); + + final List> eqWords = oracle.generateTestWords(sba, alphabet).collect(Collectors.toList()); + final List> testWords = + Streams.stream(new SBAWMethodTestsIterator<>(sba, alphabet, lookahead)).collect(Collectors.toList()); + + Assert.assertEquals(eqWords, testWords); + } +} \ No newline at end of file diff --git a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracleTest.java b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracleTest.java similarity index 75% rename from oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracleTest.java rename to oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracleTest.java index b59455fe18..69fbe311a4 100644 --- a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodSPAEQOracleTest.java +++ b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WMethodEQOracleTest.java @@ -21,28 +21,30 @@ import com.google.common.collect.Streams; import de.learnlib.oracle.membership.SimulatorOracle; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.conformance.SPATestsIterator; import net.automatalib.util.automata.conformance.WMethodTestsIterator; import net.automatalib.util.automata.random.RandomAutomata; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.impl.Alphabets; -import net.automatalib.words.impl.DefaultSPAAlphabet; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; import org.testng.Assert; import org.testng.annotations.Test; -public class WMethodSPAEQOracleTest { +public class WMethodEQOracleTest { @Test public void testOracle() { final Random random = new Random(42); - final SPAAlphabet alphabet = - new DefaultSPAAlphabet<>(Alphabets.characters('x', 'z'), Alphabets.characters('A', 'C'), 'R'); - final SPA spa = RandomAutomata.randomRedundancyFreeSPA(random, alphabet, 4); + final ProceduralInputAlphabet alphabet = + new DefaultProceduralInputAlphabet<>(Alphabets.characters('x', 'z'), + Alphabets.characters('A', 'C'), + 'R'); + final SPA spa = RandomAutomata.randomSPA(random, alphabet, 4); final int lookahead = 2; - final WMethodSPAEQOracle oracle = new WMethodSPAEQOracle<>(new SimulatorOracle<>(spa), lookahead); + final WMethodEQOracle oracle = new WMethodEQOracle<>(new SimulatorOracle<>(spa), lookahead); final List> eqWords = oracle.generateTestWords(spa, alphabet).collect(Collectors.toList()); final List> testWords = Streams.stream(new SPATestsIterator<>(spa, diff --git a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracleTest.java b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracleTest.java similarity index 75% rename from oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracleTest.java rename to oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracleTest.java index cd0d65308b..4e86b79faa 100644 --- a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodSPAEQOracleTest.java +++ b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spa/WpMethodEQOracleTest.java @@ -21,28 +21,30 @@ import com.google.common.collect.Streams; import de.learnlib.oracle.membership.SimulatorOracle; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.conformance.SPATestsIterator; import net.automatalib.util.automata.conformance.WpMethodTestsIterator; import net.automatalib.util.automata.random.RandomAutomata; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.Word; import net.automatalib.words.impl.Alphabets; -import net.automatalib.words.impl.DefaultSPAAlphabet; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; import org.testng.Assert; import org.testng.annotations.Test; -public class WpMethodSPAEQOracleTest { +public class WpMethodEQOracleTest { @Test public void testOracle() { final Random random = new Random(42); - final SPAAlphabet alphabet = - new DefaultSPAAlphabet<>(Alphabets.characters('x', 'z'), Alphabets.characters('A', 'C'), 'R'); - final SPA spa = RandomAutomata.randomRedundancyFreeSPA(random, alphabet, 4); + final ProceduralInputAlphabet alphabet = + new DefaultProceduralInputAlphabet<>(Alphabets.characters('x', 'z'), + Alphabets.characters('A', 'C'), + 'R'); + final SPA spa = RandomAutomata.randomSPA(random, alphabet, 4); final int lookahead = 2; - final WpMethodSPAEQOracle oracle = new WpMethodSPAEQOracle<>(new SimulatorOracle<>(spa), lookahead); + final WpMethodEQOracle oracle = new WpMethodEQOracle<>(new SimulatorOracle<>(spa), lookahead); final List> eqWords = oracle.generateTestWords(spa, alphabet).collect(Collectors.toList()); final List> testWords = Streams.stream(new SPATestsIterator<>(spa, diff --git a/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracleTest.java b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracleTest.java new file mode 100644 index 0000000000..20615d6491 --- /dev/null +++ b/oracles/equivalence-oracles/src/test/java/de/learnlib/oracle/equivalence/spmm/WMethodEQOracleTest.java @@ -0,0 +1,62 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.oracle.equivalence.spmm; + +import java.util.List; +import java.util.Random; +import java.util.stream.Collectors; + +import com.google.common.collect.Streams; +import de.learnlib.oracle.membership.SimulatorOracle; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.util.automata.conformance.SPMMWMethodTestsIterator; +import net.automatalib.util.automata.random.RandomAutomata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.ProceduralOutputAlphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import net.automatalib.words.impl.DefaultProceduralOutputAlphabet; +import org.testng.Assert; +import org.testng.annotations.Test; + +public class WMethodEQOracleTest { + + @Test + public void testOracle() { + final Random random = new Random(42); + final ProceduralInputAlphabet inputAlphabet = + new DefaultProceduralInputAlphabet<>(Alphabets.characters('x', 'z'), + Alphabets.characters('A', 'C'), + 'R'); + final ProceduralOutputAlphabet outputAlphabet = + new DefaultProceduralOutputAlphabet<>(Alphabets.characters('d', 'f'), '-'); + final SPMM spmm = + RandomAutomata.randomSPMM(random, inputAlphabet, outputAlphabet, 4); + final int lookahead = 2; + + final WMethodEQOracle oracle = + new WMethodEQOracle<>(new SimulatorOracle<>(spmm), lookahead); + + final List> eqWords = + oracle.generateTestWords(spmm, inputAlphabet).collect(Collectors.toList()); + final List> testWords = + Streams.stream(new SPMMWMethodTestsIterator<>(spmm, inputAlphabet, lookahead)) + .collect(Collectors.toList()); + + Assert.assertEquals(eqWords, testWords); + } +} \ No newline at end of file diff --git a/pom.xml b/pom.xml index 034d069cd7..3891dfd7a2 100644 --- a/pom.xml +++ b/pom.xml @@ -325,7 +325,7 @@ limitations under the License. de.learnlib - learnlib-spa + learnlib-procedural ${project.version} diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSBALearnerIT.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSBALearnerIT.java new file mode 100644 index 0000000000..fa93b0a75d --- /dev/null +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSBALearnerIT.java @@ -0,0 +1,77 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.testsupport.it.learner; + +import java.util.ArrayList; +import java.util.List; + +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.examples.LearningExample.SBALearningExample; +import de.learnlib.examples.LearningExamples; +import de.learnlib.oracle.equivalence.sba.SimulatorEQOracle; +import de.learnlib.oracle.membership.SimulatorOracle; +import de.learnlib.testsupport.it.learner.LearnerVariantList.SBALearnerVariantList; +import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SBALearnerVariantListImpl; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.words.ProceduralInputAlphabet; +import org.testng.annotations.Factory; + +/** + * Abstract integration test for {@link SBA} learning algorithms. + * + * @author frohme + */ +public abstract class AbstractSBALearnerIT { + + @Factory + public Object[] createExampleITCases() { + final List> examples = LearningExamples.createSBAExamples(); + final List> result = new ArrayList<>(examples.size()); + + for (SBALearningExample example : examples) { + result.addAll(createAllVariantsITCase(example)); + } + + return result.toArray(); + } + + private List> createAllVariantsITCase(SBALearningExample example) { + + final ProceduralInputAlphabet alphabet = example.getAlphabet(); + final MembershipOracle mqOracle = new SimulatorOracle<>(example.getReferenceAutomaton()); + final SBALearnerVariantListImpl variants = new SBALearnerVariantListImpl<>(); + addLearnerVariants(alphabet, mqOracle, variants); + + return LearnerITUtil.createExampleITCases(example, + variants, + new SimulatorEQOracle<>(example.getReferenceAutomaton())); + } + + /** + * Adds, for a given setup, all the variants of the DFA learner to be tested to the specified + * {@link LearnerVariantList variant list}. + * + * @param alphabet + * the input alphabet + * @param mqOracle + * the membership oracle + * @param variants + * list to add the learner variants to + */ + protected abstract void addLearnerVariants(ProceduralInputAlphabet alphabet, + MembershipOracle mqOracle, + SBALearnerVariantList variants); +} diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPALearnerIT.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPALearnerIT.java index c7a869cef4..70f0194951 100644 --- a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPALearnerIT.java +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPALearnerIT.java @@ -25,11 +25,12 @@ import de.learnlib.oracle.membership.SimulatorOracle; import de.learnlib.testsupport.it.learner.LearnerVariantList.SPALearnerVariantList; import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SPALearnerVariantListImpl; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.words.ProceduralInputAlphabet; import org.testng.annotations.Factory; /** - * Abstract integration test for VPDA learning algorithms. + * Abstract integration test for {@link SPA} learning algorithms. * * @author frohme */ @@ -49,7 +50,7 @@ public Object[] createExampleITCases() { private List> createAllVariantsITCase(SPALearningExample example) { - final SPAAlphabet alphabet = example.getAlphabet(); + final ProceduralInputAlphabet alphabet = example.getAlphabet(); final MembershipOracle mqOracle = new SimulatorOracle<>(example.getReferenceAutomaton()); final SPALearnerVariantListImpl variants = new SPALearnerVariantListImpl<>(); addLearnerVariants(alphabet, mqOracle, variants); @@ -60,8 +61,8 @@ private List> createAllVariantsITCase(SPALearningExample } /** - * Adds, for a given setup, all the variants of the DFA learner to be tested to the specified {@link - * LearnerVariantList variant list}. + * Adds, for a given setup, all the variants of the DFA learner to be tested to the specified + * {@link LearnerVariantList variant list}. * * @param alphabet * the input alphabet @@ -70,7 +71,7 @@ private List> createAllVariantsITCase(SPALearningExample * @param variants * list to add the learner variants to */ - protected abstract void addLearnerVariants(SPAAlphabet alphabet, + protected abstract void addLearnerVariants(ProceduralInputAlphabet alphabet, MembershipOracle mqOracle, SPALearnerVariantList variants); } diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPMMLearnerIT.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPMMLearnerIT.java new file mode 100644 index 0000000000..fb5ea3a89f --- /dev/null +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/AbstractSPMMLearnerIT.java @@ -0,0 +1,79 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.testsupport.it.learner; + +import java.util.ArrayList; +import java.util.List; + +import de.learnlib.api.oracle.MembershipOracle; +import de.learnlib.examples.LearningExample.SPMMLearningExample; +import de.learnlib.examples.LearningExamples; +import de.learnlib.oracle.equivalence.spmm.SimulatorEQOracle; +import de.learnlib.oracle.membership.SimulatorOracle; +import de.learnlib.testsupport.it.learner.LearnerVariantList.SPMMLearnerVariantList; +import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SPMMLearnerVariantListImpl; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.Word; +import org.testng.annotations.Factory; + +/** + * Abstract integration test for {@link SPMM} learning algorithms. + * + * @author frohme + */ +public abstract class AbstractSPMMLearnerIT { + + @Factory + public Object[] createExampleITCases() { + final List> examples = LearningExamples.createSPMMExamples(); + final List> result = new ArrayList<>(examples.size()); + + for (SPMMLearningExample example : examples) { + result.addAll(createAllVariantsITCase(example)); + } + + return result.toArray(); + } + + private List> createAllVariantsITCase(SPMMLearningExample example) { + + final SPMM reference = example.getReferenceAutomaton(); + final MembershipOracle> mqOracle = new SimulatorOracle<>(reference); + final SPMMLearnerVariantListImpl variants = new SPMMLearnerVariantListImpl<>(); + addLearnerVariants(example.getAlphabet(), reference.getErrorOutput(), mqOracle, variants); + + return LearnerITUtil.createExampleITCases(example, variants, new SimulatorEQOracle<>(reference)); + } + + /** + * Adds, for a given setup, all the variants of the DFA learner to be tested to the specified + * {@link LearnerVariantList variant list}. + * + * @param alphabet + * the input alphabet + * @param errorOutput + * the erroneous output symbol + * @param mqOracle + * the membership oracle + * @param variants + * list to add the learner variants to + */ + protected abstract void addLearnerVariants(ProceduralInputAlphabet alphabet, + O errorOutput, + MembershipOracle> mqOracle, + SPMMLearnerVariantList variants); +} diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerITUtil.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerITUtil.java index 945c6850a3..82cdf44ed5 100644 --- a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerITUtil.java +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerITUtil.java @@ -24,16 +24,22 @@ import de.learnlib.api.query.DefaultQuery; import de.learnlib.examples.LearningExample; import de.learnlib.examples.LearningExample.OneSEVPALearningExample; +import de.learnlib.examples.LearningExample.SBALearningExample; import de.learnlib.examples.LearningExample.SPALearningExample; +import de.learnlib.examples.LearningExample.SPMMLearningExample; import de.learnlib.examples.LearningExample.UniversalDeterministicLearningExample; import de.learnlib.examples.PassiveLearningExample; import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.OneSEVPALearnerVariantListImpl; +import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SBALearnerVariantListImpl; import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SPALearnerVariantListImpl; +import de.learnlib.testsupport.it.learner.LearnerVariantListImpl.SPMMLearnerVariantListImpl; import net.automatalib.automata.UniversalAutomaton; import net.automatalib.automata.UniversalDeterministicAutomaton; import net.automatalib.automata.concepts.FiniteRepresentation; import net.automatalib.automata.concepts.SuffixOutput; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.SPMM; import net.automatalib.automata.vpda.OneSEVPA; import net.automatalib.words.Alphabet; import net.automatalib.words.Word; @@ -89,6 +95,38 @@ public static List> createExampleITCases(SPALearningExam SPALearnerITCase::new); } + /** + * Creates a list of per-example test cases for all learner variants. + * + * @return the list of test cases, one for each example + */ + public static List> createExampleITCases(SBALearningExample example, + SBALearnerVariantListImpl variants, + EquivalenceOracle, I, Boolean> eqOracle) { + // explicit generics are required for correct type-inference + return LearnerITUtil., SBALearningExample, SBALearnerITCase>createExampleITCasesInternal( + example, + variants, + eqOracle, + SBALearnerITCase::new); + } + + /** + * Creates a list of per-example test cases for all learner variants. + * + * @return the list of test cases, one for each example + */ + public static List> createExampleITCases(SPMMLearningExample example, + SPMMLearnerVariantListImpl variants, + EquivalenceOracle, I, Word> eqOracle) { + // explicit generics are required for correct type-inference + return LearnerITUtil., SPMM, SPMMLearningExample, SPMMLearnerITCase>createExampleITCasesInternal( + example, + variants, + eqOracle, + SPMMLearnerITCase::new); + } + /** * Creates a list of per-example test cases for all learner variants. * diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantList.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantList.java index 07e36d6c72..c6d812e5b5 100644 --- a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantList.java +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantList.java @@ -17,7 +17,9 @@ import de.learnlib.api.algorithm.LearningAlgorithm; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.SPMM; import net.automatalib.automata.transducers.MealyMachine; import net.automatalib.automata.transducers.MooreMachine; import net.automatalib.automata.vpda.OneSEVPA; @@ -79,8 +81,12 @@ interface MooreLearnerVariantList extends LearnerVariantList extends LearnerVariantList, I, O> {} - interface OneSEVPALearnerVariantList extends LearnerVariantList, I, Boolean> {} - interface SPALearnerVariantList extends LearnerVariantList, I, Boolean> {} + interface SBALearnerVariantList extends LearnerVariantList, I, Boolean> {} + + interface SPMMLearnerVariantList extends LearnerVariantList, I, Word> {} + + interface OneSEVPALearnerVariantList extends LearnerVariantList, I, Boolean> {} + } diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantListImpl.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantListImpl.java index 4b62ac70b9..66012a1cc8 100644 --- a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantListImpl.java +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/LearnerVariantListImpl.java @@ -22,7 +22,9 @@ import de.learnlib.util.mealy.MealyUtil; import de.learnlib.util.moore.MooreUtil; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.SPMM; import net.automatalib.automata.transducers.MealyMachine; import net.automatalib.automata.transducers.MooreMachine; import net.automatalib.automata.vpda.OneSEVPA; @@ -64,6 +66,12 @@ public static class OneSEVPALearnerVariantListImpl extends LearnerVariantList public static class SPALearnerVariantListImpl extends LearnerVariantListImpl, I, Boolean> implements SPALearnerVariantList {} + public static class SBALearnerVariantListImpl extends LearnerVariantListImpl, I, Boolean> + implements SBALearnerVariantList {} + + public static class SPMMLearnerVariantListImpl extends LearnerVariantListImpl, I, Word> + implements SPMMLearnerVariantList {} + public static class MealySymLearnerVariantListImpl implements MealySymLearnerVariantList { private final MealyLearnerVariantListImpl mealyLearnerVariants = new MealyLearnerVariantListImpl<>(); diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SBALearnerITCase.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SBALearnerITCase.java new file mode 100644 index 0000000000..f0e0fad644 --- /dev/null +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SBALearnerITCase.java @@ -0,0 +1,41 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.testsupport.it.learner; + +import de.learnlib.api.oracle.EquivalenceOracle; +import de.learnlib.examples.LearningExample.SBALearningExample; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.Word; + +public class SBALearnerITCase extends AbstractLearnerVariantITCase> { + + private final SBALearningExample example; + + SBALearnerITCase(LearnerVariant, I, Boolean> variant, + SBALearningExample example, + EquivalenceOracle, I, Boolean> eqOracle) { + super(variant, example, eqOracle); + this.example = example; + } + + @Override + protected Word checkEquivalence(SBA hypothesis) { + return Automata.findSeparatingWord(this.example.getReferenceAutomaton(), + hypothesis, + this.example.getAlphabet()); + } +} diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPALearnerITCase.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPALearnerITCase.java index fe28b67bc4..1da9104fb8 100644 --- a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPALearnerITCase.java +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPALearnerITCase.java @@ -17,7 +17,7 @@ import de.learnlib.api.oracle.EquivalenceOracle; import de.learnlib.examples.LearningExample.SPALearningExample; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SPA; import net.automatalib.util.automata.Automata; import net.automatalib.words.Word; diff --git a/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPMMLearnerITCase.java b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPMMLearnerITCase.java new file mode 100644 index 0000000000..14b1fdbc16 --- /dev/null +++ b/test-support/learner-it-support/src/main/java/de/learnlib/testsupport/it/learner/SPMMLearnerITCase.java @@ -0,0 +1,41 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.testsupport.it.learner; + +import de.learnlib.api.oracle.EquivalenceOracle; +import de.learnlib.examples.LearningExample.SPMMLearningExample; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.util.automata.Automata; +import net.automatalib.words.Word; + +public class SPMMLearnerITCase extends AbstractLearnerVariantITCase, SPMM> { + + private final SPMMLearningExample example; + + SPMMLearnerITCase(LearnerVariant, I, Word> variant, + SPMMLearningExample example, + EquivalenceOracle, I, Word> eqOracle) { + super(variant, example, eqOracle); + this.example = example; + } + + @Override + protected Word checkEquivalence(SPMM hypothesis) { + return Automata.findSeparatingWord(this.example.getReferenceAutomaton(), + hypothesis, + this.example.getAlphabet()); + } +} diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/DefaultLearningExample.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/DefaultLearningExample.java index aa9c8d427d..2c804c94ca 100644 --- a/test-support/learning-examples/src/main/java/de/learnlib/examples/DefaultLearningExample.java +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/DefaultLearningExample.java @@ -19,13 +19,15 @@ import net.automatalib.automata.concepts.InputAlphabetHolder; import net.automatalib.automata.concepts.SuffixOutput; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.SPMM; import net.automatalib.automata.transducers.MealyMachine; import net.automatalib.automata.transducers.MooreMachine; import net.automatalib.automata.transducers.SubsequentialTransducer; import net.automatalib.automata.vpda.OneSEVPA; import net.automatalib.words.Alphabet; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.VPDAlphabet; import net.automatalib.words.Word; @@ -147,7 +149,45 @@ public SPA getReferenceAutomaton() { } @Override - public SPAAlphabet getAlphabet() { + public ProceduralInputAlphabet getAlphabet() { + return this.referenceAutomaton.getInputAlphabet(); + } + } + + public static class DefaultSBALearningExample implements SBALearningExample { + + private final SBA referenceAutomaton; + + public DefaultSBALearningExample(SBA referenceAutomaton) { + this.referenceAutomaton = referenceAutomaton; + } + + @Override + public SBA getReferenceAutomaton() { + return this.referenceAutomaton; + } + + @Override + public ProceduralInputAlphabet getAlphabet() { + return this.referenceAutomaton.getInputAlphabet(); + } + } + + public static class DefaultSPMMLearningExample implements SPMMLearningExample { + + private final SPMM referenceAutomaton; + + public DefaultSPMMLearningExample(SPMM referenceAutomaton) { + this.referenceAutomaton = referenceAutomaton; + } + + @Override + public SPMM getReferenceAutomaton() { + return this.referenceAutomaton; + } + + @Override + public ProceduralInputAlphabet getAlphabet() { return this.referenceAutomaton.getInputAlphabet(); } } diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExample.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExample.java index 76ebe5df4a..7ce4197052 100644 --- a/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExample.java +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExample.java @@ -17,14 +17,16 @@ import net.automatalib.automata.UniversalAutomaton; import net.automatalib.automata.fsa.DFA; -import net.automatalib.automata.spa.SPA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.SPMM; import net.automatalib.automata.transducers.MealyMachine; import net.automatalib.automata.transducers.MooreMachine; import net.automatalib.automata.transducers.StateLocalInputMealyMachine; import net.automatalib.automata.transducers.SubsequentialTransducer; import net.automatalib.automata.vpda.OneSEVPA; import net.automatalib.words.Alphabet; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.VPDAlphabet; public interface LearningExample { @@ -63,7 +65,19 @@ interface StateLocalInputMealyLearningExample interface SPALearningExample extends LearningExample> { @Override - SPAAlphabet getAlphabet(); + ProceduralInputAlphabet getAlphabet(); + } + + interface SBALearningExample extends LearningExample> { + + @Override + ProceduralInputAlphabet getAlphabet(); + } + + interface SPMMLearningExample extends LearningExample> { + + @Override + ProceduralInputAlphabet getAlphabet(); } interface OneSEVPALearningExample extends LearningExample> { diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExamples.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExamples.java index db72032c7f..699ba61aea 100644 --- a/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExamples.java +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/LearningExamples.java @@ -25,7 +25,9 @@ import de.learnlib.examples.LearningExample.MealyLearningExample; import de.learnlib.examples.LearningExample.MooreLearningExample; import de.learnlib.examples.LearningExample.OneSEVPALearningExample; +import de.learnlib.examples.LearningExample.SBALearningExample; import de.learnlib.examples.LearningExample.SPALearningExample; +import de.learnlib.examples.LearningExample.SPMMLearningExample; import de.learnlib.examples.LearningExample.SSTLearningExample; import de.learnlib.examples.LearningExample.StateLocalInputMealyLearningExample; import de.learnlib.examples.dfa.ExampleAngluin; @@ -40,23 +42,29 @@ import de.learnlib.examples.mealy.ExampleStack; import de.learnlib.examples.mealy.ExampleTinyMealy; import de.learnlib.examples.moore.ExampleRandomMoore; +import de.learnlib.examples.sba.ExampleRandomSBA; import de.learnlib.examples.spa.ExamplePalindrome; import de.learnlib.examples.spa.ExampleRandomSPA; +import de.learnlib.examples.spmm.ExampleRandomSPMM; import de.learnlib.examples.sst.ExampleRandomSST; import de.learnlib.examples.vpda.ExampleRandomOneSEVPA; import net.automatalib.words.Alphabet; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.ProceduralOutputAlphabet; import net.automatalib.words.VPDAlphabet; import net.automatalib.words.Word; import net.automatalib.words.impl.Alphabets; -import net.automatalib.words.impl.DefaultSPAAlphabet; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; +import net.automatalib.words.impl.DefaultProceduralOutputAlphabet; import net.automatalib.words.impl.DefaultVPDAlphabet; public final class LearningExamples { private static final Alphabet RANDOM_ALPHABET = Alphabets.characters('a', 'c'); - private static final SPAAlphabet SPA_ALPHABET = - new DefaultSPAAlphabet<>(Alphabets.characters('A', 'F'), Alphabets.characters('a', 'f'), 'R'); + private static final ProceduralInputAlphabet PROCEDURAL_INPUT_ALPHABET = + new DefaultProceduralInputAlphabet<>(Alphabets.characters('A', 'F'), Alphabets.characters('a', 'f'), 'R'); + private static final ProceduralOutputAlphabet PROCEDURAL_OUTPUT_ALPHABET = + new DefaultProceduralOutputAlphabet<>(Alphabets.characters('u', 'z'), '✗'); private static final VPDAlphabet VPD_ALPHABET = new DefaultVPDAlphabet<>(Alphabets.characters('a', 'f'), Alphabets.characters('1', '3'), Alphabets.characters('7', '9')); @@ -100,9 +108,9 @@ public static List> createDFAExamples() { public static List> createMooreExamples() { return Collections.singletonList(ExampleRandomMoore.createExample(new Random(RANDOM_SEED), - RANDOM_ALPHABET, - RANDOM_SIZE, - RANDOM_MEALY_OUTPUTS)); + RANDOM_ALPHABET, + RANDOM_SIZE, + RANDOM_MEALY_OUTPUTS)); } public static List> createSLIMealyExamples() { @@ -123,7 +131,24 @@ public static List> createDFAExamples() { public static List> createSPAExamples() { return Arrays.asList(ExamplePalindrome.createExample(), - ExampleRandomSPA.createExample(new Random(RANDOM_SEED), SPA_ALPHABET, PROCEDURE_SIZE)); + ExampleRandomSPA.createExample(new Random(RANDOM_SEED), + PROCEDURAL_INPUT_ALPHABET, + PROCEDURE_SIZE)); + } + + public static List> createSBAExamples() { + return Arrays.asList(de.learnlib.examples.sba.ExamplePalindrome.createExample(), + ExampleRandomSBA.createExample(new Random(RANDOM_SEED), + PROCEDURAL_INPUT_ALPHABET, + PROCEDURE_SIZE)); + } + + public static List> createSPMMExamples() { + return Arrays.asList(de.learnlib.examples.spmm.ExamplePalindrome.createExample(), + ExampleRandomSPMM.createExample(new Random(RANDOM_SEED), + PROCEDURAL_INPUT_ALPHABET, + PROCEDURAL_OUTPUT_ALPHABET, + PROCEDURE_SIZE)); } public static List> createOneSEVPAExamples() { diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExamplePalindrome.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExamplePalindrome.java new file mode 100644 index 0000000000..9fac2ac0db --- /dev/null +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExamplePalindrome.java @@ -0,0 +1,106 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.examples.sba; + +import java.util.HashMap; +import java.util.Map; + +import de.learnlib.examples.DefaultLearningExample.DefaultSBALearningExample; +import net.automatalib.automata.fsa.DFA; +import net.automatalib.automata.fsa.impl.FastDFA; +import net.automatalib.automata.fsa.impl.compact.CompactDFA; +import net.automatalib.automata.procedural.SBA; +import net.automatalib.automata.procedural.StackSBA; +import net.automatalib.util.automata.builders.AutomatonBuilders; +import net.automatalib.util.automata.fsa.MutableDFAs; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; + +public class ExamplePalindrome extends DefaultSBALearningExample { + + public ExamplePalindrome() { + super(createSBA()); + } + + public static ExamplePalindrome createExample() { + return new ExamplePalindrome(); + } + + private static SBA createSBA() { + final Alphabet internalAlphabet = Alphabets.characters('a', 'c'); + final Alphabet callAlphabet = Alphabets.characters('S', 'T'); + final ProceduralInputAlphabet alphabet = + new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, 'R'); + + final DFA sProcedure = buildSProcedure(alphabet); + final DFA tProcedure = buildTProcedure(alphabet); + + final Map> subModels = new HashMap<>(); + subModels.put('S', sProcedure); + subModels.put('T', tProcedure); + + return new StackSBA<>(alphabet, 'S', subModels); + } + + private static DFA buildSProcedure(ProceduralInputAlphabet alphabet) { + + final CompactDFA result = new CompactDFA<>(alphabet); + + // @formatter:off + AutomatonBuilders.forDFA(result) + .withInitial("s0") + .from("s0").on('T').to("s5") + .from("s0").on('a').to("s1") + .from("s0").on('b').to("s2") + .from("s0").on('R').to("s6") + .from("s1").on('S').to("s3") + .from("s1").on('R').to("s6") + .from("s2").on('S').to("s4") + .from("s2").on('R').to("s6") + .from("s3").on('a').to("s5") + .from("s4").on('b').to("s5") + .from("s5").on('R').to("s6") + .withAccepting("s0", "s1", "s2", "s3", "s4", "s5", "s6") + .create(); + // @formatter:on + + MutableDFAs.complete(result, alphabet); + return result; + } + + private static DFA buildTProcedure(ProceduralInputAlphabet alphabet) { + + final FastDFA result = new FastDFA<>(alphabet); + + // @formatter:off + AutomatonBuilders.forDFA(result) + .withInitial("t0") + .from("t0").on('S').to("t3") + .from("t0").on('c').to("t1") + .from("t1").on('T').to("t2") + .from("t1").on('R').to("t4") + .from("t2").on('c').to("t3") + .from("t3").on('R').to("t4") + .withAccepting("t0", "t1", "t2", "t3", "t4") + .create(); + // @formatter:on + + MutableDFAs.complete(result, alphabet); + return result; + } +} diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExampleRandomSBA.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExampleRandomSBA.java new file mode 100644 index 0000000000..70134dfe8d --- /dev/null +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/sba/ExampleRandomSBA.java @@ -0,0 +1,37 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.examples.sba; + +import java.util.Random; + +import de.learnlib.examples.DefaultLearningExample.DefaultSBALearningExample; +import net.automatalib.util.automata.random.RandomAutomata; +import net.automatalib.words.ProceduralInputAlphabet; + +public class ExampleRandomSBA extends DefaultSBALearningExample { + + public ExampleRandomSBA(ProceduralInputAlphabet alphabet, int size) { + this(new Random(), alphabet, size); + } + + public ExampleRandomSBA(Random random, ProceduralInputAlphabet alphabet, int size) { + super(RandomAutomata.randomSBA(random, alphabet, size)); + } + + public static ExampleRandomSBA createExample(Random random, ProceduralInputAlphabet alphabet, int size) { + return new ExampleRandomSBA<>(random, alphabet, size); + } +} diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExamplePalindrome.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExamplePalindrome.java index 5f671ae6cc..1cc05b73e2 100644 --- a/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExamplePalindrome.java +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExamplePalindrome.java @@ -22,14 +22,14 @@ import net.automatalib.automata.fsa.DFA; import net.automatalib.automata.fsa.impl.FastDFA; import net.automatalib.automata.fsa.impl.compact.CompactDFA; -import net.automatalib.automata.spa.SPA; -import net.automatalib.automata.spa.StackSPA; +import net.automatalib.automata.procedural.SPA; +import net.automatalib.automata.procedural.StackSPA; import net.automatalib.util.automata.builders.AutomatonBuilders; import net.automatalib.util.automata.fsa.MutableDFAs; import net.automatalib.words.Alphabet; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; import net.automatalib.words.impl.Alphabets; -import net.automatalib.words.impl.DefaultSPAAlphabet; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; public class ExamplePalindrome extends DefaultSPALearningExample { @@ -44,7 +44,7 @@ public static ExamplePalindrome createExample() { private static SPA createSPA() { final Alphabet internalAlphabet = Alphabets.characters('a', 'c'); final Alphabet callAlphabet = Alphabets.characters('S', 'T'); - final SPAAlphabet alphabet = new DefaultSPAAlphabet<>(internalAlphabet, callAlphabet, 'R'); + final ProceduralInputAlphabet alphabet = new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, 'R'); final DFA sProcedure = buildSProcedure(alphabet); final DFA tProcedure = buildTProcedure(alphabet); @@ -56,7 +56,7 @@ private static SPA createSPA() { return new StackSPA<>(alphabet, 'S', subModels); } - private static DFA buildSProcedure(SPAAlphabet alphabet) { + private static DFA buildSProcedure(ProceduralInputAlphabet alphabet) { final CompactDFA result = new CompactDFA<>(alphabet.getProceduralAlphabet()); @@ -78,7 +78,7 @@ private static DFA buildSProcedure(SPAAlphabet alphabet return result; } - private static DFA buildTProcedure(SPAAlphabet alphabet) { + private static DFA buildTProcedure(ProceduralInputAlphabet alphabet) { final FastDFA result = new FastDFA<>(alphabet.getProceduralAlphabet()); diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExampleRandomSPA.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExampleRandomSPA.java index 8bf8cf65e0..9ebe2ca714 100644 --- a/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExampleRandomSPA.java +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/spa/ExampleRandomSPA.java @@ -19,19 +19,19 @@ import de.learnlib.examples.DefaultLearningExample.DefaultSPALearningExample; import net.automatalib.util.automata.random.RandomAutomata; -import net.automatalib.words.SPAAlphabet; +import net.automatalib.words.ProceduralInputAlphabet; public class ExampleRandomSPA extends DefaultSPALearningExample { - public ExampleRandomSPA(SPAAlphabet alphabet, int size) { + public ExampleRandomSPA(ProceduralInputAlphabet alphabet, int size) { this(new Random(), alphabet, size); } - public ExampleRandomSPA(Random random, SPAAlphabet alphabet, int size) { - super(RandomAutomata.randomSPA(random, alphabet, size, true)); + public ExampleRandomSPA(Random random, ProceduralInputAlphabet alphabet, int size) { + super(RandomAutomata.randomSPA(random, alphabet, size)); } - public static ExampleRandomSPA createExample(Random random, SPAAlphabet alphabet, int size) { + public static ExampleRandomSPA createExample(Random random, ProceduralInputAlphabet alphabet, int size) { return new ExampleRandomSPA<>(random, alphabet, size); } } diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExamplePalindrome.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExamplePalindrome.java new file mode 100644 index 0000000000..a8325c83ec --- /dev/null +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExamplePalindrome.java @@ -0,0 +1,107 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.examples.spmm; + +import java.util.HashMap; +import java.util.Map; + +import de.learnlib.examples.DefaultLearningExample.DefaultSPMMLearningExample; +import net.automatalib.automata.procedural.SPMM; +import net.automatalib.automata.procedural.StackSPMM; +import net.automatalib.automata.transducers.MealyMachine; +import net.automatalib.automata.transducers.impl.FastMealy; +import net.automatalib.automata.transducers.impl.compact.CompactMealy; +import net.automatalib.util.automata.builders.AutomatonBuilders; +import net.automatalib.util.automata.transducers.MutableMealyMachines; +import net.automatalib.words.Alphabet; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.impl.Alphabets; +import net.automatalib.words.impl.DefaultProceduralInputAlphabet; + +public class ExamplePalindrome extends DefaultSPMMLearningExample { + + private static final char ERROR_OUTPUT = '-'; + private static final char SUCCESS_OUTPUT = '✓'; + + public ExamplePalindrome() { + super(createSPMM()); + } + + public static ExamplePalindrome createExample() { + return new ExamplePalindrome(); + } + + private static SPMM createSPMM() { + final Alphabet internalAlphabet = Alphabets.characters('a', 'c'); + final Alphabet callAlphabet = Alphabets.characters('S', 'T'); + final ProceduralInputAlphabet alphabet = + new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, 'R'); + + final MealyMachine sProcedure = buildSProcedure(alphabet); + final MealyMachine tProcedure = buildTProcedure(alphabet); + + final Map> subModels = new HashMap<>(); + subModels.put('S', sProcedure); + subModels.put('T', tProcedure); + + return new StackSPMM<>(alphabet, 'S', SUCCESS_OUTPUT, ERROR_OUTPUT, subModels); + } + + private static MealyMachine buildSProcedure(ProceduralInputAlphabet alphabet) { + + final CompactMealy result = new CompactMealy<>(alphabet); + + // @formatter:off + AutomatonBuilders.forMealy(result) + .withInitial("s0") + .from("s0").on('T').withOutput(SUCCESS_OUTPUT).to("s5") + .from("s0").on('a').withOutput('x').to("s1") + .from("s0").on('b').withOutput('y').to("s2") + .from("s0").on('R').withOutput(SUCCESS_OUTPUT).to("s6") + .from("s1").on('S').withOutput(SUCCESS_OUTPUT).to("s3") + .from("s1").on('R').withOutput(SUCCESS_OUTPUT).to("s6") + .from("s2").on('S').withOutput(SUCCESS_OUTPUT).to("s4") + .from("s2").on('R').withOutput(SUCCESS_OUTPUT).to("s6") + .from("s3").on('a').withOutput('x').to("s5") + .from("s4").on('b').withOutput('y').to("s5") + .from("s5").on('R').withOutput(SUCCESS_OUTPUT).to("s6") + .create(); + // @formatter:on + + MutableMealyMachines.complete(result, alphabet, ERROR_OUTPUT, true); + return result; + } + + private static MealyMachine buildTProcedure(ProceduralInputAlphabet alphabet) { + + final FastMealy result = new FastMealy<>(alphabet); + + // @formatter:off + AutomatonBuilders.forMealy(result) + .withInitial("t0") + .from("t0").on('S').withOutput(SUCCESS_OUTPUT).to("t3") + .from("t0").on('c').withOutput('z').to("t1") + .from("t1").on('T').withOutput(SUCCESS_OUTPUT).to("t2") + .from("t1").on('R').withOutput(SUCCESS_OUTPUT).to("t4") + .from("t2").on('c').withOutput('z').to("t3") + .from("t3").on('R').withOutput(SUCCESS_OUTPUT).to("t4") + .create(); + // @formatter:on + + MutableMealyMachines.complete(result, alphabet, ERROR_OUTPUT, true); + return result; + } +} diff --git a/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExampleRandomSPMM.java b/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExampleRandomSPMM.java new file mode 100644 index 0000000000..f70a53ab1b --- /dev/null +++ b/test-support/learning-examples/src/main/java/de/learnlib/examples/spmm/ExampleRandomSPMM.java @@ -0,0 +1,38 @@ +/* Copyright (C) 2013-2023 TU Dortmund + * This file is part of LearnLib, http://www.learnlib.de/. + * + * 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.examples.spmm; + +import java.util.Random; + +import de.learnlib.examples.DefaultLearningExample.DefaultSPMMLearningExample; +import net.automatalib.util.automata.random.RandomAutomata; +import net.automatalib.words.ProceduralInputAlphabet; +import net.automatalib.words.ProceduralOutputAlphabet; + +public class ExampleRandomSPMM extends DefaultSPMMLearningExample { + + public ExampleRandomSPMM(ProceduralInputAlphabet inputAlphabet, ProceduralOutputAlphabet outputAlphabet, int size) { + this(new Random(), inputAlphabet, outputAlphabet, size); + } + + public ExampleRandomSPMM(Random random, ProceduralInputAlphabet inputAlphabet, ProceduralOutputAlphabet outputAlphabet, int size) { + super(RandomAutomata.randomSPMM(random, inputAlphabet, outputAlphabet, size)); + } + + public static ExampleRandomSPMM createExample(Random random, ProceduralInputAlphabet inputAlphabet, ProceduralOutputAlphabet outputAlphabet, int size) { + return new ExampleRandomSPMM<>(random, inputAlphabet, outputAlphabet, size); + } +}