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

*From*: Chris Pacejo <cpa...@xxxxxxxxxxxxxxxx>*Date*: Tue, 27 Jun 2017 12:10:41 -0700 (PDT)

I was curious to try out the depth-first search option, but it has left me somewhat confused. The option reads:

-dfid num: run in model checking mode and use depth-first iterative deepening

with initial depth num

but it seems that "num" actually specifies the *maximum* depth. To me, initial depth makes more sense; I would think I'd want to start at a depth I knew ran in reasonable time, and allow the search to deepen until no more states are found. Am I using DFID incorrectly?

Further, the output is somewhat confusing, for example:

Finished computing initial states: 1 states generated, with 1 of them

distinct.

Progress: 2 states generated, 1 distinct states found.

Progress: 3 states generated, 7 distinct states found.

Progress: 4 states generated, 34 distinct states found.

Progress: 5 states generated, 106 distinct states found.

Progress: 6 states generated, 268 distinct states found.

Progress: 7 states generated, 622 distinct states found.

Progress: 8 states generated, 1396 distinct states found.

Progress: 9 states generated, 3061 distinct states found.

Progress: 10 states generated, 6556 distinct states found.

Progress: 11 states generated, 13642 distinct states found.

Progress: 12 states generated, 27508 distinct states found.

Progress: 13 states generated, 53908 distinct states found.

Progress: 14 states generated, 102505 distinct states found.

Progress: 15 states generated, 188476 distinct states found.

Progress: 16 states generated, 331447 distinct states found.

Progress: 17 states generated, 556501 distinct states found.

Progress: 18 states generated, 896551 distinct states found.

Progress: 1300376 states generated, 141961 distinct states found.

Progress: 19 states generated, 1396952 distinct states found.

Progress: 1803044 states generated, 184252 distinct states found.

Progress: 20 states generated, 2112321 distinct states found.

Progress: 2507605 states generated, 238530 distinct states found.

Progress: 21 states generated, 3107405 distinct states found.

Progress: 3504078 states generated, 312881 distinct states found.

4464367 states generated, 386985 distinct states found.

It seems that sometimes the first number is the current depth, and the second number the total # of states, while other times, the first number is the total # of states, and the second number is the # of distinct states. A brief look at the source code does not seem to indicate from where this issue arises.

-dfid num: run in model checking mode and use depth-first iterative deepening

with initial depth num

but it seems that "num" actually specifies the *maximum* depth. To me, initial depth makes more sense; I would think I'd want to start at a depth I knew ran in reasonable time, and allow the search to deepen until no more states are found. Am I using DFID incorrectly?

Further, the output is somewhat confusing, for example:

Finished computing initial states: 1 states generated, with 1 of them

distinct.

Progress: 2 states generated, 1 distinct states found.

Progress: 3 states generated, 7 distinct states found.

Progress: 4 states generated, 34 distinct states found.

Progress: 5 states generated, 106 distinct states found.

Progress: 6 states generated, 268 distinct states found.

Progress: 7 states generated, 622 distinct states found.

Progress: 8 states generated, 1396 distinct states found.

Progress: 9 states generated, 3061 distinct states found.

Progress: 10 states generated, 6556 distinct states found.

Progress: 11 states generated, 13642 distinct states found.

Progress: 12 states generated, 27508 distinct states found.

Progress: 13 states generated, 53908 distinct states found.

Progress: 14 states generated, 102505 distinct states found.

Progress: 15 states generated, 188476 distinct states found.

Progress: 16 states generated, 331447 distinct states found.

Progress: 17 states generated, 556501 distinct states found.

Progress: 18 states generated, 896551 distinct states found.

Progress: 1300376 states generated, 141961 distinct states found.

Progress: 19 states generated, 1396952 distinct states found.

Progress: 1803044 states generated, 184252 distinct states found.

Progress: 20 states generated, 2112321 distinct states found.

Progress: 2507605 states generated, 238530 distinct states found.

Progress: 21 states generated, 3107405 distinct states found.

Progress: 3504078 states generated, 312881 distinct states found.

4464367 states generated, 386985 distinct states found.

It seems that sometimes the first number is the current depth, and the second number the total # of states, while other times, the first number is the total # of states, and the second number is the # of distinct states. A brief look at the source code does not seem to indicate from where this issue arises.

- Prev by Date:
**Re: I've been working on a TLA+ guide** - Next by Date:
**TLA+ Toolbox installation problem** - Previous by thread:
**Re: [tlaplus] How can I check if a variable is stable if once set** - Next by thread:
**TLA+ Toolbox installation problem** - Index(es):