Skip to content

Commit

Permalink
Fix bug where suffix for memorable is not added to prefix (#57)
Browse files Browse the repository at this point in the history 
* add test for bug

* add check for missing parameter in prefix
  • Loading branch information
@FredrikTaquist
FredrikTaquist authored Dec 24, 2023
1 parent 9bef181 commit 08b1183
Show file tree
Hide file tree
Showing 3 changed files with 76 additions and 5 deletions.
15 changes: 12 additions & 3 deletions src/main/java/de/learnlib/ralib/dt/DTLeaf.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<SymbolicSuffix> prefixSuffixes = prefixMapped.getAllSuffixesForMemorable(p);
Set<SymbolicSuffix> 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)) {
Expand All @@ -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);
}
Expand Down
2 changes: 0 additions & 2 deletions src/main/java/de/learnlib/ralib/dt/MappedPrefix.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ public class MappedPrefix implements PrefixContainer {
private final PIV memorable = new PIV();
private final RegisterGenerator regGen = new RegisterGenerator();
private final Map<SymbolicSuffix, TreeQueryResult> tqrs = new LinkedHashMap<SymbolicSuffix, TreeQueryResult>();

public final Set<Parameter> missingParameter = new LinkedHashSet<>();

public MappedPrefix(Word<PSymbolInstance> prefix) {
Expand Down Expand Up @@ -126,7 +125,6 @@ Set<SymbolicSuffix> getAllSuffixesForMemorable(Parameter p) {
if (e.getValue().getPiv().containsKey(p))
suffixes.add(e.getKey());
}
assert !suffixes.isEmpty();
return suffixes;
}
}
64 changes: 64 additions & 0 deletions src/test/java/de/learnlib/ralib/learning/ralambda/TestUnknownMemorable.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<DataType, Theory> 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<DefaultQuery<PSymbolInstance, Boolean>> ceQueue = buildSIPCEs(ces, actions);

while (!ceQueue.isEmpty()) {
ralambda.addCounterexample(ceQueue.pop());
ralambda.learn();
}

Assert.assertTrue(true);
}

private Deque<DefaultQuery<PSymbolInstance, Boolean>> buildSIPCEs(String[] ceStrings, ParameterizedSymbol[] actionSymbols) {
Deque<DefaultQuery<PSymbolInstance, Boolean>> ces = new LinkedList<>();

Expand Down

0 comments on commit 08b1183

Please sign in to comment.