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]. Cheers Markus [1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/
Attachment:
Preferences.png
Description: PNG image
