[tlaplus] Re: Trace explorer overload?

["J.D. Meadows" <tr1pl3.d3v@xxxxxxxxx>]

I reduced the size of my input problem down to 100, and again, the invariant is triggered correctly at termination and the last state is explored, but the ensuing error trace dump takes ages and sometimes crashes. It seems it is slowly writing to a file that can grow to hundreds of MB. During this process the user has no idea of what the IDE is doing, nor how much time does it need to finish the file dump.

I'm very frustrated with this part of he tooling, it is not well finished. I've technically simulated large traces but I can't present any proof of it.

I also don't need a full trace dump, maybe just the last state and a few of the previous one would suffice.

As a last resort, I'd like the Toolbox to allow me to skip the trace dump and just println the last state from the spec code.

On Thursday, November 9, 2023 at 1:37:20 AM UTC+1 J.D. Meadows wrote:

I've done a heck of a simulation run with a large input set (500 nodes). To ensure it stops at exactly one behavior I've artificially added an invariant that checks that never all processes are "Done". Otherwise the simulation keeps running (except in case of small n input values, when it stops alone for some reason unknown to me). This trick works and TLC throws an error when the system terminates. The 'Checking mode' form is configured to max 1 trace and max trace length of 1M (I have no idea if this will be enough, but the field is mandatory, so I've put a large value). Profiling is off.

Now the problem is how to inspect the last state. There has to be a terminal state somewhere since the invariant has been violated, and I know it is correct from other runs. But I can't see the terminal state anywhere. The Toolbox trace explorer doesn't show all the states, it stopped at state 191, which upon inspection is not the terminal one. The simulation has generated almost 500 MB of logs, in the form of 4 files (two MC.out files and two MC_TE.out files) in two respective model folders (one is the main, the other has some numbers in the name). I opened them with a text editor and the last state in the files is still not the terminal one, and it looks like the 191th state, so I guess that is what the GUI is showing. 

So I have a couple of questions:

1. Is there any way of recovering the complete trace from any other file?
2. In case I have to run it again, is there any way of preventing the overload and somehow view just the terminal state that caused the error?
   

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9996f90d-5d3a-42be-b136-526e1b08ba99n%40googlegroups.com.