Re: [tlaplus] Re: Some user feedback

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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.

Hi,

for those interested, distributed TLC worker use a technique based on
OSGi's [1] 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.

Markus

[1] http://www.osgi.org/javadoc/r4v43/core/org/osgi/framework/Bundle.html