Re: [tlaplus] TLC I/O exception

[Tim Rath <tim.a...@xxxxxxxxx>]

Hi Leslie, thanks for the response. TLC had been running for less than a day, but I still would have preferred that it just warn, and keep running (of course, it could not start from a checkpoint after failing as it did). The same spec on a Linux box has made it going on 3 days now, and is still running. I'll let you know if I run into this again - I will still run things on my Windows laptop, though I may consider disabling checkpoints as Chris suggests.

On Monday, February 4, 2013 9:53:49 AM UTC-8, Leslie Lamport 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....@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...@googlegroups.com.
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.