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

*From*: Shuai Mu <msm...@xxxxxxxxx>*Date*: Sat, 25 Feb 2017 18:24:53 -0800 (PST)*References*: <266afbdf-d8ae-4bbc-baa2-5aecfad375ca@googlegroups.com> <4ba552d4-25c3-44ba-998e-0b280abbd855@googlegroups.com> <a9ef43ab-8d4a-48a6-9d08-2b981818194f@googlegroups.com> <abd7d098-3be3-4793-b01e-710b10659d42@googlegroups.com>

Hi Leslie,

Thank you very much for clarification. Then for my case it is just that the search space is too large.

On Saturday, February 25, 2017 at 10:54:11 AM UTC-5, Leslie Lamport wrote:

On Saturday, February 25, 2017 at 10:54:11 AM UTC-5, Leslie Lamport wrote:

Do you mean if I check for liveness, at most only one core will be

utilized? So we should not check any properties in the "model

overview" page to utilize more than 1 core?The "Properties" part of the "What to check?" section of the Model

Overview page is used to specify temporal formulas that can be safety

properties, liveness properties, or a conjunction of the two. The

safety properties TLC can check are invariance ([] Invariant), step

simulation ([][Action]_vars), and a conjunction of these properties.

To check any property, TLC must compute the state graph. It does that

using as many cores as the model specifies. TLC checks for violation

of safety properties while computes the state graph. It checks for

violation of liveness properties, using a single core, after computing

the state graph and periodically while computing it. (I think it

does that about every half hour.)

**References**:**Is it possible to TLA+ (and PlusCal) to check complex models?***From:*Shuai Mu

**Re: Is it possible to TLA+ (and PlusCal) to check complex models?***From:*Hillel Wayne

**Re: Is it possible to TLA+ (and PlusCal) to check complex models?***From:*Shuai Mu

**Re: Is it possible to TLA+ (and PlusCal) to check complex models?***From:*Leslie Lamport

- Prev by Date:
**Re: Is it possible to TLA+ (and PlusCal) to check complex models?** - Next by Date:
**Re: I've been working on a TLA+ guide** - Previous by thread:
**Re: Is it possible to TLA+ (and PlusCal) to check complex models?** - Next by thread:
**Re: [tlaplus] Re: Is it possible to TLA+ (and PlusCal) to check complex models?** - Index(es):