Skip to content
Snippets Groups Projects
Commit 3ea32225 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

LazyValue can cause TLC to generate too many or too few states.

Remove @Override to compile with older test framework.

Part of Github issue #798
https://github.com/tlaplus/tlaplus/issues/798



[Bug][TLC][Changelog]

Signed-off-by: default avatarMarkus Alexander Kuppe <github.com@lemmster.de>
parent 4fcc4518
No related branches found
No related tags found
No related merge requests found
...@@ -41,12 +41,10 @@ public class Github798ITest extends ModelCheckerTestCase { ...@@ -41,12 +41,10 @@ public class Github798ITest extends ModelCheckerTestCase {
super("Github798I", new String[] { "-config", "Github798I.tla" }, EC.ExitStatus.SUCCESS); super("Github798I", new String[] { "-config", "Github798I.tla" }, EC.ExitStatus.SUCCESS);
} }
@Override
protected boolean noGenerateSpec() { protected boolean noGenerateSpec() {
return true; return true;
} }
@Override
protected boolean doDumpTrace() { protected boolean doDumpTrace() {
return false; return false;
} }
......
...@@ -41,12 +41,10 @@ public class Github798NTest extends ModelCheckerTestCase { ...@@ -41,12 +41,10 @@ public class Github798NTest extends ModelCheckerTestCase {
super("Github798N", new String[] { "-config", "Github798N.tla" }, EC.ExitStatus.SUCCESS); super("Github798N", new String[] { "-config", "Github798N.tla" }, EC.ExitStatus.SUCCESS);
} }
@Override
protected boolean noGenerateSpec() { protected boolean noGenerateSpec() {
return true; return true;
} }
@Override
protected boolean doDumpTrace() { protected boolean doDumpTrace() {
return false; return false;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment