[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Some user feedback
On 23.11.2014 23:42, Leslie Lamport wrote:
>> Time taken to start TLC. I assume most of the cost is due to spawning
>> a new JVM on every invocation, and most JVMs are very slow to start.
> Simon Zambrovski tried to run TLC inside the Toolbox's JVM, but
> failed. He was unable to write the appropriate code to re-initialize
> everything so a single instance of TLC could be run more than once.
> My memory says that he re-initialized everything he could find to
> re-initialize, but it still didn't work.
for those interested, distributed TLC worker use a technique based on
OSGi's  bundle re-installing that makes it possible to reuse the same
VM for multiple TLC model checker invocations. The same technique could
be used here.