On 28.01.19 17:32, Hengfeng Wei wrote:
> Is it possible to impose constraints on the length of the diameter of
> the reachable-state graph in the model checking mode?
a recent TLC commit  introduces this functionality. The commit
message illustrates how to use it.
You can grab Toolbox or TLC nightly builds with the commit from .
tlaplus/commit/ 537725a6bf7b9c84f86d12825da4d2 c7e5e275b0