Skip to content

Commit 1829788

Browse files
FredrikTaquistFredrikTaquist
authored
Fundamental Refactoring of SL Lambda Learning Algorithm (#116)
Adds a new, more modular, data structure for classification trees with closedness and consistency checks moved to classification tree, changes the SL Lambda learning algorithm to adhere more closely to the theory, and fixes several bugs.
1 parent 996079f commit 1829788

86 files changed

Lines changed: 4885 additions & 3951 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎pom.xml‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -357,11 +357,6 @@
357357
<groupId>de.learnlib</groupId>
358358
<artifactId>learnlib-util</artifactId>
359359
</dependency>
360-
<dependency>
361-
<groupId>org.apache.commons</groupId>
362-
<artifactId>commons-lang3</artifactId>
363-
<version>${commons-lang.version}</version>
364-
</dependency>
365360
<dependency>
366361
<groupId>tools.aqua</groupId>
367362
<artifactId>jconstraints-core</artifactId>

‎src/main/java/de/learnlib/ralib/automata/Assignment.java‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
package de.learnlib.ralib.automata;
1818

1919
import java.util.List;
20+
import java.util.Map;
2021
import java.util.Map.Entry;
2122

2223
import de.learnlib.ralib.data.Constants;
@@ -42,6 +43,31 @@ public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment)
4243
this.assignment = assignment;
4344
}
4445

46+
public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
47+
RegisterValuation val = new RegisterValuation();
48+
for (Map.Entry<Register, ? extends SymbolicDataValue> e : assignment.entrySet()) {
49+
Register x = e.getKey();
50+
SymbolicDataValue sdv = e.getValue();
51+
DataValue d = sdv.isParameter() ? parameters.get((Parameter) sdv) :
52+
sdv.isRegister() ? registers.get((Register) sdv) :
53+
sdv.isConstant() ? consts.get((Constant) sdv) :
54+
null;
55+
if (d == null) {
56+
throw new IllegalStateException("Illegal assignment: " + x + " := " + sdv);
57+
}
58+
val.put(x, d);
59+
}
60+
return val;
61+
}
62+
63+
/*
64+
* @deprecated method is unsafe, use {@link #valuation()} instead
65+
* Method is unsafe because it keeps registers that are not given a new assignment, which can cause
66+
* a discrepancy in the number of registers a location has, depending on the path to the location.
67+
* Method is deprecated rather than removed because the functionality is used by XML automata models.
68+
* Removal of method requires refactoring of XML models.
69+
*/
70+
@Deprecated
4571
public RegisterValuation compute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
4672
RegisterValuation val = new RegisterValuation();
4773
List<String> rNames = assignment.keySet().stream().map(k -> k.getName()).toList();
@@ -56,6 +82,12 @@ public RegisterValuation compute(RegisterValuation registers, ParameterValuation
5682
val.put(e.getKey(), registers.get((Register) valp));
5783
}
5884
else if (valp.isParameter()) {
85+
DataValue dv = parameters.get((Parameter) valp);
86+
for (Map.Entry<Parameter, DataValue> ep : parameters.entrySet()) {
87+
if (ep.getKey().equals(valp)) {
88+
dv = ep.getValue();
89+
}
90+
}
5991
val.put(e.getKey(), parameters.get((Parameter) valp));
6092
}
6193
//TODO: check if we want to copy constant values into vars

‎src/main/java/de/learnlib/ralib/automata/MutableRegisterAutomaton.java‎

Lines changed: 39 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@
2828
import de.learnlib.ralib.words.PSymbolInstance;
2929
import de.learnlib.ralib.words.ParameterizedSymbol;
3030
import net.automatalib.automaton.MutableDeterministic;
31-
import net.automatalib.common.util.Pair;
3231
import net.automatalib.word.Word;
3332

