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

Re: [tlaplus] Toolbox is unresponsive when PrintT is used

On 19.11.2015 15:53, Y2i wrote:
> I'm trying to debug my spec using PrintT.  I understand that model
> checker verifies a huge number of steps, so I'm trying to minimize my
> test scenario and use PrintT sparingly.  Still, toolbox becomes
> unresponsive to the point of being almost unusable.   Even if I manage
> to cancel the model run, switching between tabs takes a lot of time.
>  Even after exiting/killing toolbox and restarting, then switching to
> Model tab still takes a lot of time.  Only after commenting out PrintT
> and re-running the model, or after deleting the model and re-opening the
> spec, the toolbox becomes usable again.  Would it be possible to improve
> this?

Hi Yuri,

I removed the most significant Toolbox bottlenecks in handling large
amounts of TLC output. As a consequence, the Toolbox now limits the
error trace to a tail of a fixed number of states. The value can be
increased in the Toolbox's preferences (see screenshot) if needed.

For really large outputs which remain too large for the Toolbox to
handle (i.e. every state of a billion state model is printed), TLC can
be set to redirect its user output to a dedicated file. To do so, pass
"-userFile aFileName" as a TLC command line argument. Note that Print &
PrintT generally slow down TLC.

Both changes will be available in the next Toolbox release and in the
current nightly build [1].


[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/

Attachment: Preferences.png
Description: PNG image