Array counter examples (#21)

* Add noModelElementSet value to enum

* Add support for the lus_main_const option

* Support parsing type of arbitrary arrays

* Reduced code duplication

Author: Jabe03

src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java

@@ -41,6 +41,8 @@ public class Labels
   public static final String blockType = "blockType";
   public static final String streams = "streams";
   public static final String type = "type";
+  public static final String typeInfo = "typeInfo";
+  public static final String baseType = "baseType";
   public static final String classField = "class";
   public static final String instantValues = "instantValues";
   public static final String subNodes = "subnodes";

src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java

@@ -48,7 +48,8 @@ public Stream(SubNode kind2SubNode, JsonElement jsonElement)
     json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement);
     name = jsonElement.getAsJsonObject().get(Labels.name).getAsString();
     String typeString = jsonElement.getAsJsonObject().get(Labels.type).getAsString();
-    kind2Type = Type.getType(typeString);
+    JsonElement typeInfo = jsonElement.getAsJsonObject().get(Labels.typeInfo);
+    kind2Type = Type.getType(typeString, typeInfo);
     streamClass = jsonElement.getAsJsonObject().get(Labels.classField).getAsString();
 
     this.stepValues = new ArrayList<>();

src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java

@@ -6,6 +6,9 @@
  */
 
 package edu.uiowa.cs.clc.kind2.results;
+import edu.uiowa.cs.clc.kind2.Kind2Exception;
+
+import com.google.gson.JsonElement;
 
 /**
  * An abstract class for all kind2 types.
@@ -21,7 +24,20 @@ public Type(String name)
 
   public static Type getType(String type)
   {
-    switch (type)
+    return getType(type, null);
+  }
+  private static Type makeNestedArray(String baseType, int numDims){
+    if (numDims == 0){
+      return getType(baseType);
+    } else {
+      return new Array(makeNestedArray(baseType, numDims-1));
+    }
+  }
+  
+
+  public static Type getType(String typeString, JsonElement typeInfo)
+  {
+    switch (typeString)
     {
       case "bool":
         return new Bool();
@@ -39,27 +55,30 @@ public static Type getType(String type)
       case "real":
         return new Real();
       case "array":
-        return new Array(new Bool());
+        if (typeInfo == null) throw new Kind2Exception("Array with no type info found");
+        String baseType =  typeInfo.getAsJsonObject().get(Labels.baseType).getAsString();
+        int numIndicies = typeInfo.getAsJsonObject().get("sizes").getAsJsonArray().size();
+        return makeNestedArray(baseType, numIndicies);
       default:
       {
-        if (type.matches("subrange \\[.*?\\] of int"))
+        if (typeString.matches("subrange \\[.*?\\] of int"))
         {
-          String [] range = type.replaceAll("subrange \\[", "")
+          String [] range = typeString.replaceAll("subrange \\[", "")
                                 .replaceAll("\\] of int", "").split(",");
           int min = Integer.parseInt(range[0]);
           int max = Integer.parseInt(range[0]);
           return new SubRange(min, max);
         }
 
-        if (type.startsWith("array of"))
+        if (typeString.startsWith("array of"))
         {
-          String elementTypeName = type.replaceFirst("array of", "").trim();
+          String elementTypeName = typeString.replaceFirst("array of", "").trim();
           Type elementType = getType(elementTypeName);
           return new Array(elementType);
         }
 
         // the type is enum
-        return new Enum(type);
+        return new Enum(typeString);
       }
     }
   }