1. I can't help you on that.
2. The diameter isn't a particular important measure. What you want
to do is limit the size of the state space. To learn the mechanisms
for doing that, see the Model Checking section of the Help. Of
special interest is the State Constraint section of Creating a Model >
Advanced Option Page. The mistake beginners usually make is not to
start by checking very small models (ones with few enough states to
terminate quickly).
The most effective way to limit the number of states is to write a
better spec. The art of specification is to find the simplest, most
abstract spec that captures the essence of your algorithm. For an
example, you might want to look at my specification of Paxos that I
believe is in the examples on git.
When you've got the simplest abstraction that accurately describes the
algorithm, model checking reasonable sized models may still take a lot
of time. One thing you can then do is to check a simpler, less
accurate model whose executions take fewer steps--that is, a spec with
larger atomic actions that describe multiple separate actions of the
original spec. Any error in the simple spec reveals an error in the
original spec. When you're convinced that the system with large steps
is correct, you can then start looking for errors in the more accurate
spec.
3. There's no such thing as "normal". Your experience with diameter
11 or 12 holds only for your particular example. TLC slows down
dramatically when the set of states it's found so far no longer fits
in memory and has to be stored on disk. The solution to this problem
is to find a machine with the largest memory you can. Multiple cores
help too; TLC does multiprocessing on a single machine very
effectively for checking safety. After running smaller models,
engineers will often run TLC for a couple of weeks on a very large
machine.
Leslie
On Tuesday, April 4, 2017 at 6:07:02 PM UTC-7, Eric Lee wrote: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.