Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/main/java/de/learnlib/ralib/ceanalysis/Essentializer.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright (C) 2014-2015 The LearnLib Contributors
* Copyright (C) 2014-2026 The LearnLib Contributors
* This file is part of LearnLib, http://www.learnlib.de/.
*
* Licensed under the Apache License, Version 2.0 (the "License");
Expand Down Expand Up @@ -41,7 +41,7 @@ public Essentializer(EqualityTheory theory, DataWordOracle sulOracle, DataWordOr
}

public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
final boolean refOutSul = sulOracle.answerQuery(in);
final boolean refOutSUL = sulOracle.answerQuery(in);
final boolean refOutHyp = hypOracle.answerQuery(in);
final Word<ParameterizedSymbol> acts = DataWords.actsOf(in);
DataValue[] vals = DataWords.valsOf(in);
Expand All @@ -57,7 +57,7 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
DataValue fresh = theory.getFreshValue(Arrays.asList(vals));
vals[index] = fresh;
Word<PSymbolInstance> instantiated = DataWords.instantiate(acts, vals);
if(refOutSul == sulOracle.answerQuery(instantiated) &&
if(refOutSUL == sulOracle.answerQuery(instantiated) &&
refOutHyp == hypOracle.answerQuery(instantiated)) {
continue;
}
Expand All @@ -72,7 +72,7 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
vals[sublist[i]] = (c & (1<<i)) == 0 ? fresh : v;
}
instantiated = DataWords.instantiate(acts, vals);
if (refOutSul == sulOracle.answerQuery(instantiated) &&
if (refOutSUL == sulOracle.answerQuery(instantiated) &&
refOutHyp == hypOracle.answerQuery(instantiated)) {
continue IDX;
}
Expand Down
16 changes: 8 additions & 8 deletions src/main/java/de/learnlib/ralib/ceanalysis/PrefixFinder.java
Original file line number Diff line number Diff line change
Expand Up @@ -110,11 +110,11 @@ public Result analyzeCounterExample(Word<PSymbolInstance> ce) {
Set<Mapping<DataValue, DataValue>> uToRunExtendedRenamings = extendedValuationRenamings(sdt, uVals, run, i);

Branching branching = sulOracle.getInitialBranching(u, action, sdt);
for (Expression<Boolean> gSul : branching.guardSet()) {
for (Expression<Boolean> gSUL : branching.guardSet()) {
for (Mapping<DataValue, DataValue> renaming : uToRunExtendedRenamings) {
renaming.putAll(uToRunRenaming);
if (isGuardSatisfied(gSul, renaming, symbol)) {
Optional<Result> res = checkTransition(locNext, u, action, vNext, gHyp, gSul);
if (isGuardSatisfied(gSUL, renaming, symbol)) {
Optional<Result> res = checkTransition(locNext, u, action, vNext, gHyp, gSUL);
if (res.isEmpty()) {
res = checkLocation(locNext, u, action, vNext);
}
Expand Down Expand Up @@ -278,9 +278,9 @@ private Optional<Result> checkTransition(RALocation loc,
reprDataVals[i] = reprDataVal.get();
}
PSymbolInstance psi = new PSymbolInstance(action, reprDataVals);
Word<PSymbolInstance> uExtSul = u.append(psi);
Word<PSymbolInstance> uExtSUL = u.append(psi);

// check whether leaf of loc contains an extension of u that is equivalent to uExtSul after v
// check whether leaf of loc contains an extension of u that is equivalent to uExtSUL after v
CTLeaf leaf = hyp.getLeaf(loc);
Iterator<Word<PSymbolInstance>> extensions = ct.getExtensions(u, action)
.stream()
Expand All @@ -289,15 +289,15 @@ private Optional<Result> checkTransition(RALocation loc,
while (extensions.hasNext()) {
Word<PSymbolInstance> uExtHyp = extensions.next();
SDT uExtHypSDT = sulOracle.treeQuery(uExtHyp, v).toRegisterSDT(uExtHyp, consts);
SDT uExtSulSDT = sulOracle.treeQuery(uExtSul, v).toRegisterSDT(uExtSul, consts);
SDT uExtSULSDT = sulOracle.treeQuery(uExtSUL, v).toRegisterSDT(uExtSUL, consts);

if (SDT.equivalentUnderId(uExtHypSDT, uExtSulSDT)) {
if (SDT.equivalentUnderId(uExtHypSDT, uExtSULSDT)) {
return Optional.empty(); // there is an equivalent extension, so no discrepancy
}
}

// no equivalent extension exists
Result res = new Result(uExtSul, ResultType.TRANSITION);
Result res = new Result(uExtSUL, ResultType.TRANSITION);
return Optional.of(res);
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ private IndexResult computeIndex(Word<PSymbolInstance> ce, int idx) {
SymbolicSuffix symSuffix = new SymbolicSuffix(prefix, suffix, restrictionBuilder);

SDT resHyp = hypOracle.treeQuery(location, symSuffix);
SDT resSul = sulOracle.treeQuery(location, symSuffix);
SDT resSUL = sulOracle.treeQuery(location, symSuffix);

LOGGER.trace("------------------------------------------------------");
LOGGER.trace("Computing index: {}", idx);
Expand All @@ -108,25 +108,25 @@ private IndexResult computeIndex(Word<PSymbolInstance> ce, int idx) {
LOGGER.trace("Location: {}", location);
LOGGER.trace("Transition: {}", transition);
LOGGER.trace("SDT HYP: {}", resHyp);
LOGGER.trace("SDT SYS: {}", resSul);
LOGGER.trace("SDT SYS: {}", resSUL);
LOGGER.trace("------------------------------------------------------");

LocationComponent c = components.get(location);
ParameterizedSymbol act = transition.lastSymbol().getBaseSymbol();
//System.out.println(c.getBranching(act).getBranches());
Expression<Boolean> g = c.getBranching(act).getBranches().get(transition);

boolean hasCE = sdtOracle.hasCounterexample(location, resHyp, resSul, g, transition);
boolean hasCE = sdtOracle.hasCounterexample(location, resHyp, resSUL, g, transition);

if (!hasCE) {
return IndexResult.NO_CE;
}

Set<DataValue> pSul = resSul.getDataValues();
Set<DataValue> pSUL = resSUL.getDataValues();
Set<DataValue> pHyp = c.getPrimePrefix().getAssignment().keySet();

boolean sulHasMoreRegs = !pHyp.containsAll(pSul);
boolean hypRefinesTransition = hypRefinesTransitions(location, act, resSul);
boolean sulHasMoreRegs = !pHyp.containsAll(pSUL);
boolean hypRefinesTransition = hypRefinesTransitions(location, act, resSUL);

// System.out.println("sulHasMoreRegs: " + sulHasMoreRegs);
// System.out.println("hypRefinesTransition: " + hypRefinesTransition);
Expand All @@ -138,7 +138,7 @@ private IndexResult computeIndex(Word<PSymbolInstance> ce, int idx) {
private boolean hypRefinesTransitions(Word<PSymbolInstance> prefix,
ParameterizedSymbol action, SDT sdtSUL) {

Branching branchSul = sulOracle.getInitialBranching(prefix, action, sdtSUL);
Branching branchSUL = sulOracle.getInitialBranching(prefix, action, sdtSUL);
LocationComponent c = components.get(prefix);
Branching branchHyp = c.getBranching(action);

Expand All @@ -147,14 +147,14 @@ private boolean hypRefinesTransitions(Word<PSymbolInstance> prefix,
//System.out.println(e.getKey() + " -> " + e.getValue());
}
//System.out.println("Branching Sys:");
for (Map.Entry<Word<PSymbolInstance>, Expression<Boolean>> e : branchSul.getBranches().entrySet()) {
for (Map.Entry<Word<PSymbolInstance>, Expression<Boolean>> e : branchSUL.getBranches().entrySet()) {
//System.out.println(e.getKey() + " -> " + e.getValue());
}

for (Expression<Boolean> guardHyp : branchHyp.getBranches().values()) {
boolean refines = false;
for (Expression<Boolean> guardSul : branchSul.getBranches().values()) {
if (sdtOracle.doesRefine(guardHyp, guardSul, new Mapping<>())) {
for (Expression<Boolean> guardSUL : branchSUL.getBranches().values()) {
if (sdtOracle.doesRefine(guardHyp, guardSUL, new Mapping<>())) {
refines = true;
break;
}
Expand Down
36 changes: 18 additions & 18 deletions src/main/java/de/learnlib/ralib/learning/QueryStatistics.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ public class QueryStatistics {
private static final int MEASUREMENTS = 5;

private final QueryCounter queryCounter;
private final DataWordSUL learningSul;
private final DataWordSUL testingSul;
private final DataWordSUL learningSUL;
private final DataWordSUL testingSUL;
private final Measurements[] phaseMeasurements = new Measurements[MEASUREMENTS];
private final Measurements measurements;
private int phase = OTHER;
Expand All @@ -32,24 +32,24 @@ public class QueryStatistics {

public QueryStatistics(Measurements measurements, QueryCounter queryCounter) {
this.queryCounter = queryCounter;
learningSul = null;
testingSul = null;
learningSUL = null;
testingSUL = null;
this.measurements = measurements;
initMeasurements();
}

public QueryStatistics(Measurements measurements, DataWordSUL sul) {
this.queryCounter = null;
learningSul = sul;
testingSul = null;
learningSUL = sul;
testingSUL = null;
this.measurements = measurements;
initMeasurements();
}

public QueryStatistics(Measurements measurements, DataWordSUL learningSul, DataWordSUL testingSul) {
public QueryStatistics(Measurements measurements, DataWordSUL learningSUL, DataWordSUL testingSUL) {
queryCounter = null;
this.learningSul = learningSul;
this.testingSul = testingSul;
this.learningSUL = learningSUL;
this.testingSUL = testingSUL;
this.measurements = measurements;
initMeasurements();
}
Expand All @@ -72,14 +72,14 @@ public void setPhase(int phase) {

public void updateMeasurements() {
phaseMeasurements[phase].treeQueries = phaseMeasurements[phase].treeQueries + measurements.treeQueries;
if (phase == TESTING && testingSul != null) {
if (phase == TESTING && testingSUL != null) {
updateTests();
}
else if (learningSul != null) {
phaseMeasurements[phase].inputs = phaseMeasurements[phase].inputs + learningSul.getInputs() - inputCountLastUpdate;
phaseMeasurements[phase].resets = phaseMeasurements[phase].resets + learningSul.getResets() - queryCountLastUpdate;
inputCountLastUpdate = learningSul.getInputs();
queryCountLastUpdate = learningSul.getResets();
else if (learningSUL != null) {
phaseMeasurements[phase].inputs = phaseMeasurements[phase].inputs + learningSUL.getInputs() - inputCountLastUpdate;
phaseMeasurements[phase].resets = phaseMeasurements[phase].resets + learningSUL.getResets() - queryCountLastUpdate;
inputCountLastUpdate = learningSUL.getInputs();
queryCountLastUpdate = learningSUL.getResets();
}
else if (queryCounter != null) {
phaseMeasurements[phase].resets = phaseMeasurements[phase].resets + queryCounter.getQueryCount() - queryCountLastUpdate;
Expand Down Expand Up @@ -115,9 +115,9 @@ public Set<Word<PSymbolInstance>> getCEs() {
}

public void updateTests() {
if (testingSul != null) {
phaseMeasurements[phase].inputs = testingSul.getInputs();
phaseMeasurements[phase].resets = testingSul.getResets();
if (testingSUL != null) {
phaseMeasurements[phase].inputs = testingSUL.getInputs();
phaseMeasurements[phase].resets = testingSUL.getResets();
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@

public class SLLambda implements RaLearningAlgorithm {

private final ClassificationTree ct;
private final ClassificationTree ct;

private final Constants consts;
private final Constants consts;

private final Deque<DefaultQuery<PSymbolInstance, Boolean>> counterexamples;

Expand Down Expand Up @@ -121,8 +121,8 @@ private boolean analyzeCounterExample() {
DefaultQuery<PSymbolInstance, Boolean> ce = counterexamples.peek();
Word<PSymbolInstance> ceWord = ce.getInput();
boolean accHyp = hyp.accepts(ceWord);
boolean accSul = ce.getOutput();
if (accHyp == accSul) {
boolean accSUL = ce.getOutput();
if (accHyp == accSUL) {
// not a ce, dequeue it
counterexamples.poll();
return true;
Expand Down
16 changes: 8 additions & 8 deletions src/main/java/de/learnlib/ralib/tools/ClassAnalyzer.java
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ public class ClassAnalyzer extends AbstractToolWithRandomWalk {

private DataWordSUL sulTest;

private DataWordSUL trackingSulTest;
private DataWordSUL trackingSULTest;

private IORandomWalk randomWalk = null;

Expand Down Expand Up @@ -210,7 +210,7 @@ public void setup(Configuration config) throws ConfigurationException {
IOFilter ioOracle = new IOFilter(ioCache, inputSymbols);

sulTest = new ClasssAnalyzerDataWordSUL(target, methods, md);
trackingSulTest = sulTest;
trackingSULTest = sulTest;
if (this.timeoutMillis > 0L) {
this.sulTest = new TimeOutSUL(this.sulTest, this.timeoutMillis);
}
Expand All @@ -219,7 +219,7 @@ public void setup(Configuration config) throws ConfigurationException {
if (OPTION_CACHE_TESTS.parse(config)) {
SULOracle testBack = new SULOracle(sulTest, SpecialSymbols.ERROR);
IOCache testCache = new IOCache(testBack, ioCache);
this.sulTest = new CachingSUL(trackingSulTest, testCache);
this.sulTest = new CachingSUL(trackingSULTest, testCache);
}


Expand Down Expand Up @@ -340,8 +340,8 @@ public void run() throws RaLibToolException {
break;
}

resets = trackingSulTest.getResets();
inputs = trackingSulTest.getInputs();
resets = trackingSULTest.getResets();
inputs = trackingSULTest.getInputs();

SimpleProfiler.start(__LEARN__);
ceLengths.add(ce.getInput().length());
Expand All @@ -360,9 +360,9 @@ public void run() throws RaLibToolException {
Word<PSymbolInstance> sysTrace = back.trace(ce.getInput());
System.out.println("### SYS TRACE: " + sysTrace);

SimulatorSUL hypSul = new SimulatorSUL(hyp, teachers, consts);
IOOracle iosul = new SULOracle(hypSul, SpecialSymbols.ERROR);
Word<PSymbolInstance> hypTrace = iosul.trace(ce.getInput());
SimulatorSUL hypSUL = new SimulatorSUL(hyp, teachers, consts);
IOOracle ioSUL = new SULOracle(hypSUL, SpecialSymbols.ERROR);
Word<PSymbolInstance> hypTrace = ioSUL.trace(ce.getInput());
System.out.println("### HYP TRACE: " + hypTrace);

assert !hypTrace.equals(sysTrace);
Expand Down
8 changes: 4 additions & 4 deletions src/main/java/de/learnlib/ralib/tools/IOSimulator.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*
* Copyright (C) 2014-2025 The LearnLib Contributors
* Copyright (C) 2014-2026 The LearnLib Contributors
* This file is part of LearnLib, http://www.learnlib.de/.
*
* Licensed under the Apache License, Version 2.0 (the "License");
Expand Down Expand Up @@ -183,12 +183,12 @@ public void setup(Configuration config) throws ConfigurationException {
this.sulTest = new TimeOutSUL(this.sulTest, this.timeoutMillis);
}

DataWordSUL trackingSulTest = this.sulTest;
DataWordSUL trackingSULTest = this.sulTest;

if (OPTION_CACHE_TESTS.parse(config)) {
SULOracle testBack = new SULOracle(sulTest, ERROR);
IOCache testCache = new IOCache(testBack, ioCache);
this.sulTest = new CachingSUL(trackingSulTest, testCache);
this.sulTest = new CachingSUL(trackingSULTest, testCache);
}

if (useFresh) {
Expand Down Expand Up @@ -226,7 +226,7 @@ public TreeOracle createTreeOracle(RegisterAutomaton hyp) {
default:
throw new ConfigurationException("Unknown Learning algorithm: " + this.learner);
}
QueryStatistics queryStats = new QueryStatistics(measurements, sulLearn, trackingSulTest);
QueryStatistics queryStats = new QueryStatistics(measurements, sulLearn, trackingSULTest);
this.rastar.setStatisticCounter(queryStats);

this.eqTest = new IOEquivalenceTest(model, teachers, consts, true, actions);
Expand Down
28 changes: 14 additions & 14 deletions src/test/java/de/learnlib/ralib/sul/CachingSULTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,11 @@ public void stepTest() {
PriorityQueueSUL sul = new PriorityQueueSUL();
IOOracle ioOracle = new SULOracle(sul, ERROR);
IOCache ioCache = new IOCache(ioOracle);
CachingSUL cachingSul = new CachingSUL(sul, ioCache);
cachingSul.pre();
PSymbolInstance ok = cachingSul.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
PSymbolInstance out = cachingSul.step(new PSymbolInstance(POLL));
cachingSul.post();
CachingSUL cachingSUL = new CachingSUL(sul, ioCache);
cachingSUL.pre();
PSymbolInstance ok = cachingSUL.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
PSymbolInstance out = cachingSUL.step(new PSymbolInstance(POLL));
cachingSUL.post();
Assert.assertEquals(ok.getBaseSymbol(), OK);
Assert.assertEquals(out.getBaseSymbol(), OUTPUT);
Assert.assertEquals(sul.getInputs(), 2);
Expand All @@ -42,20 +42,20 @@ public void cachingTest() {
PriorityQueueSUL sul = new PriorityQueueSUL();
IOOracle ioOracle = new SULOracle(sul, ERROR);
IOCache ioCache = new IOCache(ioOracle);
CachingSUL cachingSul = new CachingSUL(sul, ioCache);
CachingSUL cachingSUL = new CachingSUL(sul, ioCache);

cachingSul.pre();
cachingSul.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
cachingSul.step(new PSymbolInstance(POLL));
cachingSul.post();
cachingSUL.pre();
cachingSUL.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
cachingSUL.step(new PSymbolInstance(POLL));
cachingSUL.post();

Assert.assertEquals(sul.getInputs(), 2);
Assert.assertEquals(sul.getResets(), 1);

cachingSul.pre();
cachingSul.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
cachingSul.step(new PSymbolInstance(POLL));
cachingSul.post();
cachingSUL.pre();
cachingSUL.step(new PSymbolInstance(OFFER, new DataValue(DOUBLE_TYPE, new BigDecimal(1))));
cachingSUL.step(new PSymbolInstance(POLL));
cachingSUL.post();

Assert.assertEquals(sul.getInputs(), 2);
Assert.assertEquals(sul.getResets(), 1);
Expand Down