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

Two Questions about (State) Constraints in TLC

From: Hengfeng Wei <hengx...@xxxxxxxxx>
Date: Mon, 28 Jan 2019 17:32:31 -0800 (PST)

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?

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

Thanks.

Regards,

hengxin

Follow-Ups:
- Re: [tlaplus] Two Questions about (State) Constraints in TLC
  - From: Markus Kuppe
- Re: [tlaplus] Two Questions about (State) Constraints in TLC
  - From: Stephan Merz

Prev by Date: Re: [tlaplus] How to define an invariant that describes a sorted sequence
Next by Date: Re: Problem with instance substitutions
Previous by thread: Re: [tlaplus] How to Avoid Attempted to check set membership in a tuple value.
Next by thread: Re: [tlaplus] Two Questions about (State) Constraints in TLC
Index(es):
- Date
- Thread