VSCode status panel stuck in computing initial states when using simulation mode

[joshuazh-x]

I'm trying to run model checking on TLA+ spec at https://github.com/joshuazh-x/raft/blob/trace-validation/tla/MCetcdraft.tla using simulation mode. The output shows progresses but the status panel in vscode stuck in computing initial states.

I use TLA+ Nightly extension installed on WSL. VSCode version is 1.85.1.

[joshuazh-x]

The case of the above screenshot uses VSCode command "TLA+: Check model with TLC" with additional options "-fpmem 0.9 -simulate" passed to TLC. Not sure if I did it in the right way for simulation mode.

I notice output from command line "java -XX:+UseParallelGC -cp ./tla2tools.jar:./CommunityModules-deps.jar tlc2.TLC -config ./MCetcdraft.cfg ./MCetcdraft.tla -fpmem 0.9 -simulate" is different from that in the VSCode. Where can I check the effective command line in VSCode?

[lemmy]

IIRC, the extension doesn't log the command-line. You will have to use ps axu.

[joshuazh-x]

I see. The difference of output comes from option -tool which is used in vscode. Such difference is expected and shall not be the cause of this issue.