Incremental

src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java

@@ -9,15 +9,19 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.io.InputStreamReader;
 import java.net.URI;
 import java.util.ArrayList;
 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;
+import edu.uiowa.cs.clc.kind2.results.Result;
 
 /**
  * The primary interface to Kind2.
@@ -334,45 +338,56 @@ 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()));
     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);
+          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());
     } 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 +423,7 @@ public void setOtherOptions(List<String> options) {
 
   public List<String> getOptions() {
     List<String> options = new ArrayList<>();
-    options.add("-json");
+    options.add("-ijson");
     if (logLevel != null) {
       options.add(logLevel.getOption());
     }

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);
+
+}

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
@@ -70,7 +75,7 @@
   /**
    * Kind2 json output.
    */
-  private String json;
+  private JsonArray json;
   /**
    * a list of kind2 logs.
    */
@@ -157,7 +162,7 @@
 
   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;
@@ -289,6 +294,159 @@
     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();
+    }
+    this.json.add(jsonElement); 
+
+      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<String> 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.
    */
@@ -330,7 +488,7 @@
    * @return Kind2 json output.
    */
   public String getJson() {
-    return json;
+    return json.toString();
   }
 
   /**
@@ -409,7 +567,7 @@
   /**
    * Sets the value of printingCounterExamplesEnabled
    *
    * @param value
    */
   public static void setPrintingCounterExamplesEnabled(boolean value) {
     Result.printingCounterExamplesEnabled = value;
@@ -426,7 +584,7 @@
   /**
    * Sets the value of printingUnknownCounterExamplesEnabled
    *
    * @param value
    */
   public static void setPrintingUnknownCounterExamplesEnabled(boolean value) {
     Result.printingUnknownCounterExamplesEnabled = value;
@@ -442,7 +600,7 @@
   /**
    * set the value of printingLineNumbersEnabled
    *
    * @param value
    */
   public static void setPrintingLineNumbersEnabled(boolean value) {
     Result.printingLineNumbersEnabled = value;
@@ -451,7 +609,7 @@
   /**
    * Set the opening symbols for printing lustre names
    *
    * @param symbols
    */
   public static void setOpeningSymbols(String symbols) {
     Result.openingSymbols = symbols;