[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Workaround


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.


On 02 Oct 2014, at 11:00, fl <freder...@xxxxxxxxxxx> wrote:

If you can find a short example in which tlapm hangs after it has begun proving obligations, we would appreciate seeing it.
In fact nothing is wrong with tlapm. I just sometimes believe it is able to prove a step but  realize, because
of the time it takes, that I would rather split the goal into simpler ones.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.