Re: Multi-threaded TLC Simulation Mode

[William Schultz <wjs...@xxxxxxxxxxx>]

Thanks Markus. Running multiple TLC processes with different seeds is pretty easy to do, I just wanted to verify the behavior I was seeing. I will open a Github issue as well.

On Saturday, February 24, 2018 at 12:03:18 PM UTC-5, William Schultz wrote:

I am trying to check a model with TLC using the following parameters (the specific spec isn't really important):

java tlc2.TLC -simulate -depth 20 -cleanup -gzip -workers 12 -metadir /hdd/tlc_states_1 -config MC.cfg MC.tla

When I run TLC the CPU utilization looks suspiciously low (my machine has 12 cores). Here is a a snapshot from htop while TLC was running:

Does simulation mode not run in a multi-threaded mode by default? One alternative I imagine is to just run multiple TLC processes in simulation mode, each with a different random seed, which would probably achieve the same result. Just wondering if this is a known/expected behavior.

Thanks,

Will