Re: [tlaplus] Two Questions about (State) Constraints in TLC

Hi Markus,

I have tried the features you mentioned.

It is really useful.

Looking forward to the new version.

Thanks

Hengxin

On Tuesday, January 29, 2019 at 11:49:07 PM UTC+8, Markus Alexander Kuppe wrote:

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?

Hi Hengxin,

a recent TLC commit [1] introduces this functionality. The commit
message illustrates how to use it.

You can grab Toolbox or TLC nightly builds with the commit from [2].

Thanks
Markus

[1]
https://github.com/tlaplus/tlaplus/commit/537725a6bf7b9c84f86d12825da4d2c7e5e275b0
[2] http://dl.tlapl.us/tlatoolbox/ci/