vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

Pluscal translation errors suppressed if there are existing TLA+ errors

Open hwayne opened this issue 1 year ago • 1 comments

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).

hwayne avatar Sep 18 '24 21:09 hwayne