Support for constants in class analyzer

pom.xml

@@ -22,6 +22,7 @@
         <jaxb-runtime.version>4.0.5</jaxb-runtime.version>
         <jconstraints.version>0.9.9</jconstraints.version>
         <learnlib.version>0.17.0</learnlib.version>
+        <gson.version>2.8.0</gson.version>
     </properties>
 
     <build>
@@ -206,5 +207,10 @@
             <groupId>org.slf4j</groupId>
             <artifactId>slf4j-api</artifactId>
         </dependency>
+        <dependency>
+            <groupId>com.google.code.gson</groupId>
+            <artifactId>gson</artifactId>
+            <version>${gson.version}</version>
+        </dependency>
     </dependencies>
 </project>

src/main/java/de/learnlib/ralib/data/DataValue.java

@@ -73,5 +73,33 @@ public DataType getType() {
         return type;
     }
 
+    public static <P> DataValue<P> valueOf(String strVal, DataType type) {
+    	return new DataValue(type, valueOf(strVal, type.getBase()));
+    }
+
+    public static <P> P valueOf(String strVal, Class<P> 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;
+    }
 
 }

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<String, TypedTheory> parseTeacherConfig(String config)
             throw new ConfigurationException(ex.getMessage());
         }
     }
+
+    protected DataValue[] parseDataValues(String gsonDataValueArray, Map<String, DataType> 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;
+    	}
+    }
 }

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<DataType, Theory> teachers;
 
+    private final Constants consts = new Constants();
+
     private Class<?> target = null;
 
     private final Map<String, DataType> 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<DataType, Theory>();
@@ -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<PSymbolInstance> 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<PSymbolInstance> hypTrace = iosul.trace(ce.getInput());
             System.out.println("### HYP TRACE: " + hypTrace);

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<DataType, Map<DataValue, Object>> buckets = new HashMap<>();
 
+    private final Constants consts;
+
     public ClasssAnalyzerDataWordSUL(Class<?> sulClass, Map<ParameterizedSymbol, MethodConfig> methods, int d) {
-        this.sulClass = sulClass;
-        this.methods = methods;
-        this.maxDepth = d;
+        this(sulClass, methods, d, new Constants());
+    }
+
+    public ClasssAnalyzerDataWordSUL(Class<?> sulClass, Map<ParameterizedSymbol, MethodConfig> 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<DataValue, Object> map = this.buckets.get(t);
         return map == null || !map.containsValue(id);
     }

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;
+	}
+}

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());
+    	}
+    }
+
 }