From 5f4c76eafa2aaf874a3ce89a73ddb9f06502c951 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 29 Apr 2024 11:04:45 -0500 Subject: [PATCH 1/4] Support realizability checks --- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 17 ++++ .../uiowa/cs/clc/kind2/results/Analysis.java | 85 +++++++++++++++---- .../uiowa/cs/clc/kind2/results/Labels.java | 5 ++ .../cs/clc/kind2/results/NodeResult.java | 11 ++- .../uiowa/cs/clc/kind2/results/Object.java | 6 ++ .../kind2/results/RealizabilityResult.java | 49 +++++++++++ .../uiowa/cs/clc/kind2/results/Result.java | 17 ++++ 7 files changed, 174 insertions(+), 16 deletions(-) create mode 100644 src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java 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 index 87d6a7f..463e6c9 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -184,6 +184,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 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 index 906f5b9..58365d2 100644 --- 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> propertiesMap; + /** + * realizability result in the current analysis. + */ + private RealizabilityResult realizabilityResult = RealizabilityResult.none; + /** + * Deadlocking trace of current analysis + */ + private String deadlock = null; + /** + * Context of current analysis + */ + private String context = ""; /** * is the current analysis comes from an exhaustiveness check of the state space covered by the modes of a contract. */ @@ -68,17 +80,28 @@ 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); @@ -86,15 +109,17 @@ public Analysis(JsonElement jsonElement) 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)); } } -} +} \ No newline at end of file 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 5e70ef8..d8bf936 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 @@ -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 = "exampleTrace"; 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 index 5e27dc0..0eab880 100644 --- 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,15 @@ public String printVerificationSummary() Set unreachableProperties = this.getUnreachableProperties(); printProperties(stringBuilder, unreachableProperties); + RealizabilityResult realizabilityResult = getLastAnalysis().getRealizabilityResult(); + 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 +477,4 @@ public Set getUnreachableProperties() return unreachableProperties; } -} +} \ No newline at end of file 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 index f44739c..d3a1238 100644 --- 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 "realizabilityResult": + 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 new file mode 100644 index 0000000..a52a7ab --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java @@ -0,0 +1,49 @@ +/* + * 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"), + none("None"); + + 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; + case "None": + case "none": + return none; + default: + throw new UnsupportedOperationException("Realizability result " + realizabilityResult + " is not defined"); + } + } + + @Override + public String toString() + { + return this.value; + } +} \ No newline at end of file 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 index 3f0abe5..1e3069a 100644 --- 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); From 3a12491a8b7bcb228d829444fa9d090332cae5a8 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 29 Apr 2024 12:04:06 -0500 Subject: [PATCH 2/4] Fix case and keyword bugs when parsing Kind 2 json output --- src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java | 2 +- .../edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) 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 index d3a1238..b804975 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Object.java @@ -44,7 +44,7 @@ public static Object getKind2Object(String kind2Object) return analysisStart; case "property": return property; - case "realizabilityResult": + case "realizabilityCheck": return realizabilityResult; case "satisfiabilityCheck": return satisfiabilityCheck; 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 index a52a7ab..59e311f 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java @@ -12,9 +12,9 @@ */ public enum RealizabilityResult { - realizable("Realizable"), - unrealizable("Unrealizable"), - none("None"); + realizable("realizable"), + unrealizable("unrealizable"), + none("none"); private final String value; From 428e6a703e52c3b38e3a55ad205c2a56b6858b56 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 30 Apr 2024 10:41:18 -0500 Subject: [PATCH 3/4] Use null to denote missing values for consistency --- src/main/java/edu/uiowa/cs/clc/kind2/results/Analysis.java | 4 ++-- .../edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java | 6 +----- 2 files changed, 3 insertions(+), 7 deletions(-) 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 index 58365d2..b980878 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Analysis.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Analysis.java @@ -53,7 +53,7 @@ public class Analysis /** * realizability result in the current analysis. */ - private RealizabilityResult realizabilityResult = RealizabilityResult.none; + private RealizabilityResult realizabilityResult = null; /** * Deadlocking trace of current analysis */ @@ -61,7 +61,7 @@ public class Analysis /** * Context of current analysis */ - private String context = ""; + private String context = null; /** * is the current analysis comes from an exhaustiveness check of the state space covered by the modes of a contract. */ 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 index 59e311f..f980045 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/RealizabilityResult.java @@ -13,8 +13,7 @@ public enum RealizabilityResult { realizable("realizable"), - unrealizable("unrealizable"), - none("none"); + unrealizable("unrealizable"); private final String value; @@ -33,9 +32,6 @@ public static RealizabilityResult getRealizabilityResult(String realizabilityRes case "Unrealizable": case "unrealizable": return unrealizable; - case "None": - case "none": - return none; default: throw new UnsupportedOperationException("Realizability result " + realizabilityResult + " is not defined"); } From d644b93cc11c015703ae68166a12c8dede0a7014 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 30 Apr 2024 11:13:41 -0500 Subject: [PATCH 4/4] Add null check for realizabilityResult --- .../edu/uiowa/cs/clc/kind2/results/NodeResult.java | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) 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 index 0eab880..ab40262 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/NodeResult.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/NodeResult.java @@ -137,12 +137,14 @@ public String printVerificationSummary() printProperties(stringBuilder, unreachableProperties); RealizabilityResult realizabilityResult = getLastAnalysis().getRealizabilityResult(); - 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"); + 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();