Fundamental Refactoring of SL Lambda Learning Algorithm

pom.xml

@@ -218,11 +218,6 @@
             <groupId>de.learnlib</groupId>
             <artifactId>learnlib-util</artifactId>
         </dependency>
-        <dependency>
-            <groupId>org.apache.commons</groupId>
-            <artifactId>commons-lang3</artifactId>
-            <version>${commons-lang.version}</version>
-        </dependency>
         <dependency>
             <groupId>tools.aqua</groupId>
             <artifactId>jconstraints-core</artifactId>

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

@@ -17,6 +17,7 @@
 package de.learnlib.ralib.automata;
 
 import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
 
 import de.learnlib.ralib.data.Constants;
@@ -42,6 +43,27 @@ public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment)
         this.assignment = assignment;
     }
 
+    public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
+    	RegisterValuation val = new RegisterValuation();
+    	for (Map.Entry<Register, ? extends SymbolicDataValue> e : assignment.entrySet()) {
+    		Register x = e.getKey();
+    		SymbolicDataValue sdv = e.getValue();
+    		DataValue d = sdv.isParameter() ? parameters.get((Parameter) sdv) :
+    			sdv.isRegister() ? registers.get((Register) sdv) :
+    				sdv.isConstant() ? consts.get((Constant) sdv) :
+    					null;
+    		if (d == null) {
+    			throw new IllegalStateException("Illegal assignment: " + x + " := " + sdv);
+    		}
+    		val.put(x, d);
+    	}
+    	return val;
+    }
+
+    /*
+     * @deprecated method is unsafe, use {@link #valuation()} instead
+     */
+    @Deprecated
     public RegisterValuation compute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
         RegisterValuation val = new RegisterValuation();
         List<String> rNames = assignment.keySet().stream().map(k -> k.getName()).toList();
@@ -56,6 +78,12 @@ public RegisterValuation compute(RegisterValuation registers, ParameterValuation
                 val.put(e.getKey(), registers.get((Register) valp));
             }
             else if (valp.isParameter()) {
+            	DataValue dv = parameters.get((Parameter) valp);
+            	for (Map.Entry<Parameter, DataValue> ep : parameters.entrySet()) {
+            		if (ep.getKey().equals(valp)) {
+            			dv = ep.getValue();
+            		}
+            	}
                 val.put(e.getKey(), parameters.get((Parameter) valp));
             }
             //TODO: check if we want to copy constant values into vars

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

@@ -28,7 +28,6 @@
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
 import net.automatalib.automaton.MutableDeterministic;
