From 0b7bd6539f1b471e0d1df997170b251e6b950339 Mon Sep 17 00:00:00 2001
From: Joshua Bergthold <jbergthold@uiowa.edu>
Date: Fri, 20 Feb 2026 10:36:07 -0600
Subject: [PATCH 1/3] 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 <jbergthold@uiowa.edu>
Date: Wed, 1 Apr 2026 16:35:24 -0500
Subject: [PATCH 2/3] 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<String> 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) {
    * <p>
    * 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.
+   * <p>
+   * 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 496945a3f2809af57b3b250344ce58128bae30b2 Mon Sep 17 00:00:00 2001
From: Joshua Bergthold <jbergthold@uiowa.edu>
Date: Thu, 9 Apr 2026 15:29:16 -0500
Subject: [PATCH 3/3] Correct javadoc comments

---
 src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 8 ++++----
 1 file changed, 4 insertions(+), 4 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 30b2b40..7209019 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
@@ -1425,9 +1425,9 @@ public void setLusMain(String lusMain) {
   }
 
   /**
-   * Set the top type declaration in the Lustre input file.
+   * Designate a type declaration in the Lustre input file as the main 
+   * model element for the analysis
    * <p>
-   * Default: "--%MAIN" annotation in source if any, last node otherwise
    *
    * @param lusMainType the main type
    */
@@ -1436,9 +1436,9 @@ public void setLusMainType(String lusMainType) {
   }
 
   /**
-   * Set the top type declaration in the Lustre input file.
+   * Designate a constant declaration in the Lustre input file as the main 
+   * model element for the analysis   
    * <p>
-   * Default: "--%MAIN" annotation in source if any, last node otherwise
    *
    * @param lusMainConst the main constant
    */