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 index abf2ad5..0937d73 100644 --- 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 index bd231bd..ae84125 100644 --- 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 index 32f3096..465bda5 100644 --- 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 index c77c49c..df79519 100644 --- 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()