Fix Java compiler warnings

Resolves the 14 warnings reported by the Eclipse JDT compiler (the one
backing the VS Code Java extension); javac was already clean.

- Remove unused imports: URISyntaxException (Main), HashMap/Map
  (PostAnalysis), Collector (Suggestion).
- Remove write-only field Node.jsonElement; the constructor parameter is
  still used to build the json string.
- Remove NodeResult.isVisited, which was never read anywhere.
- Add LogLevel.toString() returning the backing value, matching the
  Object enum in the same package. Behaviorally a no-op, since every
  constant's value string is identical to its name.
- Add a default case to the object-type switch in Result.addJsonElement
  so the four untracked constants no longer warn. This matches the
  existing behavior of Result.initialize, which ignores them as well.
- Make Suggestion.getKind2Result() public. It was dead because it was
  private, unlike the equivalent accessor on NodeResult, Property,
  StepValue, Value, and SubNode, which are all public.
- Drop two unused local variables in Kind2ResultTests, keeping the calls.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: daniel-larraz

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

@@ -50,4 +50,10 @@ public static LogLevel getLevel(String level)
         throw new UnsupportedOperationException("Log " + level + " is not defined");
     }
   }
+
+  @Override
+  public String toString()
+  {
+    return this.value;
+  }
 }

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

@@ -9,7 +9,6 @@
 
 import java.io.IOException;
 import java.math.RoundingMode;
-import java.net.URISyntaxException;
 import java.nio.file.Files;
 import java.nio.file.Paths;
 

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

@@ -24,7 +24,6 @@ public class Node
    */
   private final String json;
 
-  private final JsonElement jsonElement;
   /**
    * Name of the node
    */
@@ -41,7 +40,6 @@ public class Node
   public Node(ModelElementSet modelElementSet, JsonElement jsonElement)
   {
     this.modelElementSet = modelElementSet;
-    this.jsonElement = jsonElement;
     json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement);
     JsonObject jsonObject = jsonElement.getAsJsonObject();
     name = jsonObject.get(Labels.name).getAsString();

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

@@ -41,12 +41,6 @@ public class NodeResult
    */
   private boolean isAnalyzed = false;
 
-  /**
-   * determines whether the current component is printed. The current component may be called recursively
-   * by multiple components, and we need to print it only once.
-   */
-  private boolean isVisited = true;
-
   /**
    * The list of suggestions for this component.
    */

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

@@ -11,9 +11,7 @@
 import com.google.gson.JsonElement;
 
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.List;
-import java.util.Map;
 
 /**
  * PostAnalysis in Kind 2

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

@@ -435,6 +435,10 @@ public void addJsonElement(JsonElement jsonElement) {
           // no properties to check, causing missing analyses before postAnalyses, as well as this object.
         }
       break;
+
+      default:
+        // other object types are not tracked by the result
+        break;
   }
 
   }

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

@@ -8,7 +8,6 @@
 package edu.uiowa.cs.clc.kind2.results;
 
 import java.util.*;
-import java.util.stream.Collector;
 import java.util.stream.Collectors;
 
 /**
@@ -71,7 +70,7 @@ private Suggestion(NodeResult nodeResult, SuggestionType suggestionType)
   /**
    * @return the associated kind2 result.
    */
-  private Result getKind2Result()
+  public Result getKind2Result()
   {
     return nodeResult.getKind2Result();
   }

src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java

