Check model with TLC is a no-op if there is no PlusCal in the file

[david415]

Dear vscode-tlaplus maintainer,

There seems to be a bug where the TLA+ plugin does not check the model unless the model contains PlusCal. In other words, for pure TLA+ files it does not work.

My apologies if this is a duplicate of another bug. I did some due diligence but may have overlooked something.

Sincerely, David

[david415]

Here's a minimal TLA+ spec that demonstrates this bug, at least on my laptop it does:

---------------------------- MODULE trafficlight ----------------------------

EXTENDS Integers, TLC

VARIABLES red, yellow, green

vars == <<red, yellow, green>>

Init == /\ red = 1
        /\ yellow = 0
        /\ green = 0

Switch == /\ red = 1
          /\ red' = 0
          /\ green' = 1
          /\ yellow' = 0
       \/ /\ green = 1
          /\ green' = 0
          /\ yellow' = 1
          /\ red' = 0
       \/ /\ yellow = 1
          /\ yellow' = 0
          /\ red' = 1
          /\ green' = 0
          
Next == Switch          

Spec == Init /\ [][Next]_vars /\ SF_vars(Next)

TypeOK == /\ red \in {0,1}
          /\ green \in {0,1}
          /\ yellow \in {0,1} 

OneLightOnly == red + yellow + green = 1


=============================================================================

[lemmy]

The extension currently does not automatically generate a stub TLC config file for TLA+ specifications. In my opinion, the autogenerated config for PlusCal specifications is generally not useful unless it is manually corrected and completed. Therefore, I am leaning towards removing the automatic generation of a config stub in order to maintain consistency.