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

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

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/