From 08b118391d8a42e501a7794aa8d5041a63bdd815 Mon Sep 17 00:00:00 2001 From: FredrikTaquist <60506950+FredrikTaquist@users.noreply.github.com> Date: Sun, 24 Dec 2023 12:36:24 +0100 Subject: [PATCH] Fix bug where suffix for memorable is not added to prefix (#57) * add test for bug * add check for missing parameter in prefix --- .../java/de/learnlib/ralib/dt/DTLeaf.java | 15 ++++- .../de/learnlib/ralib/dt/MappedPrefix.java | 2 - .../ralambda/TestUnknownMemorable.java | 64 +++++++++++++++++++ 3 files changed, 76 insertions(+), 5 deletions(-) diff --git a/src/main/java/de/learnlib/ralib/dt/DTLeaf.java b/src/main/java/de/learnlib/ralib/dt/DTLeaf.java index 611ffaca..d409a17d 100644 --- a/src/main/java/de/learnlib/ralib/dt/DTLeaf.java +++ b/src/main/java/de/learnlib/ralib/dt/DTLeaf.java @@ -480,13 +480,20 @@ private boolean checkVariableConsistency(MappedPrefix mp, DT dt, Constants const int max = DataWords.paramLength(DataWords.actsOf(prefix)); for (Parameter p : memMP.keySet()) { - if (!memPrefix.containsKey(p) && p.getId() <= max) { - for (SymbolicSuffix suffix : mp.getAllSuffixesForMemorable(p)) { + boolean prefixMissingParam = !memPrefix.containsKey(p) || + prefixMapped.missingParameter.contains(p); + if (prefixMissingParam && p.getId() <= max) { + Set prefixSuffixes = prefixMapped.getAllSuffixesForMemorable(p); + Set suffixes = mp.getAllSuffixesForMemorable(p); + assert !suffixes.isEmpty(); + for (SymbolicSuffix suffix : suffixes) { TreeQueryResult suffixTQR = mp.getTQRs().get(suffix); SymbolicDecisionTree sdt = suffixTQR.getSdt(); SymbolicSuffix newSuffix = suffixBuilder != null && sdt instanceof SDT ? suffixBuilder.extendSuffix(mp.getPrefix(), (SDT)sdt, suffixTQR.getPiv(), suffix) : new SymbolicSuffix(mp.getPrefix(), suffix, consts); + if (prefixSuffixes.contains(newSuffix)) + continue; TreeQueryResult tqr = oracle.treeQuery(prefix, newSuffix); if (tqr.getPiv().keySet().contains(p)) { @@ -495,7 +502,9 @@ private boolean checkVariableConsistency(MappedPrefix mp, DT dt, Constants const return false; } } - mp.missingParameter.add(p); + if (!prefixMapped.missingParameter.contains(p)) { + mp.missingParameter.add(p); + } } else { mp.missingParameter.remove(p); } diff --git a/src/main/java/de/learnlib/ralib/dt/MappedPrefix.java b/src/main/java/de/learnlib/ralib/dt/MappedPrefix.java index 5b8410c0..f0328cce 100644 --- a/src/main/java/de/learnlib/ralib/dt/MappedPrefix.java +++ b/src/main/java/de/learnlib/ralib/dt/MappedPrefix.java @@ -24,7 +24,6 @@ public class MappedPrefix implements PrefixContainer { private final PIV memorable = new PIV(); private final RegisterGenerator regGen = new RegisterGenerator(); private final Map tqrs = new LinkedHashMap(); - public final Set missingParameter = new LinkedHashSet<>(); public MappedPrefix(Word prefix) { @@ -126,7 +125,6 @@ Set getAllSuffixesForMemorable(Parameter p) { if (e.getValue().getPiv().containsKey(p)) suffixes.add(e.getKey()); } - assert !suffixes.isEmpty(); return suffixes; } } diff --git a/src/test/java/de/learnlib/ralib/learning/ralambda/TestUnknownMemorable.java b/src/test/java/de/learnlib/ralib/learning/ralambda/TestUnknownMemorable.java index 96dd7e20..4aad984a 100644 --- a/src/test/java/de/learnlib/ralib/learning/ralambda/TestUnknownMemorable.java +++ b/src/test/java/de/learnlib/ralib/learning/ralambda/TestUnknownMemorable.java @@ -297,6 +297,70 @@ public void testSkippingMemorable() { Assert.assertTrue(true); } + @Test + public void testSkippingMemorable2() { + + RegisterAutomatonImporter loader = TestUtil.getLoader( + "/de/learnlib/ralib/automata/xml/sip.xml"); + + RegisterAutomaton model = loader.getRegisterAutomaton(); + + ParameterizedSymbol[] inputs = loader.getInputs().toArray( + new ParameterizedSymbol[]{}); + + ParameterizedSymbol[] actions = loader.getActions().toArray( + new ParameterizedSymbol[]{}); + + final Constants consts = loader.getConstants(); + + + final Map teachers = new LinkedHashMap<>(); + loader.getDataTypes().stream().forEach((t) -> { + IntegerEqualityTheory theory = new IntegerEqualityTheory(t); + theory.setUseSuffixOpt(true); + teachers.put(t, theory); + }); + + DataWordSUL sul = new SimulatorSUL(model, teachers, consts); + IOOracle ioOracle = new SULOracle(sul, ERROR); + IOCache ioCache = new IOCache(ioOracle); + IOFilter ioFilter = new IOFilter(ioCache, inputs); + + ConstraintSolver solver = new SimpleConstraintSolver(); + + MultiTheoryTreeOracle mto = new MultiTheoryTreeOracle( + ioFilter, teachers, consts, solver); + MultiTheorySDTLogicOracle mlo = + new MultiTheorySDTLogicOracle(consts, solver); + + TreeOracleFactory hypFactory = (RegisterAutomaton hyp) -> + new MultiTheoryTreeOracle(new SimulatorOracle(hyp), teachers, consts, solver); + + RaLambda ralambda = new RaLambda(mto, hypFactory, mlo, consts, true, actions); + ralambda.setSolver(solver); + ralambda.learn(); + + String[] ces = {"IINVITE[0[int]] O100[0[int]] / true", + "IACK[0[int]] Otimeout[] IINVITE[0[int]] Otimeout[] / true", + "IINVITE[0[int]] O100[0[int]] Inil[] O183[0[int]] / true", + "IINVITE[0[int]] O100[0[int]] IPRACK[0[int]] O200[0[int]] / true", + "IINVITE[0[int]] O100[0[int]] IPRACK[1[int]] O481[1[int]] / true", + "Inil[] Otimeout[] IINVITE[0[int]] O100[0[int]] / true", + "IINVITE[0[int]] O100[0[int]] IACK[0[int]] Otimeout[] IPRACK[1[int]] O481[1[int]] / true", + "IINVITE[0[int]] O100[0[int]] IPRACK[0[int]] O200[0[int]] Inil[] O180[0[int]] / true", + "IINVITE[0[int]] O100[0[int]] IACK[0[int]] Otimeout[] IPRACK[0[int]] O200[0[int]] / true", + "IINVITE[0[int]] O100[0[int]] IPRACK[0[int]] O200[0[int]] IPRACK[0[int]] Otimeout[] IINVITE[0[int]] O100[0[int]] Inil[] O486[0[int]] / true"}; + + Deque> ceQueue = buildSIPCEs(ces, actions); + + while (!ceQueue.isEmpty()) { + ralambda.addCounterexample(ceQueue.pop()); + ralambda.learn(); + } + + Assert.assertTrue(true); + } + private Deque> buildSIPCEs(String[] ceStrings, ParameterizedSymbol[] actionSymbols) { Deque> ces = new LinkedList<>();