Merge pull request #9 from lorchrob/ref-type-realizability

Add support for realizability checks and deadlocking traces
kind2-mc · May 1, 2024 · bb6a278 · bb6a278
2 parents 28d6019 + d644b93
commit bb6a278
Show file tree

Hide file tree

Showing 7 changed files with 172 additions and 16 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
@@ -199,6 +199,23 @@ public void apiDebug(String text) {
     }
   }
 
+  /**
+   * Run Kind on a Lustre program with module options
+   *
+   * @param program Lustre program as text
+   * @param result Place to store results as they come in
+   * @param monitor Used to check for cancellation
+   * @param modules A list of modules to enable
+   * @throws Kind2Exception
+   */
+  public void execute(String program, Result result, IProgressMonitor monitor, List<Module> modules) {
+    for (Module module: modules) {
+      enable(module);
+    }
+
+    execute(program, result, monitor);
+  }
+
   /**
    * Run Kind on a Lustre program
    *

diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Analysis.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Analysis.java
@@ -50,6 +50,18 @@ public class Analysis
    * in file files/S1.json
    */
   private final Map<String, List<Property>> propertiesMap;
+  /**
+   * realizability result in the current analysis.
+   */
+  private RealizabilityResult realizabilityResult = null;
+  /**
+   * Deadlocking trace of current analysis
+   */
+  private String deadlock = null;
+  /**
+   * Context of current analysis
+   */
+  private String context = null;
   /**
    * is the current analysis comes from an exhaustiveness check of the state space covered by the modes of a contract.
    */
@@ -68,33 +80,46 @@ public Analysis(JsonElement jsonElement)
     json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonElement);
 
     this.nodeName = jsonElement.getAsJsonObject().get(Labels.top).getAsString();
+    try {
+      this.context = jsonElement.getAsJsonObject().get(Labels.context).getAsString();
+    } catch (Exception e) {
+    }
     this.abstractNodes = new ArrayList<>();
+    try {
     JsonArray abstractArray = jsonElement.getAsJsonObject().get(Labels.abstractField).getAsJsonArray();
-    for (JsonElement node : abstractArray)
-    {
-      abstractNodes.add(node.getAsString());
+      for (JsonElement node : abstractArray)
+      {
+        abstractNodes.add(node.getAsString());
+      }
+    } catch (Exception e) {
     }
+
     this.concreteNodes = new ArrayList<>();
-    JsonArray concreteArray = jsonElement.getAsJsonObject().get(Labels.concrete).getAsJsonArray();
-    for (JsonElement node : concreteArray)
-    {
-      concreteNodes.add(node.getAsString());
+    try {
+      JsonArray concreteArray = jsonElement.getAsJsonObject().get(Labels.concrete).getAsJsonArray();
+      for (JsonElement node : concreteArray)
+      {
+        concreteNodes.add(node.getAsString());
+      }
+    } catch (Exception e) {
     }
 
     subNodes = new ArrayList<>(abstractNodes);
     subNodes.addAll(concreteNodes);
 
     assumptions = new ArrayList<>();
 
+    try {
     JsonArray assumptionInvariants = jsonElement.getAsJsonObject().get(Labels.assumptions).getAsJsonArray();
-    for (JsonElement invariant : assumptionInvariants)
-    {
-      JsonArray invariantArray = invariant.getAsJsonArray();
-      String nodeName = invariantArray.get(0).getAsString();
-      String number = invariantArray.get(1).getAsString();
-      assumptions.add(new Pair<>(nodeName, number));
+      for (JsonElement invariant : assumptionInvariants)
+      {
+        JsonArray invariantArray = invariant.getAsJsonArray();
+        String nodeName = invariantArray.get(0).getAsString();
+        String number = invariantArray.get(1).getAsString();
+        assumptions.add(new Pair<>(nodeName, number));
+      }
+    } catch (Exception e) {
     }
-
     this.propertiesMap = new HashMap<>();
   }
 
@@ -122,6 +147,36 @@ public void addProperty(Property property)
     }
   }
 
+  public void setRealizabilityResult(RealizabilityResult val) 
+  {
+    this.realizabilityResult = val;
+  }
+
+  public RealizabilityResult getRealizabilityResult() 
+  {
+    return this.realizabilityResult;
+  }
+
+  public void setDeadlock(String val) 
+  {
+    this.deadlock = val;
+  }
+
+  public String getDeadlock() 
+  {
+    return this.deadlock;
+  }
+
+  public void setContext(String val) 
+  {
+    this.context = val;
+  }
+
+  public String getContext() 
+  {
+    return this.context;
+  }
+
   /**
    * @return Kind2 json output for this object
    */
