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 5099e7f..7209019 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 @@ -110,6 +110,7 @@ public class Kind2Api { private LogLevel logLevel; private String lusMain; private String lusMainType; + private String lusMainConst; private String fakeFilepath; public Kind2Api() { @@ -178,6 +179,7 @@ public Kind2Api() { logLevel = null; lusMain = null; lusMainType = null; + lusMainConst = null; } DebugLogger debug = new DebugLogger(); @@ -418,6 +420,10 @@ public List getOptions() { options.add("--lus_main_type"); options.add(lusMainType); } + if (lusMainConst != null) { + options.add("--lus_main_const"); + options.add(lusMainConst); + } if (smtSolver != null) { options.add("--smt_solver"); options.add(smtSolver.toString()); @@ -1419,16 +1425,27 @@ public void setLusMain(String lusMain) { } /** - * Set the top type declaration in the Lustre input file. + * Designate a type declaration in the Lustre input file as the main + * model element for the analysis *

- * Default: "--%MAIN" annotation in source if any, last node otherwise * - * @param lusMainType the main node + * @param lusMainType the main type */ public void setLusMainType(String lusMainType) { this.lusMainType = lusMainType; } + /** + * Designate a constant declaration in the Lustre input file as the main + * model element for the analysis + *

+ * + * @param lusMainConst the main constant + */ + public void setLusMainConst(String lusMainConst) { + this.lusMainConst = lusMainConst; + } + /** * Set the fake filepath for error messages. * 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 b064821..932d9cb 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 @@ -186,6 +186,7 @@ public void initialize(String json) { astInfo = new TypeDeclInfo(jsonElement); break; case "constDecl": + case "paramDecl": astInfo = new ConstDeclInfo(jsonElement); break; case "node":