vscode-tlaplus
vscode-tlaplus copied to clipboard
Pluscal translation errors suppressed if there are existing TLA+ errors
Spec:
---- MODULE PlusCal ----
EXTENDS TLC
(*--algorithm sample_computation
variables x = 0;
begin
print(x);
x = 1;
end algorithm;*)
\* BEGIN TRANSLATION
\* END TRANSLATION
Foo == x > 0
====
Running Parse Module gives the error "Unknown Operator: x" in Foo. Translating the PlusCal should fix this error, but translation fails silently. Commenting out the Foo operator provides the translation error, which is that x = 1; is not valid PlusCal. So the error with Foo (in the TLA+) is suppressing the error with x = 1; (in the PlusCal).