From 0b7bd6539f1b471e0d1df997170b251e6b950339 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Fri, 20 Feb 2026 10:36:07 -0600 Subject: [PATCH 1/7] 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/7] 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/7] 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/7] 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: { From b068b9eee92d4482206bf9d700db380d1c8ab5c5 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Thu, 30 Apr 2026 07:33:15 -0500 Subject: [PATCH 5/7] Incremental with executable and API --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 29 ++-- .../uiowa/cs/clc/kind2/results/Result.java | 158 +++++++++++++++++- 2 files changed, 170 insertions(+), 17 deletions(-) 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 7209019..f692211 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 @@ -9,12 +9,17 @@ import java.io.File; import java.io.IOException; +import java.io.InputStreamReader; import java.net.URI; import java.util.ArrayList; +import java.util.Arrays; import java.util.HashSet; import java.util.List; import java.util.Set; +import com.google.gson.JsonElement; +import com.google.gson.JsonStreamParser; + import edu.uiowa.cs.clc.kind2.Kind2Exception; import edu.uiowa.cs.clc.kind2.results.Result; import edu.uiowa.cs.clc.kind2.lustre.Program; @@ -346,33 +351,29 @@ private void callKind2(String program, Result result, IProgressMonitor monitor) ProcessBuilder builder = getKind2ProcessBuilder(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; - String output = ""; boolean exceptionThrown = false; - + JsonStreamParser jsp; try { process = builder.start(); process.getOutputStream().write(program.getBytes()); process.getOutputStream().flush(); process.getOutputStream().close(); - while (!monitor.isCanceled() && process.isAlive()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - sleep(POLL_INTERVAL); + jsp = new JsonStreamParser(new InputStreamReader(process.getInputStream())); + while (!monitor.isCanceled() && jsp.hasNext()) { + JsonElement jele = jsp.next(); + debug.println("Parsing JSON element: " + jele.toString()); + result.initializeInc(jele); + debug.println(result.getResultMap().toString()); } + debug.println("Exited loop because of isCanceled:" + !monitor.isCanceled() + " ; processIsAlive: " + process.isAlive() + "jspHasNext:" + jsp.hasNext()); } catch (Throwable t) { exceptionThrown = true; throw t; } finally { try { if (!monitor.isCanceled()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); try { - result.initialize(output); + result.closeInitialization(); } catch (Throwable t) { if (!exceptionThrown) { throw t; @@ -408,7 +409,7 @@ public void setOtherOptions(List options) { public List getOptions() { List options = new ArrayList<>(); - options.add("-json"); + options.add("-ijson"); if (logLevel != null) { options.add(logLevel.getOption()); } 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 932d9cb..2d84c89 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 @@ -70,7 +70,7 @@ public class Result { /** * Kind2 json output. */ - private String json; + private JsonArray json; /** * a list of kind2 logs. */ @@ -157,7 +157,7 @@ public static Result analyzeJsonResult(String json) { public void initialize(String json) { JsonArray jsonArray = JsonParser.parseString(json).getAsJsonArray(); - this.json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonArray); + this.json = jsonArray; Analysis kind2Analysis = null; // for post analysis Analysis previousAnalysis = null; @@ -286,6 +286,158 @@ public void initialize(String json) { isInitialized = true; } + Analysis kind2Analysis = null; + // for post analysis + Analysis previousAnalysis = null; + boolean emptyAnalysis = false; + public void initializeInc(JsonElement jsonElement) { + if (/*init condition */ this.json == null){ + this.json = new JsonArray(); + + } + JsonObject jsonObject; + String objectType = jsonElement.getAsJsonObject().get(Labels.objectType).getAsString(); + Object kind2Object = Object.getKind2Object(objectType); + switch (kind2Object){ + case kind2Options: + Options options = new Options(jsonElement); + this.options = options; + break; + case log: + Log log = new Log(this, jsonElement); + this.kind2Logs.add(log); + break; + + + case lsp: + jsonObject = jsonElement.getAsJsonObject(); + String kind = jsonObject.get(Labels.kind).getAsString(); + AstInfo astInfo; + switch (kind) { + case "typeDecl": + astInfo = new TypeDeclInfo(jsonElement); + break; + case "constDecl": + case "paramDecl": + astInfo = new ConstDeclInfo(jsonElement); + break; + case "node": + astInfo = new NodeInfo(jsonElement); + break; + case "function": + astInfo = new FunctionInfo(jsonElement); + break; + case "contract": + astInfo = new ContractInfo(jsonElement); + break; + default: + throw new RuntimeException("Failed to analyze kind2 json output"); + } + this.astInfos.add(astInfo); + break; + + case analysisStart: + // define new analysis + kind2Analysis = new Analysis(jsonElement); + this.put(kind2Analysis.getNodeName(), kind2Analysis); + break; + + case analysisStop: + if (kind2Analysis != null) { + // finish the analysis + NodeResult nodeResult = resultMap.get(kind2Analysis.getNodeName()); + for (Analysis analysis : nodeResult.getAnalyses()) { + List subNodes = analysis.getSubNodes(); + for (String node : subNodes) { + if (resultMap.containsKey(node)) { + nodeResult.addChild(resultMap.get(node)); + } + } + } + + + + + + previousAnalysis = kind2Analysis; + kind2Analysis = null; + } else { + throw new RuntimeException("Failed to analyze kind2 json output"); + } + break; + + case property: + if (kind2Analysis != null) { + Property property = new Property(kind2Analysis, jsonElement); + kind2Analysis.addProperty(property); + } else { + throw new RuntimeException("Can not parse kind2 json output"); + } + break; + + case realizabilityResult: + if (kind2Analysis != null) { + jsonObject = jsonElement.getAsJsonObject(); + String res = jsonObject.get(Labels.result).getAsString(); + if (res.equals(Labels.realizable)) { + kind2Analysis.setRealizabilityResult(RealizabilityResult.realizable); + } else if (res.equals(Labels.unrealizable)) { + kind2Analysis.setRealizabilityResult(RealizabilityResult.unrealizable); + } + JsonElement deadlockElement = jsonObject.get(Labels.deadlockingTrace); + String deadlock = new GsonBuilder().setPrettyPrinting().create().toJson(deadlockElement); + kind2Analysis.setDeadlock(deadlock); + } else { + throw new RuntimeException("Can not parse kind2 json output"); + } + break; + + case postAnalysisStart: + if (previousAnalysis != null) { + PostAnalysis postAnalysis = new PostAnalysis(previousAnalysis, jsonElement); + previousAnalysis.setPostAnalysis(postAnalysis); + } else { + // This can occur sometimes with no previous analysis when the node had no properties to check. + emptyAnalysis = true; + } + break; + + case postAnalysisEnd: + if (previousAnalysis != null && previousAnalysis.getPostAnalysis() != null) { + // finish the post analysis + previousAnalysis = null; + } else if (emptyAnalysis){ + //Do nothing, had a no-analysis postAnalysisStart beforehand. + } else { + throw new RuntimeException("Failed to analyze kind2 json output"); + } + break; + + case modelElementSet: + if (previousAnalysis != null && previousAnalysis.getPostAnalysis() != null) { + PostAnalysis postAnalysis = previousAnalysis.getPostAnalysis(); + ModelElementSet elementSet = new ModelElementSet(postAnalysis, jsonElement); + postAnalysis.addModelElementSet(elementSet); + } else { + // This branch gets hit sometimes when we have empty (nonexistent) analyses of nodes with + // no properties to check, causing missing analyses before postAnalyses, as well as this object. + } + break; + } + + } + + public void closeInitialization(){ + + // build the node tree + // this.buildTree(); + // analyze the result + this.analyze(); + + isInitialized = true; + } + + /** * construct a tree of subcomponents. */ @@ -327,7 +479,7 @@ public Options getOptions() { * @return Kind2 json output. */ public String getJson() { - return json; + return json.toString(); } /** From cdfb77c51c9efd7b3c2dca7d47267df4c67547f0 Mon Sep 17 00:00:00 2001 From: Joshua Bergthold Date: Fri, 8 May 2026 12:47:43 -0500 Subject: [PATCH 6/7] Add listener for incremental LSP --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 21 ++++++++++++++++--- .../cs/clc/kind2/api/ResultListener.java | 10 +++++++++ .../uiowa/cs/clc/kind2/results/Result.java | 3 ++- 3 files changed, 30 insertions(+), 4 deletions(-) create mode 100644 src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java 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 f692211..7495f40 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 @@ -193,7 +193,7 @@ public Kind2Api() { * Put the KindApi into debug mode where it saves all output */ public void setApiDebug() { - debug = new DebugLogger("-api-debug-"); + debug = new DebugLogger("c-api-debug-"); } /** @@ -339,14 +339,26 @@ public String interpret(String program, String main, String json) { * @throws Kind2Exception */ public void execute(String program, Result result, IProgressMonitor monitor) { + this.execute(program, result, monitor, (ResultListener)null); + } + + /** + * Run Kind on a Lustre program + * + * @param program Lustre program as text + * @param result Place to store results as they come in + * @param monitor Used to check for cancellation + * @throws Kind2Exception + */ + public void execute(String program, Result result, IProgressMonitor monitor, ResultListener listener) { try { - callKind2(program, result, monitor); + callKind2(program, result, monitor, listener); } catch (Throwable t) { throw new Kind2Exception(t.getMessage(), t); } } - private void callKind2(String program, Result result, IProgressMonitor monitor) + private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); @@ -363,6 +375,9 @@ private void callKind2(String program, Result result, IProgressMonitor monitor) JsonElement jele = jsp.next(); debug.println("Parsing JSON element: " + jele.toString()); result.initializeInc(jele); + if(listener != null){ + listener.onUpdate(result); + } debug.println(result.getResultMap().toString()); } debug.println("Exited loop because of isCanceled:" + !monitor.isCanceled() + " ; processIsAlive: " + process.isAlive() + "jspHasNext:" + jsp.hasNext()); diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java new file mode 100644 index 0000000..2acc0c3 --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java @@ -0,0 +1,10 @@ +package edu.uiowa.cs.clc.kind2.api; + +import edu.uiowa.cs.clc.kind2.results.Result; + + +public interface ResultListener { + + public void onUpdate(Result result); + +} 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 2d84c89..fde1fd9 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 @@ -293,8 +293,9 @@ public void initialize(String json) { public void initializeInc(JsonElement jsonElement) { if (/*init condition */ this.json == null){ this.json = new JsonArray(); - } + this.json.add(jsonElement); + JsonObject jsonObject; String objectType = jsonElement.getAsJsonObject().get(Labels.objectType).getAsString(); Object kind2Object = Object.getKind2Object(objectType); From b9fbdb73535009c5aab9d19133bc37152e69d509 Mon Sep 17 00:00:00 2001 From: Josh Date: Tue, 14 Jul 2026 15:53:43 -0500 Subject: [PATCH 7/7] Clean up --- .../java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 5 ++--- .../java/edu/uiowa/cs/clc/kind2/results/Result.java | 13 +++++++++---- 2 files changed, 11 insertions(+), 7 deletions(-) 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 7495f40..b3c95d0 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 @@ -12,7 +12,6 @@ import java.io.InputStreamReader; import java.net.URI; import java.util.ArrayList; -import java.util.Arrays; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -21,8 +20,8 @@ import com.google.gson.JsonStreamParser; import edu.uiowa.cs.clc.kind2.Kind2Exception; -import edu.uiowa.cs.clc.kind2.results.Result; import edu.uiowa.cs.clc.kind2.lustre.Program; +import edu.uiowa.cs.clc.kind2.results.Result; /** * The primary interface to Kind2. @@ -193,7 +192,7 @@ public Kind2Api() { * Put the KindApi into debug mode where it saves all output */ public void setApiDebug() { - debug = new DebugLogger("c-api-debug-"); + debug = new DebugLogger("-api-debug-"); } /** 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 58d7cd0..ffd39cf 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 @@ -7,16 +7,21 @@ package edu.uiowa.cs.clc.kind2.results; +import java.math.RoundingMode; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + import com.google.gson.GsonBuilder; import com.google.gson.JsonArray; import com.google.gson.JsonElement; import com.google.gson.JsonObject; import com.google.gson.JsonParser; -import java.math.RoundingMode; -import java.util.*; -import java.util.stream.Collectors; - /** * The class is the top one in Kind2 explanations. An instance of this class is generated from kind2 * json string using the method {@link Result#analyzeJsonResult(String)}. The returned instance