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

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

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:
   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.)