Re: [tlaplus] TLC I/O exception

Hi Tim,

In recent versions of the toolbox, it is possible to disable checkpoints completely.

In the TLC, "Advanced Options" tab, under the "TLC Options" section, put the following in the box marked "TLC command line parameters" (the box is near the bottom of the page; depending on your monitor size, you may need to scroll down to see it):

-checkpoint 0

I always disable checkpoints now. I don't need them when checking models that generate a few states. And for models that check a lot of states, periodic checkpointing adds significant overhead to model-checking, and starting from a checkpoint takes a very long time.

The downside is that you lose the ability to start from a checkpoint if TLC crashes, or if you need to make a minor fix to the spec (that doesn't change the set of states or behaviors). But I've only encountered those situations a couple of times, so this was still a win for me. Your mileage may vary of course.

cheers,

Chris

On Mon, Feb 4, 2013 at 9:53 AM, TLA Plus <tlapl...@xxxxxxxxx> wrote:

As part of the checkpointing procedure, TLC was trying to delete the file MC.st.chkpt and rename MC.st.tmp to MC.st.chkpt. One of those file operations failed. On Windows, this sort of thing tends to happen because the OS for some reason thinks that one of those files is still in use. Please let us know if you can reproduce this problem or if you encounter it again. About all we could to is have TLC give a warning that the checkpoint failed and keep going.

Leslie

On Sat, Feb 2, 2013 at 1:37 PM, Tim Rath <tim.a...@xxxxxxxxx> wrote:

Hi,

while checking a spec, I got the following exception thrown by TLC:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.io.IOException: Trace.commitChkpt: cannot delete C:\Users\rath\Documents\tla\modules\ConfigurationShift.toolbox\shift\13-02-01-18-38-28\MC.st.chkpt

MC.st.chkpt does not exist:

...

02/02/2013 06:38 AM 133,863 998
02/02/2013 06:39 AM 131,924 999
02/01/2013 06:38 PM 0 MC.fp
02/02/2013 12:28 PM 135,386,520 MC.st
02/02/2013 12:28 PM 16 MC.st.tmp
02/02/2013 12:28 PM 113,367 queue.chkpt
02/02/2013 12:13 PM 14,072 vars.chkpt
02/02/2013 12:28 PM 14,072 vars.tmp

So I'm not sure if this is a TLC bug, machine file system problem, or actually a bug in the spec or model that somehow cascaded into this IO error..

The console doesn't appear to have anything interesting in it - I see the error message come through, but that's it.

Anyway, just checking to see if anyone has seen this, or is interested in knowing about it. I'll keep the model on disk state in case anything in there might be useful. Unfortunately I can't share the spec as it is considered IP.

I'm running the same spec on a different machine and os now as well - we'll see if it repeats there.

Thanks,
Tim

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.