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

[david415]

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

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

[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


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