3 Random Questions

[Eric Lee <ericl...@xxxxxxxxx>]

I've been working with the TLA+ Toolbox for about a month, and I have a couple questions that I cannot find the answers to from browsing the old posts in this group or consulting the various manuals online. Please let me know if this is not the appropriate place to do this.

1. I use the TLA+ Toolbox on Ubuntu 16.04.2, and there is some weird visual artifacts that occur when I quickly scroll in the TLA module editor. If I scroll too fast, the editor seems to lag behind and repeat itself until I stop scrolling. I'm not sure how big of an issue this would be considered, but it would be nice to know if there is a fix for it.

2. I am currently working with the Raft TLA spec, and I was wondering if there is any way I can view the states that are being explored. I've seen something about Print or PrintT in the toolbox, but I was wondering what the best way to examine this is. Also, is there a way to limit the diameter of the state space exploration? I've managed to do this by adding variables myself into the spec, but does the toolbox have something built in?

3. Lastly, what kind of runtimes are normal for testing specifications? In my experience, after reaching diameter 11 or 12, progress slows to a halt. I read that the state exploration grows exponentially with the diameter, and I should test my spec for "as long as my patience would last". Does anyone have any tips for a better workflow? This is probably a dumb question.