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

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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