@@ -206,5 +207,10 @@
org.slf4j
slf4j-api
+
+ com.google.code.gson
+ gson
+ ${gson.version}
+
diff --git a/src/main/java/de/learnlib/ralib/data/DataValue.java b/src/main/java/de/learnlib/ralib/data/DataValue.java
index ec3bc65e..17658ad5 100644
--- a/src/main/java/de/learnlib/ralib/data/DataValue.java
+++ b/src/main/java/de/learnlib/ralib/data/DataValue.java
@@ -73,5 +73,33 @@ public DataType getType() {
return type;
}
+ public static DataValue
valueOf(String strVal, DataType type) {
+ return new DataValue(type, valueOf(strVal, type.getBase()));
+ }
+
+ public static
P valueOf(String strVal, Class
cls) {
+ P realValue = null;
+ if (Number.class.isAssignableFrom(cls)) {
+ Object objVal;
+ try {
+ objVal = cls.getMethod("valueOf", String.class).invoke(cls, strVal);
+
+ realValue = cls.cast(objVal);
+ } catch (Exception e) {
+ throw new RuntimeException(e);
+ }
+ } else {
+ if (cls.isPrimitive()) {
+ if (cls.equals(int.class))
+ return (P) Integer.valueOf(strVal);
+ else if (cls.equals(double.class))
+ return (P) Double.valueOf(strVal);
+ else if (cls.equals(long.class))
+ return (P) Long.valueOf(strVal);
+ }
+ throw new RuntimeException("Cannot deserialize values of the class " + cls);
+ }
+ return realValue;
+ }
}
diff --git a/src/main/java/de/learnlib/ralib/tools/AbstractToolWithRandomWalk.java b/src/main/java/de/learnlib/ralib/tools/AbstractToolWithRandomWalk.java
index 24f0b09a..aadb2fa8 100644
--- a/src/main/java/de/learnlib/ralib/tools/AbstractToolWithRandomWalk.java
+++ b/src/main/java/de/learnlib/ralib/tools/AbstractToolWithRandomWalk.java
@@ -22,6 +22,10 @@
import java.util.Random;
import java.util.logging.Level;
+import com.google.gson.Gson;
+
+import de.learnlib.ralib.data.DataType;
+import de.learnlib.ralib.data.DataValue;
import de.learnlib.ralib.solver.ConstraintSolver;
import de.learnlib.ralib.solver.ConstraintSolverFactory;
import de.learnlib.ralib.tools.classanalyzer.TypedTheory;
@@ -134,6 +138,11 @@ public Level parse(Configuration c) throws ConfigurationException {
", " + ConstraintSolverFactory.ID_Z3 + ".",
ConstraintSolverFactory.ID_SIMPLE, true);
+ protected static final ConfigurationOption.StringOption OPTION_CONSTANTS
+ = new ConfigurationOption.StringOption("constants",
+ "Regular constants of form [{\"type\":typeA,\"value\":\"valueA\"}, ...]",
+ null, true);
+
protected Random random = null;
protected boolean useCeOptimizers;
@@ -210,4 +219,29 @@ private Pair parseTeacherConfig(String config)
throw new ConfigurationException(ex.getMessage());
}
}
+
+ protected DataValue[] parseDataValues(String gsonDataValueArray, Map typeMap) {
+ Gson gson = new Gson();
+ GsonDataValue[] gDvs = gson.fromJson(gsonDataValueArray, GsonDataValue[].class);
+ DataValue[] dataValues = new DataValue[gDvs.length];
+ for (int i = 0; i < gDvs.length; i++) {
+ DataType type = typeMap.get(gDvs[i].type);
+ dataValues[i] = gDvs[i].toDataValue(type);
+ }
+
+ return dataValues;
+ }
+
+ static class GsonDataValue {
+ public String type;
+ public String value;
+
+ public DataValue toDataValue(DataType type) {
+ if (type.getName().compareTo(this.type) != 0) {
+ throw new RuntimeException("Type name mismatch");
+ }
+ DataValue dv = new DataValue(type, DataValue.valueOf(value, type.getBase()));
+ return dv;
+ }
+ }
}
diff --git a/src/main/java/de/learnlib/ralib/tools/ClassAnalyzer.java b/src/main/java/de/learnlib/ralib/tools/ClassAnalyzer.java
index bf187460..0ccf1d63 100644
--- a/src/main/java/de/learnlib/ralib/tools/ClassAnalyzer.java
+++ b/src/main/java/de/learnlib/ralib/tools/ClassAnalyzer.java
@@ -31,6 +31,8 @@
import de.learnlib.ralib.automata.xml.RegisterAutomatonExporter;
import de.learnlib.ralib.data.Constants;
import de.learnlib.ralib.data.DataType;
+import de.learnlib.ralib.data.DataValue;
+import de.learnlib.ralib.data.util.SymbolicDataValueGenerator;
import de.learnlib.ralib.equivalence.IOCounterExamplePrefixFinder;
import de.learnlib.ralib.equivalence.IOCounterExamplePrefixReplacer;
import de.learnlib.ralib.equivalence.IOCounterexampleLoopRemover;
@@ -126,6 +128,8 @@ public class ClassAnalyzer extends AbstractToolWithRandomWalk {
private Map teachers;
+ private final Constants consts = new Constants();
+
private Class target = null;
private final Map types = new LinkedHashMap<>();
@@ -166,11 +170,6 @@ public void setup(Configuration config) throws ConfigurationException {
Integer md = OPTION_MAX_DEPTH.parse(config);
- sulLearn = new ClasssAnalyzerDataWordSUL(target, methods, md);
- if (this.timeoutMillis > 0L) {
- this.sulLearn = new TimeOutSUL(this.sulLearn, this.timeoutMillis);
- }
-
ParameterizedSymbol[] inputSymbols = inList.toArray(new ParameterizedSymbol[]{});
actList.add(SpecialSymbols.ERROR);
@@ -181,7 +180,17 @@ public void setup(Configuration config) throws ConfigurationException {
actList.add(SpecialSymbols.DEPTH);
ParameterizedSymbol[] actions = actList.toArray(new ParameterizedSymbol[]{});
- final Constants consts = new Constants();
+ String cstString = OPTION_CONSTANTS.parse(config);
+ if (cstString != null) {
+ final SymbolicDataValueGenerator.ConstantGenerator cgen = new SymbolicDataValueGenerator.ConstantGenerator();
+ DataValue[] cstArray = super.parseDataValues(cstString, types);
+ Arrays.stream(cstArray).forEach(c -> consts.put(cgen.next(c.getType()), c));
+ }
+
+ sulLearn = new ClasssAnalyzerDataWordSUL(target, methods, md, consts);
+ if (this.timeoutMillis > 0L) {
+ this.sulLearn = new TimeOutSUL(this.sulLearn, this.timeoutMillis);
+ }
// create teachers
teachers = new LinkedHashMap();
@@ -235,8 +244,6 @@ public TreeOracle createTreeOracle(RegisterAutomaton hyp) {
}
};
- //this.rastar = new RaStar(mto, hypFactory, mlo, consts, true, actions);
-
switch (this.learner) {
case AbstractToolWithRandomWalk.LEARNER_SLSTAR:
this.rastar = new RaStar(mto, hypFactory, mlo, consts, true, actions);
@@ -355,7 +362,7 @@ public void run() throws RaLibToolException {
Word sysTrace = back.trace(ce.getInput());
System.out.println("### SYS TRACE: " + sysTrace);
- SimulatorSUL hypSul = new SimulatorSUL(hyp, teachers, new Constants());
+ SimulatorSUL hypSul = new SimulatorSUL(hyp, teachers, consts);
IOOracle iosul = new SULOracle(hypSul, SpecialSymbols.ERROR);
Word hypTrace = iosul.trace(ce.getInput());
System.out.println("### HYP TRACE: " + hypTrace);
diff --git a/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java b/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java
index 4cf8c0ce..58e7d33c 100644
--- a/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java
+++ b/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java
@@ -22,6 +22,7 @@
import java.util.Map;
import de.learnlib.exception.SULException;
+import de.learnlib.ralib.data.Constants;
import de.learnlib.ralib.data.DataType;
import de.learnlib.ralib.data.DataValue;
import de.learnlib.ralib.data.FreshValue;
@@ -47,10 +48,17 @@ public class ClasssAnalyzerDataWordSUL extends DataWordSUL {
private final Map> buckets = new HashMap<>();
+ private final Constants consts;
+
public ClasssAnalyzerDataWordSUL(Class sulClass, Map methods, int d) {
- this.sulClass = sulClass;
- this.methods = methods;
- this.maxDepth = d;
+ this(sulClass, methods, d, new Constants());
+ }
+
+ public ClasssAnalyzerDataWordSUL(Class sulClass, Map methods, int d, Constants consts) {
+ this.sulClass = sulClass;
+ this.methods = methods;
+ this.maxDepth = d;
+ this.consts = consts;
}
@Override
@@ -151,6 +159,12 @@ private Object resolve(DataValue d) {
}
private boolean isFresh(DataType t, Object id) {
+ if (consts.values()
+ .stream()
+ .filter(d -> d.getType().equals(t) && d.getId().equals(id))
+ .findAny()
+ .isPresent())
+ return false;
Map map = this.buckets.get(t);
return map == null || !map.containsValue(id);
}
diff --git a/src/test/java/de/learnlib/ralib/example/container/ContainerSUL.java b/src/test/java/de/learnlib/ralib/example/container/ContainerSUL.java
new file mode 100644
index 00000000..eeb4c550
--- /dev/null
+++ b/src/test/java/de/learnlib/ralib/example/container/ContainerSUL.java
@@ -0,0 +1,16 @@
+package de.learnlib.ralib.example.container;
+
+public class ContainerSUL {
+
+ public static final int ERROR = 0;
+
+ private Integer val = null;
+
+ public void put(Integer val) {
+ this.val = val;
+ }
+
+ public Integer get() {
+ return val == null ? ERROR : val;
+ }
+}
diff --git a/src/test/java/de/learnlib/ralib/tools/ClassAnalyzerTest.java b/src/test/java/de/learnlib/ralib/tools/ClassAnalyzerTest.java
index 094b3cbd..c2afef78 100644
--- a/src/test/java/de/learnlib/ralib/tools/ClassAnalyzerTest.java
+++ b/src/test/java/de/learnlib/ralib/tools/ClassAnalyzerTest.java
@@ -131,4 +131,39 @@ public void classAnalyzerInequalitiesTest() {
}
}
+ @Test
+ public void classAnalyzerConstantsTest() {
+
+ final String[] options = new String[] {
+ "class-analyzer",
+ "target=de.learnlib.ralib.example.container.ContainerSUL;" +
+ "methods=put(java.lang.Integer:int)void+" +
+ "get()java.lang.Integer:int;" +
+ "random.seed=652102309071547789;" +
+ "logging.level=WARNING;" +
+ "max.time.millis=600000;" +
+ "learner=sllambda;" +
+ "use.ceopt=false;" +
+ "use.suffixopt=true;" +
+ "use.fresh=true;" +
+ "use.rwalk=true;" +
+ "export.model=false;" +
+ "rwalk.prob.fresh=0.8;" +
+ "rwalk.prob.reset=0.1;" +
+ "rwalk.max.depth=6;" +
+ "rwalk.max.runs=1000;" +
+ "rwalk.reset.count=false;" +
+ "rwalk.draw.uniform=false;" +
+ "teachers=int:de.learnlib.ralib.tools.theories.IntegerEqualityTheory;" +
+ "constants=[{'type':'int','value':'0'}]"};
+
+ try {
+ ConsoleClient cl = new ConsoleClient(options);
+ int ret = cl.run();
+ Assert.assertEquals(ret, 0);
+ } catch (Throwable t) {
+ Assert.fail(t.getClass().getName());
+ }
+ }
+
}