Re: [tlaplus] Re: TLC: NoSuchElementException on checkpoint restore

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

On 04.04.2017 17:09, evgeniy....@xxxxxxxxx wrote:
> After recovering from checkpoint I have a very weird messages displayed periodically:
> tlc RAPlus.tla -config RAPlus.cfg -deadlock -metadir /run/media/MC -checkpoint 30 -recover /run/media/MC/17-04-03-13-54-53
> TLC2 Version 2.09 of 28 January 2016
> Running in Model-Checking mode with 3 workers.
> Parsing file RAPlus.tla
> Parsing file /home/sh/tla2tools/tla/tla2sany/StandardModules/Naturals.tla
> Parsing file /home/sh/tla2tools/tla/tla2sany/StandardModules/Sequences.tla
> Parsing file /home/sh/tla2tools/tla/tla2sany/StandardModules/TLC.tla
> Parsing file /home/sh/tla2tools/tla/tla2sany/StandardModules/FiniteSets.tla
> Semantic processing of module Naturals
> Semantic processing of module Sequences
> Semantic processing of module TLC
> Semantic processing of module FiniteSets
> Semantic processing of module RAPlus
> Starting... (2017-04-04 18:04:14)
> Implied-temporal checking--satisfiability problem has 21 branches.
> Starting recovery from checkpoint /run/media/sh/MC/17-04-03-13-54-53/
> AAAAAA
> AAAAAA
> AAAAAA
> AAAAAA
> 
> and so on.
> 
> My model has nothing to do with that "AAAAAA" messages. I have not saw such messages before.
>
> [...]
>
> Some time later I got this message:
> 
> Error: Java ran out of memory.  Running Java with a larger memory allocation
> pool (heap) may fix this.  But it won't help if some state has an enormous
> number of successor states, or if TLC must compute the value of a huge set.
> Finished in 04min 10s at (2017-04-04 18:08:25)
> 
> This is strange because I ran TLC with the same parameters for virtual machine memory 
> as before. 


Hi Evgeniy,

the "AAAAAA" messages are obviously bogus but anyway harmless. My guess
is, that the corresponding print statement in the code is a leftover
from a debugging session.
The reason why TLC shows several messages is, because your liveness
properties have been split into 21 branches and TLC recovers a graph for
each one them.

With regards to the out of memory error, are you saying that you only
get the error if you recover from a checkpoint but don't get it, if you
run the exact same model (same parameters, safety & liveness properties,
...) without recovery? If yes, can you make your checkpoint data and
spec & model (privately) available to me?

By the way, when did you download the Toolbox? The version TLC reports
indicates that you are running a nightly/CI build.

Cheers
Markus