From 3ea322254974cd39a4dd336fff12b203a6743dd1 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Mon, 20 Mar 2023 15:57:11 -0700
Subject: [PATCH] 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: Markus Alexander Kuppe <github.com@lemmster.de>
---
.../org.lamport.tlatools/test/tlc2/tool/Github798ITest.java | 2 --
.../org.lamport.tlatools/test/tlc2/tool/Github798NTest.java | 2 --
2 files changed, 4 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
index a49d386c7..6dad1288f 100644
--- a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
@@ -41,12 +41,10 @@ public class Github798ITest extends ModelCheckerTestCase {
super("Github798I", new String[] { "-config", "Github798I.tla" }, EC.ExitStatus.SUCCESS);
}
- @Override
protected boolean noGenerateSpec() {
return true;
}
- @Override
protected boolean doDumpTrace() {
return false;
}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java
index dd2a34933..2cb00946c 100644
--- a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java
@@ -41,12 +41,10 @@ public class Github798NTest extends ModelCheckerTestCase {
super("Github798N", new String[] { "-config", "Github798N.tla" }, EC.ExitStatus.SUCCESS);
}
- @Override
protected boolean noGenerateSpec() {
return true;
}
- @Override
protected boolean doDumpTrace() {
return false;
}
--
GitLab