diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java index a49d386c730e3ae84b822dbad675cd05d9c0472d..6dad1288fd45581996b2ffb0d18cdf2500080d7d 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 dd2a349339cd2cbb86055c57be4d46129cf2b9bd..2cb00946cc9329cd4975877b47ecd6bc3ecbd94b 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; }