@@ -314,4 +369,4 @@ void setPostAnalysis(PostAnalysis postAnalysis)
       throw new RuntimeException(String.format("Post Analysis is already set for '%1$s'.", nodeName));
     }
   }
-}
+}
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
@@ -34,6 +34,8 @@ public class Labels
   public static final String source = "source";
   public static final String timeout = "timeout";
   public static final String counterExample = "counterExample";
+  public static final String deadlockingTrace = "deadlockingTrace";
+  public static final String context = "context";
   public static final String exampleTrace = "witness";
   public static final String blockType = "blockType";
   public static final String streams = "streams";
@@ -57,6 +59,9 @@ public class Labels
   public static final String ivc = "ivc";
   public static final String ivcComplement = "ivc complement";
   public static final String runtime = "runtime";
+  public static final String result = "result";
+  public static final String realizable = "realizable";
+  public static final String unrealizable = "unrealizable";
   public static final String unit = "unit";
   public static final String nodes = "nodes";
   public static final String elements = "elements";

diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/NodeResult.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/NodeResult.java
@@ -136,6 +136,17 @@ public String printVerificationSummary()
     Set<Property> unreachableProperties = this.getUnreachableProperties();
     printProperties(stringBuilder, unreachableProperties);
 
+    RealizabilityResult realizabilityResult = getLastAnalysis().getRealizabilityResult();
+    if (realizabilityResult != null) {
+      if (realizabilityResult.equals(RealizabilityResult.realizable)) {
+        stringBuilder.append("\nRealizability result: \nRealizable\n");
+      } else if (realizabilityResult.equals(RealizabilityResult.unrealizable)) {
+        stringBuilder.append("\nRealizability result: \nUnrealizable\n");
+      } else {
+        stringBuilder.append("\nRealizability result: \nNone\n");
+      }
+    }
+
     return stringBuilder.toString();
   }
 
@@ -468,4 +479,4 @@ public Set<Property> getUnreachableProperties()
 
     return unreachableProperties;
   }
-}
+}
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
@@ -16,6 +16,8 @@ public enum Object
   log("log"),
   analysisStart("analysisStart"),
   property("property"),
+  realizabilityResult("realizabilityResult"),
+  satisfiabilityCheck("satisfiabilityCheck"),
   analysisStop("analysisStop"),
   postAnalysisStart("postAnalysisStart"),
   postAnalysisEnd("postAnalysisEnd"),
@@ -42,6 +44,10 @@ public static Object getKind2Object(String kind2Object)
         return analysisStart;
       case "property":
         return property;
+      case "realizabilityCheck":
+        return realizabilityResult;
+      case "satisfiabilityCheck":
+        return satisfiabilityCheck;
       case "analysisStop":
         return analysisStop;
       case "postAnalysisStart":

diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java
@@ -0,0 +1,45 @@
+/*
+ * Copyright (c) 2024, Board of Trustees of the University of Iowa
+ * All rights reserved.
+ *
+ * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information.
+ */
+
+package edu.uiowa.cs.clc.kind2.results;
+
+/**
+ * Enum for realizability results.
+ */
+public enum RealizabilityResult
+{
+  realizable("realizable"),
+  unrealizable("unrealizable");
+
+  private final String value;
+
+  RealizabilityResult(String value)
+  {
+    this.value = value;
+  }
+
+  public static RealizabilityResult getRealizabilityResult(String realizabilityResult)
+  {
+    switch (realizabilityResult)
+    {
+      case "Realizable":
+      case "realizable":
+        return realizable;
+      case "Unrealizable":
+      case "unrealizable":
+        return unrealizable;
+      default:
+        throw new UnsupportedOperationException("Realizability result " + realizabilityResult + " is not defined");
+    }
+  }
+
+  @Override
+  public String toString()
+  {
+    return this.value;
+  }
+}
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
@@ -248,6 +248,23 @@ public void initialize(String json) {
         }
       }
 
+      if (kind2Object == Object.realizabilityResult) {
+        if (kind2Analysis != null) {
+          JsonObject 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");
+        }
+      }
+
       if (kind2Object == Object.postAnalysisStart) {
         if (previousAnalysis != null) {
           PostAnalysis postAnalysis = new PostAnalysis(previousAnalysis, jsonElement);