Skip to content

Commit

Permalink
Hey Markus, this is why you run tests locally first!
Browse files Browse the repository at this point in the history 
see f1cf514

[Bug][TLC]
  • Loading branch information
@lemmy
lemmy committed Aug 5, 2020
1 parent f1cf514 commit d11e08d
Show file tree
Hide file tree
Showing 4 changed files with 88 additions and 52 deletions.
3 changes: 2 additions & 1 deletion tlatools/org.lamport.tlatools/src/pcal/trans.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -843,7 +843,8 @@ else if (ch == '*' && ch2 == ')') {
return null ;
} ;

output.add((ecLine + 1), (PCAL_TRANSLATION_COMMENT_LINE_PREFIX + " " + String.format(Validator.CHECKSUM_TEMPLATE, "ffffffff")));
output.add((ecLine + 1), (PCAL_TRANSLATION_COMMENT_LINE_PREFIX + " "
+ String.format(Validator.CHECKSUM_TEMPLATE, "ffffffff", "ffffffff")));
untabInputVec.insertElementAt(PCAL_TRANSLATION_COMMENT_LINE_PREFIX, (ecLine + 1));
output.add((ecLine + 2), (TLA_TRANSLATION_COMMENT_LINE_PREFIX + " "));
untabInputVec.insertElementAt(TLA_TRANSLATION_COMMENT_LINE_PREFIX, (ecLine + 2));
Expand Down
14 changes: 7 additions & 7 deletions tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1031,8 +1031,8 @@ private void validateParseUnit(final ParseUnit parseUnit) {
TLC called: By default, a warning should be raised. It should be considered
the same as Case 2. */
ToolIO.out.println(String.format(
"!! WARNING: The PlusCal algorithm and its TLA+ translation have changed in the "
+ "module %s since the last translation was performed. Replace equality with inequality signs on the BEGIN and END TRANSLATION lines to disable this warning.",
"!! WARNING: The PlusCal algorithm and its TLA+ translation in "
+ "module %s filename since the last translation.",
parseUnit.getName()));
} else if (results.contains(ValidationResult.TLA_DIVERGENCE_EXISTS)) {
/* The algorithm hash is valid and the translation hash is invalid.
Expand All @@ -1045,18 +1045,18 @@ translator. To handle case (1), I suggest the default should be to run
TLC but raise a transient window with a warning that is easily ignored.
For case (2), it should be possible to put something in a translation
comment to disable the warning. */
ToolIO.out.println(String.format("!! WARNING: The TLA+ translation has changed in the "
+ "module %s since the last translation was performed. Replace equality with inequality sign on the END TRANSLATION line to disable this warning.", parseUnit.getName()));
ToolIO.out.println(String.format("!! WARNING: The TLA+ translation in "
+ "module %s has changed since its last translation.", parseUnit.getName()));
} else if (results.contains(ValidationResult.PCAL_DIVERGENCE_EXISTS)) {
/* The algorithm hash is invalid and the translation hash is valid.
TLC called: By default, a warning should be generated. I see little reason
for not generating the warning. So, it doesn't matter if its inconvenient
to turn off the warning, but turning it off should affect only the current
spec; and it should be easy to turn back on. */
ToolIO.out.println(String.format("!! WARNING: The PlusCal algorithm has changed in the "
+ "module %s since the last translation was performed. Replace equality with inequality sign on the BEGIN TRANSLATION line to disable this warning.", parseUnit.getName()));
ToolIO.out.println(String.format("!! WARNING: The PlusCal algorithm in "
+ "module %s has changed since its last translation.", parseUnit.getName()));
} else if (results.contains(ValidationResult.ERROR_ENCOUNTERED)) {
ToolIO.err.println("A Java problem was encountered attempting to validate the specification for "
ToolIO.err.println("A unexpected problem was encountered attempting to validate the specification for "
+ parseUnit.getName());
}
} catch (final IOException e) {
Expand Down
115 changes: 71 additions & 44 deletions tlatools/org.lamport.tlatools/test/pcal/DivergenceTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,12 @@ public void divergenceTest00() throws IOException {
"\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "Semantic processing of module " + filename);
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertNoSubstring("!! WARNING " + filename);
}

@Test
Expand All @@ -85,7 +90,7 @@ public void divergenceTest01() throws IOException {
"begin\n" +
" skip;\n" +
"end algorithm; *)\n" +
"\\* BEGIN TRANSLATION - the hash of the PCal code: PCal-6d2bf9f0e5d0cc207316a004ca8a0713\n" +
"\\* BEGIN TRANSLATION (chksum(PCal) \\in STRING /\\ chksum(TLA+) \\in STRING)\n" +
"VARIABLE pc\n" +
"\n" +
"vars == << pc >>\n" +
Expand All @@ -106,9 +111,14 @@ public void divergenceTest01() throws IOException {
"\n" +
"Termination == <>(pc = \"Done\")\n" +
"\n" +
"\\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-c42acd1a2a013bcd259342cfe120880f\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "Semantic processing of module " + filename);
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertNoSubstring("!! WARNING " + filename);
}

@Test
Expand All @@ -122,7 +132,7 @@ public void divergenceTest02() throws IOException {
"begin\n" +
" print \"msg\";\n" + // PlusCal diverged
"end algorithm; *)\n" +
"\\* BEGIN TRANSLATION - the hash of the PCal code: PCal-6d2bf9f0e5d0cc207316a004ca8a0713\n" +
"\\* BEGIN TRANSLATION (chksum(PCal) = \"4860ac97\" /\\ chksum(TLA+) = \"af3d9146\")\n" +
"VARIABLE pc\n" +
"\n" +
"vars == << pc >>\n" +
Expand All @@ -143,10 +153,16 @@ public void divergenceTest02() throws IOException {
"\n" +
"Termination == <>(pc = \"Done\")\n" +
"\n" +
"\\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-c42acd1a2a013bcd259342cfe120880f\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "!! WARNING: Either the PlusCal or its TLA+ translation has changed in the specification for "
+ filename + " since the last time translation was performed.");
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertSubstring(String.format(
"!! WARNING: The PlusCal algorithm in module %s has changed since its last translation.",
filename));
}

@Test
Expand All @@ -160,7 +176,7 @@ public void divergenceTest03() throws IOException {
"begin\n" +
" skip;\n" +
"end algorithm; *)\n" +
"\\* BEGIN TRANSLATION - the hash of the PCal code: PCal-6d2bf9f0e5d0cc207316a004ca8a0713\n" +
"\\* BEGIN TRANSLATION (checksum(PlusCal) = \"4860ac97\" /\\ ChkSum(tla+) = \"af3d9146\")\n" +
"VARIABLE pc\n" +
"\n" +
"vars == << pc >>\n" +
Expand All @@ -180,10 +196,16 @@ public void divergenceTest03() throws IOException {
"\n" +
"Termination == <>(pc = \"Done\")\n" +
"\n" +
"\\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-c42acd1a2a013bcd259342cfe120880f\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "!! WARNING: Either the PlusCal or its TLA+ translation has changed in the specification for "
+ filename + " since the last time translation was performed.");
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertSubstring(String.format(
"!! WARNING: The TLA+ translation in module %s has changed since its last translation.",
filename));
}

@Test
Expand All @@ -197,7 +219,7 @@ public void divergenceTest04() throws IOException {
"begin\n" +
" print \"msg\";\n" + // PlusCal diverged
"end algorithm; *)\n" +
"\\* BEGIN TRANSLATION - the hash of the PCal code: PCal-6d2bf9f0e5d0cc207316a004ca8a0713\n" +
"\\* BEGIN TRANSLATION (checksum(PlusCal) = \"4860ac97\" /\\ ChkSum(tla+) = \"af3d9146\") \n" +
"VARIABLE pc\n" +
"\n" +
"vars == << pc >>\n" +
Expand All @@ -217,40 +239,29 @@ public void divergenceTest04() throws IOException {
"\n" +
"Termination == <>(pc = \"Done\")\n" +
"\n" +
"\\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-c42acd1a2a013bcd259342cfe120880f\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "!! WARNING: Either the PlusCal or its TLA+ translation has changed in the specification for "
+ filename + " since the last time translation was performed.");
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertSubstring(String.format(
"!! WARNING: The PlusCal algorithm and its TLA+ translation in module %s filename since the last translation.",
filename));
}

@Test
public void divergenceTest05() throws IOException {
final String filename = "divergenceTest05" + System.currentTimeMillis();
final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
"---- MODULE " + filename + " ----\n" +
"\n" +
"(*\n" +
"--algorithm a\n" +
"begin\n" +
" skip;\n" +
"end algorithm; *)\n" +
"\n=========================");
test(filename, absolutePath, "PlusCal was found in the specification for "+ filename +" but no TLA+ translation could be found.");
}

@Test
@Ignore
public void divergenceTest06() throws IOException {
final String filename = "divergenceTest06" + System.currentTimeMillis();
final String filename = "divergenceTest04" + System.currentTimeMillis();
final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
"---- MODULE " + filename + " ----\n" +
"\n" +
"(*\n" +
"--algorithm a\n" +
"begin\n" +
" skip;\n" +
" print \"msg\";\n" + // PlusCal diverged
"end algorithm; *)\n" +
"\\* BEGIN TRANSLATION\n" +
"\\* BEGIN TRANSLATION (checksum(PlusCal) \\in STRING /\\ ChkSum(tla+) \\in STRING) \n" +
"VARIABLE pc\n" +
"\n" +
"vars == << pc >>\n" +
Expand All @@ -264,25 +275,41 @@ public void divergenceTest06() throws IOException {
"(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
"Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
"\n" +
"Next == Lbl_1\n" + // TLA+ diverged, but no hash.
"Next == Lbl_1\n" + // TLA+ diverged.
"\n" +
"Spec == Init /\\ [][Next]_vars\n" +
"\n" +
"Termination == <>(pc = \"Done\")\n" +
"\n" +
"\\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-c42acd1a2a013bcd259342cfe120880f\n" +
"\\* END TRANSLATION\n" +
"\n=========================");
test(filename, absolutePath, "!! WARNING: Either the PlusCal or its TLA+ translation has changed in the specification for "
+ filename + " since the last time translation was performed.");
}

private void test(final String filename, final String absolutePath, final String expected) {
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring(expected);
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertNoSubstring(String.format(
"!! WARNING:",
filename));
}

@Test
public void divergenceTest06() throws IOException {
final String filename = "divergenceTest05" + System.currentTimeMillis();
final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
"---- MODULE " + filename + " ----\n" +
"\n" +
"(*\n" +
"--algorithm a\n" +
"begin\n" +
" skip;\n" +
"end algorithm; *)\n" +
"\n=========================");
// Parse with SANY and check for errors (collects parse errors into ToolIO.out)
final TestPrintStream testPrintStream = new TestPrintStream();
ToolIO.out = testPrintStream;
SANY.SANYmain(new String[] { absolutePath });
testPrintStream.assertSubstring("Semantic processing of module " + filename);
testPrintStream.assertNoSubstring("!! WARNING " + filename);
}
}
8 changes: 8 additions & 0 deletions tlatools/org.lamport.tlatools/test/util/TestPrintStream.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,4 +68,12 @@ public void assertSubstring(String substring) {
}
fail("Substring not found");
}

public void assertNoSubstring(String substring) {
for (String string : strings) {
if (string.contains(substring)) {
fail("Substring not found");
}
}
}
}

0 comments on commit d11e08d

Please sign in to comment.