From 0b7bd6539f1b471e0d1df997170b251e6b950339 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Fri, 20 Feb 2026 10:36:07 -0600 Subject: [PATCH 1/4] Add noModelElementSet value to enum --- src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java index 184f559..0dcab85 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java @@ -24,8 +24,8 @@ public enum Object modelElementSet("modelElementSet"), progress("progress"), lsp("lsp"), - modelSetEnumeration("modelSetEnumeration"); - + modelSetEnumeration("modelSetEnumeration"), + noModelElementSet("noModelElementSet"); private final String value; private Object(String value) @@ -63,6 +63,8 @@ public static Object getKind2Object(String kind2Object) return lsp; case "modelSetEnumeration": return modelSetEnumeration; + case "noModelElementSet": + return noModelElementSet; default: throw new UnsupportedOperationException("Value " + kind2Object + " is not defined"); } From 46fdd59d931beaaeb2202514e386a8e735cf84b3 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Wed, 1 Apr 2026 16:35:24 -0500 Subject: [PATCH 2/4] Add support for the lus_main_const option --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 19 ++++++++++++++++++- .../uiowa/cs/clc/kind2/results/Result.java | 1 + 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 5099e7f..30b2b40 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -110,6 +110,7 @@ public class Kind2Api { private LogLevel logLevel; private String lusMain; private String lusMainType; + private String lusMainConst; private String fakeFilepath; public Kind2Api() { @@ -178,6 +179,7 @@ public Kind2Api() { logLevel = null; lusMain = null; lusMainType = null; + lusMainConst = null; } DebugLogger debug = new DebugLogger(); @@ -418,6 +420,10 @@ public List getOptions() { options.add("--lus_main_type"); options.add(lusMainType); } + if (lusMainConst != null) { + options.add("--lus_main_const"); + options.add(lusMainConst); + } if (smtSolver != null) { options.add("--smt_solver"); options.add(smtSolver.toString()); @@ -1423,12 +1429,23 @@ public void setLusMain(String lusMain) { *

* Default: "--%MAIN" annotation in source if any, last node otherwise * - * @param lusMainType the main node + * @param lusMainType the main type */ public void setLusMainType(String lusMainType) { this.lusMainType = lusMainType; } + /** + * Set the top type declaration in the Lustre input file. + *

+ * Default: "--%MAIN" annotation in source if any, last node otherwise + * + * @param lusMainConst the main constant + */ + public void setLusMainConst(String lusMainConst) { + this.lusMainConst = lusMainConst; + } + /** * Set the fake filepath for error messages. * diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java index b064821..932d9cb 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java @@ -186,6 +186,7 @@ public void initialize(String json) { astInfo = new TypeDeclInfo(jsonElement); break; case "constDecl": + case "paramDecl": astInfo = new ConstDeclInfo(jsonElement); break; case "node": From 7716f9b9db57365099afd0c7e2b1847f82463a53 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Mon, 6 Apr 2026 16:44:36 -0500 Subject: [PATCH 3/4] Support parsing type of arbitrary arrays --- .../uiowa/cs/clc/kind2/results/Labels.java | 2 + .../uiowa/cs/clc/kind2/results/Stream.java | 3 +- .../edu/uiowa/cs/clc/kind2/results/Type.java | 58 +++++++++++++++++++ 3 files changed, 61 insertions(+), 2 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java index 0937d73..a286c8d 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Labels.java +++ b/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"; diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java index 33dbcdc..e2e7456 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java @@ -47,8 +47,7 @@ public Stream(SubNode kind2SubNode, JsonElement jsonElement) this.kind2SubNode = kind2SubNode; 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); + kind2Type = Type.getType(jsonElement); streamClass = jsonElement.getAsJsonObject().get(Labels.classField).getAsString(); this.stepValues = new ArrayList<>(); diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java index 1790776..b3d8e6d 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java @@ -7,6 +7,8 @@ package edu.uiowa.cs.clc.kind2.results; +import com.google.gson.JsonElement; + /** * An abstract class for all kind2 types. */ @@ -63,6 +65,62 @@ public static Type getType(String type) } } } + 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(JsonElement typeInfo) + { + String typeString = typeInfo.getAsJsonObject().get(Labels.type).getAsString(); + switch (typeString) + { + case "bool": + return new Bool(); + case "int": + case "uint8": + case "uint16": + case "uint32": + case "uint64": + case "int8": + case "int16": + case "int32": + case "int64": + case "subrange": + return new Int(); + case "real": + return new Real(); + case "array": + String baseType = typeInfo.getAsJsonObject().get(Labels.typeInfo).getAsJsonObject().get(Labels.baseType).getAsString(); + int numIndicies = typeInfo.getAsJsonObject().get(Labels.typeInfo).getAsJsonObject().get("sizes").getAsJsonArray().size(); + return makeNestedArray(baseType, numIndicies); + default: + { + if (typeString.matches("subrange \\[.*?\\] of int")) + { + 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 (typeString.startsWith("array of")) + { + String elementTypeName = typeString.replaceFirst("array of", "").trim(); + Type elementType = getType(elementTypeName); + return new Array(elementType); + } + + // the type is enum + return new Enum(typeString); + } + } + } @Override public String toString() From 82e8aad3702afd53561705feebddaab32d9f4639 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Fri, 10 Apr 2026 09:29:57 -0500 Subject: [PATCH 4/4] Reduced code duplication --- .../uiowa/cs/clc/kind2/results/Stream.java | 4 +- .../edu/uiowa/cs/clc/kind2/results/Type.java | 51 +++---------------- 2 files changed, 9 insertions(+), 46 deletions(-) diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java index e2e7456..0267144 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Stream.java @@ -47,7 +47,9 @@ public Stream(SubNode kind2SubNode, JsonElement jsonElement) this.kind2SubNode = kind2SubNode; json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement); name = jsonElement.getAsJsonObject().get(Labels.name).getAsString(); - kind2Type = Type.getType(jsonElement); + String typeString = jsonElement.getAsJsonObject().get(Labels.type).getAsString(); + JsonElement typeInfo = jsonElement.getAsJsonObject().get(Labels.typeInfo); + kind2Type = Type.getType(typeString, typeInfo); streamClass = jsonElement.getAsJsonObject().get(Labels.classField).getAsString(); this.stepValues = new ArrayList<>(); diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java index b3d8e6d..71b4d10 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Type.java @@ -6,6 +6,7 @@ */ package edu.uiowa.cs.clc.kind2.results; +import edu.uiowa.cs.clc.kind2.Kind2Exception; import com.google.gson.JsonElement; @@ -23,47 +24,7 @@ public Type(String name) public static Type getType(String type) { - switch (type) - { - case "bool": - return new Bool(); - case "int": - case "uint8": - case "uint16": - case "uint32": - case "uint64": - case "int8": - case "int16": - case "int32": - case "int64": - case "subrange": - return new Int(); - case "real": - return new Real(); - case "array": - return new Array(new Bool()); - default: - { - if (type.matches("subrange \\[.*?\\] of int")) - { - String [] range = type.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")) - { - String elementTypeName = type.replaceFirst("array of", "").trim(); - Type elementType = getType(elementTypeName); - return new Array(elementType); - } - - // the type is enum - return new Enum(type); - } - } + return getType(type, null); } private static Type makeNestedArray(String baseType, int numDims){ if (numDims == 0){ @@ -74,9 +35,8 @@ private static Type makeNestedArray(String baseType, int numDims){ } - public static Type getType(JsonElement typeInfo) + public static Type getType(String typeString, JsonElement typeInfo) { - String typeString = typeInfo.getAsJsonObject().get(Labels.type).getAsString(); switch (typeString) { case "bool": @@ -95,8 +55,9 @@ public static Type getType(JsonElement typeInfo) case "real": return new Real(); case "array": - String baseType = typeInfo.getAsJsonObject().get(Labels.typeInfo).getAsJsonObject().get(Labels.baseType).getAsString(); - int numIndicies = typeInfo.getAsJsonObject().get(Labels.typeInfo).getAsJsonObject().get("sizes").getAsJsonArray().size(); + 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: {