| Hello, by default you get a popup window that allows you to cancel a proof if you realize that you don't want to wait for all backends (and all obligations) to fail, instead of having to kill tlapm from the command line or an OS-level process manager. An analogous popup opens for the TLC model checker. However, the Toolbox does not show this popup window if you choose the option to always run such commands in the background (Preferences -> General -> Always run in background). Moreover, you can interrupt backends individually using the "Stop proving" button in the "Interesting Obligations" pane, although this affects only individual provers for single proof obligations, so it is not a convenient way to abort an entire proof. Stephan On 02 Oct 2014, at 11:00, fl <freder...@xxxxxxxxxxx> wrote:
|