search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Getting `unrecognized option: -noTE` when running TLC #273

Closed ele7ija closed 2 years ago

ele7ija commented 2 years ago

Running vscode-tlaplus v1.5.4.

When I try to run the TLA+: Check model with TLC, output tab shows the following TLC logs:

/usr/lib/jvm/java-11-temurin//bin/java -XX:+UseParallelGC -cp /home/bp/.vscode-oss/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar tlc2.TLC BlockingQueue.tla -tool -modelcheck -coverage 1 -config BlockingQueue.cfg -deadlock -noTE

TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Error: unrecognized option: -noTE
Usage: java tlc2.TLC [-option] inputfile

I failed to find the setting to remove the -noTE option which I cannot even find listed in output of java -XX:+UseParallelGC -cp /home/bp/.vscode-oss/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar tlc2.TLC -help so am blocked.

ele7ija commented 2 years ago

Okay, solved it, weirdly it seems that tlaplus.tlc.modelChecker.options was edited with value -deadlock -noTE. Is this the default value?

ele7ija commented 2 years ago

So the final RCA is that I cloned https://github.com/lemmy/BlockingQueue repo without noticing the custom settings in .vscode folder.

lemmy commented 2 years ago

@ele7ija My BlockingQueue repo installs a nightly build of the TLA+ VSCode extension, which bundles a newer version of TLC that supports the -noTE parameter. If you encounter other problems, consider switching to nightly.