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

[Stephan Merz <stepha...@xxxxxxxxx>]

Dear Hengfeng Wei,

> On 29 Jan 2019, at 02:32, Hengfeng Wei <hengx...@xxxxxxxxx> wrote:
> 
> Dear all,
> 
> I have two questions about (state) constraints in TLC:
> 
> 1. Suppose I want to check Spec => [ ]Property under the state constraint SC in command line mode.
> How should I specify the state constraint in command line?

the constraint is specified in the configuration file, using a clause of the form

CONSTRAINT SC

> 2. Is it possible to impose constraints on the length of the diameter of the reachable-state graph in the model checking mode?

No, I don't think so. (I presume you would like to stop exploration when the diameter of the partial state graph computed by TLC reaches some threshold value.)

Regards,
Stephan