[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].


[2] http://dl.tlapl.us/tlatoolbox/ci/