Skip to content

Commit 0d78aeb

Browse files
authored
Constant checking and param support (#20)
* Add noModelElementSet value to enum * Add support for the lus_main_const option * Correct javadoc comments
1 parent 2d73bcb commit 0d78aeb

File tree

2 files changed

+21
-3
lines changed

2 files changed

+21
-3
lines changed

src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,7 @@ public class Kind2Api {
110110
private LogLevel logLevel;
111111
private String lusMain;
112112
private String lusMainType;
113+
private String lusMainConst;
113114
private String fakeFilepath;
114115

115116
public Kind2Api() {
@@ -178,6 +179,7 @@ public Kind2Api() {
178179
logLevel = null;
179180
lusMain = null;
180181
lusMainType = null;
182+
lusMainConst = null;
181183
}
182184

183185
DebugLogger debug = new DebugLogger();
@@ -418,6 +420,10 @@ public List<String> getOptions() {
418420
options.add("--lus_main_type");
419421
options.add(lusMainType);
420422
}
423+
if (lusMainConst != null) {
424+
options.add("--lus_main_const");
425+
options.add(lusMainConst);
426+
}
421427
if (smtSolver != null) {
422428
options.add("--smt_solver");
423429
options.add(smtSolver.toString());
@@ -1419,16 +1425,27 @@ public void setLusMain(String lusMain) {
14191425
}
14201426

14211427
/**
1422-
* Set the top type declaration in the Lustre input file.
1428+
* Designate a type declaration in the Lustre input file as the main
1429+
* model element for the analysis
14231430
* <p>
1424-
* Default: "--%MAIN" annotation in source if any, last node otherwise
14251431
*
1426-
* @param lusMainType the main node
1432+
* @param lusMainType the main type
14271433
*/
14281434
public void setLusMainType(String lusMainType) {
14291435
this.lusMainType = lusMainType;
14301436
}
14311437

1438+
/**
1439+
* Designate a constant declaration in the Lustre input file as the main
1440+
* model element for the analysis
1441+
* <p>
1442+
*
1443+
* @param lusMainConst the main constant
1444+
*/
1445+
public void setLusMainConst(String lusMainConst) {
1446+
this.lusMainConst = lusMainConst;
1447+
}
1448+
14321449
/**
14331450
* Set the fake filepath for error messages.
14341451
*

src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,7 @@ public void initialize(String json) {
186186
astInfo = new TypeDeclInfo(jsonElement);
187187
break;
188188
case "constDecl":
189+
case "paramDecl":
189190
astInfo = new ConstDeclInfo(jsonElement);
190191
break;
191192
case "node":

0 commit comments

Comments
 (0)