We are going to enhance the Toolbox and the TLC model checker to
enable running TLC on a network of machines. We hope this will
provide a speedup that is linear in the number of machines for dozens
and perhaps hundreds of machines. Because of the variety of networks
that people might use, we cannot make it as easy to use TLC on a
network as on a single machine. To try to make it reasonably easy for
must users, we would like to find out how this will be used.
If you would be likely to use this feature, please let us know how you
would use it. You can either post to this forum or send email to
Leslie Lamport (http://lamport.org) briefly
describing:
- What operating system(s) you will be using.
- The network of computers you will be using, including its bandwidth,
the number of machines and the kinds of machines (how many cores and
how much memory they have). - How the computer running the Toolbox will be connected to the
network running TLC, and if it will be continuously connected
to the network throughout a TLC run. - If possible, the approximate number of distinct states generated
by the models you would like to check.
When run on a network, TLC will check only safety properties, not liveness
properties. (The liveness-checking algorithm cannot easily be parallelized.)