[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: TLC: NoSuchElementException on checkpoint restore
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.