search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
352 stars 31 forks source link

"Stop model checking" button doesn't work on Windows #345

Open hwayne opened 1 day ago

hwayne commented 1 day ago

Description:

image

I'm running in simulation mode, so TLC should only stop when I click the "stop" link. Clicking it does nothing. This is also true with regular model checking and unbound models.

Steps to reproduce:

  1. Start a spec
  2. Click the "stop" button next to Running

Expectations:

TLC should stop checking. It continues until it finishes (or forever).

Version Information:

FedericoPonzi commented 1 day ago

I'm sorry but I wasn't able to reproduce. I tried on both Windows 11 and Ubuntu, in my laptop when I click on (stop) the state switches from Running to Stopped and I can see the java pid is also gone.

When that button is clicked, internally it calls process.kill('SIGINT'), which causes a graceful termination on Linux while on Windows according to the doc:

On Windows, where POSIX signals do not exist, the signal argument will be ignored, and the process will be killed forcefully and abruptly (similar to'SIGKILL').

I tested in both simulate and normal model checking, and I also tried to wait 3 minutes before stopping and worked every time.