-import net.automatalib.common.util.Pair;
 import net.automatalib.word.Word;
 
 /**
@@ -119,39 +118,6 @@ protected List<Transition> getTransitions(Word<PSymbolInstance> dw) {
         return tseq;
     }
 
-    protected List<Pair<Transition,RegisterValuation>> getTransitionsAndValuations(Word<PSymbolInstance> dw) {
-        RegisterValuation vars = RegisterValuation.copyOf(getInitialRegisters());
-        RALocation current = initial;
-        List<Pair<Transition,RegisterValuation>> tvseq = new ArrayList<>();
-        for (PSymbolInstance psi : dw) {
-
-            ParameterValuation pars = ParameterValuation.fromPSymbolInstance(psi);
-
-            Collection<Transition> candidates =
-                    current.getOut(psi.getBaseSymbol());
-
-            if (candidates == null) {
-                return null;
-            }
-
-            boolean found = false;
-            for (Transition t : candidates) {
-                if (t.isEnabled(vars, pars, constants)) {
-                    vars = t.execute(vars, pars, constants);
-                    current = t.getDestination();
-                    tvseq.add(Pair.of(t, RegisterValuation.copyOf(vars)));
-                    found = true;
-                    break;
-                }
-            }
-
-            if (!found) {
-                return null;
-            }
-        }
-        return tvseq;
-    }
-
     @Override
     public RALocation getLocation(Word<PSymbolInstance> dw) {
         List<Transition> tseq = getTransitions(dw);
@@ -300,4 +266,43 @@ public Transition copyTransition(Transition t, RALocation s) {
         throw new UnsupportedOperationException("Not supported yet.");
     }
 
+    public RARun getRun(Word<PSymbolInstance> word) {
+        int n = word.length();
+        RALocation[] locs = new RALocation[n+1];
+        RegisterValuation[] vals = new RegisterValuation[n+1];
+        PSymbolInstance[] symbols = new PSymbolInstance[n];
+        Transition[] transitions = new Transition[n];
+
+        locs[0] = getInitialState();
+        vals[0] = new RegisterValuation();
+
+        for (int i = 0; i < n; i++) {
+            symbols[i] = word.getSymbol(i);
+            ParameterValuation pars = ParameterValuation.fromPSymbolInstance(symbols[i]);
+
+            Collection<Transition> candidates = locs[i].getOut(symbols[i].getBaseSymbol());
+            if (candidates == null) {
+                return null;
+            }
+
+            boolean found = false;
+
+            for (Transition t : candidates) {
+                if (t.isEnabled(vals[i], pars, constants)) {
+                    transitions[i] = t;
+                    vals[i+1] = t.execute(vals[i], pars, constants);
+                    locs[i+1] = t.getDestination();
+                    found = true;
+                    break;
+                }
+            }
+
+            if (!found) {
+                return null;
+            }
+        }
+
+        return new RARun(locs, vals, symbols, transitions);
+    }
+
 }

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

@@ -0,0 +1,158 @@
+package de.learnlib.ralib.automata;
+
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import de.learnlib.ralib.automata.output.OutputMapping;
+import de.learnlib.ralib.automata.output.OutputTransition;
+import de.learnlib.ralib.data.Constants;
+import de.learnlib.ralib.data.DataValue;
+import de.learnlib.ralib.data.Mapping;
+import de.learnlib.ralib.data.RegisterValuation;
+import de.learnlib.ralib.data.SymbolicDataValue;
+import de.learnlib.ralib.data.SymbolicDataValue.Parameter;
+import de.learnlib.ralib.smt.VarsValuationVisitor;
+import de.learnlib.ralib.words.PSymbolInstance;
+import gov.nasa.jpf.constraints.api.Expression;
+import gov.nasa.jpf.constraints.expressions.NumericBooleanExpression;
+import gov.nasa.jpf.constraints.expressions.NumericComparator;
+import gov.nasa.jpf.constraints.util.ExpressionUtil;
+
+/**
+ * Data structure containing the locations, register valuations, symbol instances
+ * and transitions at each step of a run of a hypothesis over a data word.
+ *
+ * @author fredrik
+ */
+public class RARun {
+
+	private final RALocation[] locations;
+	private final RegisterValuation[] valuations;
+	private final PSymbolInstance[] symbols;
+	private final Transition[] transitions;
+
+	public RARun(RALocation[] locations, RegisterValuation[] valuations, PSymbolInstance[] symbols, Transition[] transitions) {
+		this.locations = locations;
+		this.valuations = valuations;
+		this.symbols = symbols;
+		this.transitions = transitions;
+	}
+
+	public RALocation getLocation(int i) {
+		return locations[i];
+	}
+
+	public RegisterValuation getValuation(int i) {
+		return valuations[i];
+	}
+
+	public PSymbolInstance getTransitionSymbol(int i) {
+		return symbols[i-1];
+	}
+
+	public Transition getRATransition(int i) {
+		return transitions[i-1];
+	}
+
+	/**
+	 * Get the guard of the {@code Transition} at index {@code i}. If the {@code Transition}
+	 * is an {@code OutputTransition}, the guard is computed from the transition's
+	 * {@code OutputMapping}.
+	 *
+	 * @param i
+	 * @return
+	 */
+	public Expression<Boolean> getGuard(int i) {
+		Transition transition = getRATransition(i);
+		if (transition == null) {
+			return null;
+		}
+		return transition instanceof OutputTransition ?
+				outputGuard((OutputTransition) transition) :
+					transition.getGuard();
+	}
+
+	/**
+	 * Get the guard of the {@code Transition} at index {@code i}. If the {@code Transition}
+	 * is an {@code OutputTransition}, the guard is computed from the transition's
+	 * {@code OutputMapping}. Registers of the guard will be evaluated according to  the
+	 * data values from the register valuation at index {@code i}, and constants will be
+	 * evaluated according to {@code consts}.
+	 *
+	 * @param i
+	 * @return
+	 */
+	public Expression<Boolean> getGuard(int i, Constants consts) {
+		Expression<Boolean> guard = getGuard(i);
+		VarsValuationVisitor vvv = new VarsValuationVisitor();
+		Mapping<SymbolicDataValue, DataValue> vals = new Mapping<>();
+		vals.putAll(getValuation(i));
+		vals.putAll(consts);
+		return vvv.apply(guard, vals);
+	}
+
+	private Expression<Boolean> outputGuard(OutputTransition t) {
+		OutputMapping out = t.getOutput();
+
+		Set<Parameter> params = new LinkedHashSet<>();
+		params.addAll(out.getFreshParameters());
+		params.addAll(out.getOutput().keySet());
+		Set<SymbolicDataValue> regs = new LinkedHashSet<>();
+		regs.addAll(out.getOutput().values());
+
+		Expression[] expressions = new Expression[params.size()];
+		int index = 0;
+
+		// fresh parameters
+		List<Parameter> prior = new ArrayList<>();
+		List<Parameter> fresh = new ArrayList<>(out.getFreshParameters());
+		Collections.sort(fresh, (a,b) -> Integer.compare(a.getId(), b.getId()));
+		for (Parameter p : fresh) {
+			Expression[] diseq = new Expression[prior.size() + regs.size()];
+			int i = 0;
+			for (Parameter prev : prior) {
+				diseq[i++] = new NumericBooleanExpression(p, NumericComparator.NE, prev);
+			}
+			for (SymbolicDataValue s : regs) {
+				diseq[i++] = new NumericBooleanExpression(p, NumericComparator.NE, s);
+			}
+			expressions[index++] = ExpressionUtil.and(diseq);
+			prior.add(p);
+		}
+
+		// mapped parameters
+		for (Map.Entry<Parameter, SymbolicDataValue> e : out.getOutput().entrySet()) {
+			Parameter p = e.getKey();
+			SymbolicDataValue s = e.getValue();
+			expressions[index++] = new NumericBooleanExpression(p, NumericComparator.EQ, s);
+		}
+
+		return ExpressionUtil.and(expressions);
+	}
+
+	@Override
+	public String toString() {
+		if (locations.length == 0) {
+			return "ε";
+		}
+
+		String str = "<" + locations[0] + ", " + valuations[0] + ">";
+		for (int i = 1; i < locations.length; i++) {
+			str = str +
+					" -- " +
+					symbols[i-1] +
+					" -- <" +
+					locations[i] +
+					", " +
+					valuations[i] +
+					">";
+		}
+
+		return str;
+	}
+}

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

@@ -53,6 +53,14 @@ public boolean isEnabled(RegisterValuation registers, ParameterValuation paramet
         return guard.evaluateSMT(SMTUtil.compose(registers, parameters, consts));
     }
 
+    public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
+    	return this.getAssignment().valuation(registers, parameters, consts);
+    }
+
+    /*
+     * @deprecated method is unsafe, use {@link #valuation()} instead
+     */
+    @Deprecated
     public RegisterValuation execute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
         return this.getAssignment().compute(registers, parameters, consts);
     }