[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC I/O exception
- From: TLA Plus <tlapl...@xxxxxxxxx>
- Date: Mon, 4 Feb 2013 09:53:49 -0800
- References: <firstname.lastname@example.org>
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.
On Sat, Feb 2, 2013 at 1:37 PM, Tim Rath <tim.a...@xxxxxxxxx>
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.
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.