3433
/**
@@ -119,39 +118,6 @@ protected List<Transition> getTransitions(Word<PSymbolInstance> dw) {
119118
return tseq;
120119
}
121120

122-
protected List<Pair<Transition,RegisterValuation>> getTransitionsAndValuations(Word<PSymbolInstance> dw) {
123-
RegisterValuation vars = RegisterValuation.copyOf(getInitialRegisters());
124-
RALocation current = initial;
125-
List<Pair<Transition,RegisterValuation>> tvseq = new ArrayList<>();
126-
for (PSymbolInstance psi : dw) {
127-
128-
ParameterValuation pars = ParameterValuation.fromPSymbolInstance(psi);
129-
130-
Collection<Transition> candidates =
131-
current.getOut(psi.getBaseSymbol());
132-
133-
if (candidates == null) {
134-
return null;
135-
}
136-
137-
boolean found = false;
138-
for (Transition t : candidates) {
139-
if (t.isEnabled(vars, pars, constants)) {
140-
vars = t.execute(vars, pars, constants);
141-
current = t.getDestination();
142-
tvseq.add(Pair.of(t, RegisterValuation.copyOf(vars)));
143-
found = true;
144-
break;
145-
}
146-
}
147-
148-
if (!found) {
149-
return null;
150-
}
151-
}
152-
return tvseq;
153-
}
154-
155121
@Override
156122
public RALocation getLocation(Word<PSymbolInstance> dw) {
157123
List<Transition> tseq = getTransitions(dw);
@@ -300,4 +266,43 @@ public Transition copyTransition(Transition t, RALocation s) {
300266
throw new UnsupportedOperationException("Not supported yet.");
301267
}
302268

269+
public RARun getRun(Word<PSymbolInstance> word) {
270+
int n = word.length();
271+
RALocation[] locs = new RALocation[n+1];
272+
RegisterValuation[] vals = new RegisterValuation[n+1];
273+
PSymbolInstance[] symbols = new PSymbolInstance[n];
274+
Transition[] transitions = new Transition[n];
275+
276+
locs[0] = getInitialState();
277+
vals[0] = new RegisterValuation();
278+
279+
for (int i = 0; i < n; i++) {
280+
symbols[i] = word.getSymbol(i);
281+
ParameterValuation pars = ParameterValuation.fromPSymbolInstance(symbols[i]);
282+
283+
Collection<Transition> candidates = locs[i].getOut(symbols[i].getBaseSymbol());
284+
if (candidates == null) {
285+
return null;
286+
}
287+
288+
boolean found = false;
289+
290+
for (Transition t : candidates) {
291+
if (t.isEnabled(vals[i], pars, constants)) {
292+
transitions[i] = t;
293+
vals[i+1] = t.execute(vals[i], pars, constants);
294+
locs[i+1] = t.getDestination();
295+
found = true;
296+
break;
297+
}
298+
}
299+
300+
if (!found) {
301+
return null;
302+
}
303+
}
304+
305+
return new RARun(locs, vals, symbols, transitions);
306+
}
307+
303308
}

‎src/main/java/de/learnlib/ralib/automata/RARun.java‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
package de.learnlib.ralib.automata;
2+
3+
4+
import java.util.ArrayList;
5+
import java.util.Collections;
6+
import java.util.LinkedHashSet;
7+
import java.util.List;
8+
import java.util.Map;
9+
import java.util.Set;
10+
11+
import de.learnlib.ralib.automata.output.OutputMapping;
12+
import de.learnlib.ralib.automata.output.OutputTransition;
13+
import de.learnlib.ralib.data.Constants;
14+
import de.learnlib.ralib.data.DataValue;
15+
import de.learnlib.ralib.data.Mapping;
16+
import de.learnlib.ralib.data.RegisterValuation;
17+
import de.learnlib.ralib.data.SymbolicDataValue;
18+
import de.learnlib.ralib.data.SymbolicDataValue.Parameter;
19+
import de.learnlib.ralib.smt.VarsValuationVisitor;
20+
import de.learnlib.ralib.words.PSymbolInstance;
21+
import gov.nasa.jpf.constraints.api.Expression;
22+
import gov.nasa.jpf.constraints.expressions.NumericBooleanExpression;
23+
import gov.nasa.jpf.constraints.expressions.NumericComparator;
24+
import gov.nasa.jpf.constraints.util.ExpressionUtil;
25+
26+
/**
27+
* Data structure containing the locations, register valuations, symbol instances
28+
* and transitions at each step of a run of a hypothesis over a data word.
29+
*
30+
* @author fredrik
31+
*/
32+
public class RARun {
33+
34+
private final RALocation[] locations;
35+
private final RegisterValuation[] valuations;
36+
private final PSymbolInstance[] symbols;
37+
private final Transition[] transitions;
38+
39+
public RARun(RALocation[] locations, RegisterValuation[] valuations, PSymbolInstance[] symbols, Transition[] transitions) {
40+
this.locations = locations;
41+
this.valuations = valuations;
42+
this.symbols = symbols;
43+
this.transitions = transitions;
44+
}
45+
46+
public RALocation getLocation(int i) {
47+
return locations[i];
48+
}
49+
50+
public RegisterValuation getValuation(int i) {
51+
return valuations[i];
52+
}
53+
54+
public PSymbolInstance getTransitionSymbol(int i) {
55+
return symbols[i-1];
56+
}
57+
58+
public Transition getRATransition(int i) {
59+
return transitions[i-1];
60+
}
61+
62+
/**
63+
* Get the guard of the {@code Transition} at index {@code i}. If the {@code Transition}
64+
* is an {@code OutputTransition}, the guard is computed from the transition's
65+
* {@code OutputMapping}.
66+
*
67+
* @param i
68+
* @return
69+
*/
70+
public Expression<Boolean> getGuard(int i) {
71+
Transition transition = getRATransition(i);
72+
if (transition == null) {
73+
return null;
74+
}
75+
return transition instanceof OutputTransition ?
76+
outputGuard((OutputTransition) transition) :
77+
transition.getGuard();
78+
}
79+
80+
/**
81+
* Get the guard of the {@code Transition} at index {@code i}. If the {@code Transition}
82+
* is an {@code OutputTransition}, the guard is computed from the transition's
83+
* {@code OutputMapping}. Registers of the guard will be evaluated according to the
84+
* data values from the register valuation at index {@code i}, and constants will be
85+
* evaluated according to {@code consts}.
86+
*
87+
* @param i
88+
* @return
89+
*/
90+
public Expression<Boolean> getGuard(int i, Constants consts) {
91+
Expression<Boolean> guard = getGuard(i);
92+
VarsValuationVisitor vvv = new VarsValuationVisitor();
93+
Mapping<SymbolicDataValue, DataValue> vals = new Mapping<>();
94+
vals.putAll(getValuation(i));
95+
vals.putAll(consts);
96+
return vvv.apply(guard, vals);
97+
}
98+
99+
private Expression<Boolean> outputGuard(OutputTransition t) {
100+
OutputMapping out = t.getOutput();
101+
102+
Set<Parameter> params = new LinkedHashSet<>();
103+
params.addAll(out.getFreshParameters());
104+
params.addAll(out.getOutput().keySet());
105+
Set<SymbolicDataValue> regs = new LinkedHashSet<>();
106+
regs.addAll(out.getOutput().values());
107+
108+
Expression[] expressions = new Expression[params.size()];
109+
int index = 0;
110+
111+
// fresh parameters
112+
List<Parameter> prior = new ArrayList<>();
113+
List<Parameter> fresh = new ArrayList<>(out.getFreshParameters());
114+
Collections.sort(fresh, (a,b) -> Integer.compare(a.getId(), b.getId()));
115+
for (Parameter p : fresh) {
116+
Expression[] diseq = new Expression[prior.size() + regs.size()];
117+
int i = 0;
118+
for (Parameter prev : prior) {
119+
diseq[i++] = new NumericBooleanExpression(p, NumericComparator.NE, prev);
120+
}
121+
for (SymbolicDataValue s : regs) {
122+
diseq[i++] = new NumericBooleanExpression(p, NumericComparator.NE, s);
123+
}
124+
expressions[index++] = ExpressionUtil.and(diseq);
125+
prior.add(p);
126+
}
127+
128+
// mapped parameters
129+
for (Map.Entry<Parameter, SymbolicDataValue> e : out.getOutput().entrySet()) {
130+
Parameter p = e.getKey();
131+
SymbolicDataValue s = e.getValue();
132+
expressions[index++] = new NumericBooleanExpression(p, NumericComparator.EQ, s);
133+
}
134+
135+
return ExpressionUtil.and(expressions);
136+
}
137+
138+
@Override
139+
public String toString() {
140+
if (locations.length == 0) {
141+
return "ε";
142+
}
143+
144+
String str = "<" + locations[0] + ", " + valuations[0] + ">";
145+
for (int i = 1; i < locations.length; i++) {
146+
str = str +
147+
" -- " +
148+
symbols[i-1] +
149+
" -- <" +
150+
locations[i] +
151+
", " +
152+
valuations[i] +
153+
">";
154+
}
155+
156+
return str;
157+
}
158+
}

‎src/main/java/de/learnlib/ralib/automata/Transition.java‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,18 @@ public boolean isEnabled(RegisterValuation registers, ParameterValuation paramet
5353
return guard.evaluateSMT(SMTUtil.compose(registers, parameters, consts));
5454
}
5555

56+
public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
57+
return this.getAssignment().valuation(registers, parameters, consts);
58+
}
59+
60+
/*
61+
* @deprecated method is unsafe, use {@link #valuation()} instead
62+
* Method is unsafe because it keeps registers that are not given a new assignment, which can cause
63+
* a discrepancy in the number of registers a location has, depending on the path to the location.
64+
* Method is deprecated rather than removed because the functionality is used by XML automata models.
65+
* Removal of method requires refactoring of XML models.
66+
*/
67+
@Deprecated
5668
public RegisterValuation execute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
5769
return this.getAssignment().compute(registers, parameters, consts);
5870
}

0 commit comments

Comments
 (0)