Merge pull request #10 from lorchrob/candidate-props

Support candidate property type
kind2-mc · May 6, 2024 · c35ca3d · c35ca3d
2 parents 25b7e75 + 4a17683
commit c35ca3d
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 1 deletion.
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
@@ -32,6 +32,7 @@ public class Labels
   public static final String answer = "answer";
   public static final String value = "value";
   public static final String source = "source";
+  public static final String isCandidate = "isCandidate";
   public static final String timeout = "timeout";
   public static final String counterExample = "counterExample";
   public static final String deadlockingTrace = "deadlockingTrace";

diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Property.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Property.java
@@ -61,6 +61,10 @@ public class Property
    * NonVacuityCheck if it comes from a non-vacuity check.
    */
   private final PropertyType source;
+   /**
+   * True iff the property is a candidate property
+   */
+  private final Boolean isCandidate;
   /**
    * The source of the answer, and the result value of the check.
    * The result can be valid, falsifiable, unknown, reachable, or unreachable
@@ -103,6 +107,11 @@ public Property(Analysis analysis, JsonElement jsonElement)
     line = jsonObject.get(Labels.line).getAsString();
     column = jsonObject.get(Labels.column).getAsString();
     source = PropertyType.getPropertyType(jsonObject.get(Labels.source).getAsString());
+    if (jsonObject.has(Labels.isCandidate)) {
+      isCandidate = jsonObject.get(Labels.isCandidate).getAsBoolean();
+    } else {
+      isCandidate = null;
+    }
     JsonElement answerJsonObject = jsonObject.get(Labels.answer);
     answer = Answer.getAnswer(answerJsonObject.getAsJsonObject().get(Labels.value).getAsString());
     JsonElement counterExampleElement = jsonObject.get(Labels.counterExample);
@@ -198,6 +207,11 @@ public PropertyType getSource()
     return source;
   }
 
+  public Boolean getIsCandidate()
+  {
+    return isCandidate;
+  }
+
   public CounterExample getCounterExample()
   {
     return counterExample;

diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/PropertyType.java
@@ -53,7 +53,7 @@ public static PropertyType getPropertyType(String propertyType)
       case "nonVacuityCheck":
         return nonVacuityCheck;
       default:
-        throw new UnsupportedOperationException("Property type " + propertyType + " is not defined");
+        throw new UnsupportedOperationException("Property type " + propertyType + " is not supported");
     }
   }
 

diff --git a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java
@@ -30,6 +30,23 @@ void reset()
     Result.setClosingSymbols("");
   }
 
+  @Test
+  void candidateProps()
+  {
+    String json = "[{'objectType' : 'log','level' : 'info','source' : 'parse','value' : 'kind2 v2.1.0-226-g2e70bac'},{'objectType' : 'kind2Options','enabled' :[  ],'timeout' : 0.000000,'bmcMax' : 0,'compositional' : false,'modular' : false},{'objectType' : 'analysisStart','top' : 'N','concrete' : [],'abstract' : [],'assumptions' : []},{'objectType' : 'property','name' : 'InvProp[l5c4]','source' : 'PropAnnot','file' : './examples/bug.lus','line' : 5,'column' : 4,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.060},'k' : 0,'answer' : {'source' : 'ic3qe', 'value' : 'falsifiable'},'counterExample' :[  {    'blockType' : 'node',    'name' : 'N',    'streams' :    [      {        'name' : 'x',        'type' : 'subrange',        'typeInfo' :        {          'min' : 0,          'max' : 5        },        'class' : 'input',        'instantValues' :        [          [0, 5]        ]      },      {        'name' : 'y',        'type' : 'int',        'class' : 'output',        'instantValues' :        [          [0, 6]        ]      }    ]  }]},{'objectType' : 'property','name' : '((1 <= y) and (y <= 6))','source' : 'Generated','isCandidate': true,'file' : './examples/bug.lus','line' : 1,'column' : 44,'runtime' : {'unit' : 'sec', 'timeout' : false, 'value' : 0.060},'answer' : {'source' : 'ic3qe', 'value' : 'valid'}},{'objectType' : 'analysisStop'}]";
+
+    Boolean result = 
+    Result.analyzeJsonResult(json)
+      .getRoot()
+      .getAnalyses()
+      .get(0)
+      .getProperties()
+      .get(1)
+      .getIsCandidate();
+
+    assert(result);
+  }
+
 
   @Test
   void suggestion1()