@@ -383,11 +383,10 @@ void iml()
   @Test
   void iml2()
   {
-    Result result;
     String json = "[{'objectType': 'kind2Options', 'enabled': ['bmc', 'ind', 'ind2', 'ic3', 'invgents', 'invgenos', 'invgenintos', 'invgenintos'], 'timeout': 5.0, 'bmcMax': 0, 'compositional': True, 'modular': True}, {'objectType': 'log', 'level': 'info', 'source': 'parse', 'value': 'kind2 v1.1.0-488-gcc1e9bd5'}, {'objectType': 'log', 'level': 'error', 'source': 'parse', 'line': 28, 'column': 53, 'value': 'Syntax error'}]";
     try
     {
-      result = Result.analyzeJsonResult(json);
+      Result.analyzeJsonResult(json);
     }
     catch (RuntimeException exception)
     {
@@ -404,8 +403,7 @@ void iml3()
     Result.setPrintingLineNumbersEnabled(true);
     String json = "[{'objectType': 'kind2Options', 'enabled': ['bmc', 'ind', 'ind2', 'ic3', 'invgents', 'invgenos', 'invgenintos', 'invgenintos'], 'timeout': 1.0, 'bmcMax': 0, 'compositional': True, 'modular': True}, {'objectType': 'log', 'level': 'info', 'source': 'parse', 'value': 'kind2 v1.1.0-488-gcc1e9bd5'}, {'objectType': 'analysisStart', 'top': 'agree_dot_UTRC_Explain_Yes_dot_top_level_dot_Impl', 'concrete': [], 'abstract': ['agree_dot_UTRC_Explain_Yes_dot_C', 'agree_dot_UTRC_Explain_Yes_dot_B', 'agree_dot_UTRC_Explain_Yes_dot_A'], 'assumptions': []}, {'objectType': 'property', 'name': 'guarantee[l26c2][1]', 'scope': 'agree_dot_UTRC_Explain_Yes_dot_top_level_dot_Impl', 'line': 26, 'column': 2, 'source': 'Guarantee', 'runtime': {'unit': 'sec', 'timeout': False, 'value': 0.021}, 'k': 0, 'answer': {'source': 'ic3', 'value': 'falsifiable'}, 'counterExample': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_top_level_dot_Impl', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'A_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'A_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 20]]}, {'name': 'B_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'B_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 35]]}], 'subnodes': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_B', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 35]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_A', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 20]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_C', 'streams': [{'name': 'Input1.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input1.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Input2.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 35]]}, {'name': 'Input2.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}]}]}, {'objectType': 'property', 'name': 'agree_dot_UTRC_Explain_Yes_dot_A[l32c19].assume[l64c2][1]', 'scope': 'agree_dot_UTRC_Explain_Yes_dot_A', 'line': 64, 'column': 2, 'source': 'Assumption', 'runtime': {'unit': 'sec', 'timeout': False, 'value': 0.021}, 'k': 0, 'answer': {'source': 'ic3', 'value': 'falsifiable'}, 'counterExample': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_top_level_dot_Impl', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'A_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'A_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 20]]}, {'name': 'B_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'B_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 35]]}], 'subnodes': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_B', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 35]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_A', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 20]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_C', 'streams': [{'name': 'Input1.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input1.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Input2.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 35]]}, {'name': 'Input2.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}]}]}, {'objectType': 'property', 'name': 'agree_dot_UTRC_Explain_Yes_dot_B[l34c19].assume[l45c2][1]', 'scope': 'agree_dot_UTRC_Explain_Yes_dot_B', 'line': 45, 'column': 2, 'source': 'Assumption', 'runtime': {'unit': 'sec', 'timeout': False, 'value': 0.021}, 'k': 0, 'answer': {'source': 'ic3', 'value': 'falsifiable'}, 'counterExample': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_top_level_dot_Impl', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'A_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'A_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 20]]}, {'name': 'B_sub_Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'local', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'B_sub_Output.data', 'type': 'int', 'class': 'local', 'instantValues': [[0, 35]]}], 'subnodes': [{'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_B', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 35]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_A', 'streams': [{'name': 'Input.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 0]]}, {'name': 'Input.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 20]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}, {'blockType': 'node', 'name': 'agree_dot_UTRC_Explain_Yes_dot_C', 'streams': [{'name': 'Input1.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 20]]}, {'name': 'Input1.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Input2.data', 'type': 'int', 'class': 'input', 'instantValues': [[0, 35]]}, {'name': 'Input2.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'input', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}, {'name': 'Output.data', 'type': 'int', 'class': 'output', 'instantValues': [[0, 55]]}, {'name': 'Output.direction', 'type': 'iml_dot_systems_dot_Direction', 'class': 'output', 'instantValues': [[0, 'iml_dot_systems_dot_Direction_dot_IN']]}]}]}]}, {'objectType': 'analysisStop'}]";
 
-    Result result = Result.analyzeJsonResult(json);
-    // System.out.println(result);
+    Result.analyzeJsonResult(json);
   }
 
   @Test