[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC unexpected exception
- From: tlaplus-google-group@xxxxxxxxxxx
- Date: Tue, 22 Feb 2022 10:53:31 -0800
- Ironport-data: A9a23:tdawMa4AR2+bLotVUhapDAxRtMnCchMFZxGqfqrLsTDasY5as4F+v jQfDTzSbvuCMzfxft50Pork9B4GvMXdzN9lSlFlrHxkZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UYYoAwgpLeNeYH5JZSlLxqhp0uaEvfDjW1nX4 Ymo+ZWFULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 Mdvjo2ZWCoCBLWPhcgjSD5EGAUhHZQTrdcrIVDn2SCS50jPcn+p3PA3SU9rbcsX/eF4BWwI/ vsdQNwPRkrb1qTmnfTiELkq25RLwMrDZOvzvll8yTjBCes9AprFSI/hxe1g8wcctulnJ9z5R +FDUhtGSTv5TjdjZnouLbMWk+CviX3yfCdftUqO46Ew5gA/ySQvjum1YISLEjCMbelWxBqa9 myfw1TCPSsTZN6l8CW3tX3504cjmguiAN5IfFGizdZmgUaY23cIIAESXB2+uuP8i0ikWtsZK koO+yNoo7JayaCwZtz0Xhn9v3vd+xBBC5xfFOo17AzLwa3Ri+qEOoQaZixjU80PpeIdfyRpy 3O3hPT1DhgwkITAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3E6K8FItvJCFaGu 3cAlo6V6+Vm4XCxeM6lH75l8FKBva7t3NjgbbhHQ8lJG9OFpifLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp2kPS+RY69DquLP7Kih6SdkifXrEmCgmbAjwjQfLQEzMnTx L/HK5/3VS9CYUiZ5GPuGLxNuVPU+szO7TqLGcqTI+WP3r2Za3qYIYrpw3PfBt3VGJis+V2Lm /4Gbpvi40gBDYXWP3eGmaZOfQFiBSVqWfje9p0HHsbdeVAOMD96W5fsLUYJJ+SJaYwIzbmYl px8M2cDoGfCaYrvc1vSMSk7MOu1NXu9xFpiVRER0Z+T8yBLSe6SAG03LfPbpJErq75uy+BaV f4Ad5nSC/hDUG2ZqTsaapb5oYN4cwmznkSFOC/8OGozeJtpRgro/N74f1q/r3JXVXXp6sZu8 ae90g77QIYYQ1gwBsjhbv/ynUi6umIQmb4vUkaReotTdUzg/ZJEMSv0ivNrccgAJQ+an2me2 gOTGgsVv6/BrtZtotXOgKmFqaavEvd/RxYLQTOEsOzubSSDpzit245NVuqMbAvxbmKs9fXwf /hRwtH9LOYDwARAvb16Hus51qk5/dbu++JXwwk9RyfLYl2nB6laL2GCzNVIsqERlLZVtRHvB BCA/d5VPbiGIsT4CEVXLw0gN7zR2fYRkzjUzPI0PESrtHQspeHYDxpfb0uWlShQDLppK4d5k +0vj8gbtl6kgR0wP9fa0y1Z+jjeLnEEVKl75JgWDJWx0Vguw1BGJIPZU2r4vcHJZNJLPU0nZ DSTgfOa1bhbw0PDdVs1FGTMjbUB38VQ4EgSwQ9QPUmNl/rEmuQzgE9b/wMxQ1kH1R5Aye9yZ jVmOhwnIaSV4wpun9VJW2zwSQhNCAfHqh70wloNiGqLQE6vWWjAI3c6JP6WuUUQ9WtTc3sAo +HJlDu7AWmzJZ+ywy0pRER+oObiR9FZ+QrFl8SqEN6CAoEhJzHih/b2N2YPrhLmB+I3hVHG9 Lkxp78rNvOkOH5CubA/Bqmbya8UFEKOKltETKwz56gOB2zdJGy/1DTSeUm9dtkRdq7K7VOgE J4pYc1VUAmmz2CBqTcUAaNKKLhx2/Ez48caPa/vLHYCrqDYtSdjq5nK9yLziWJ3Ec9il90xd tHYez6YSDfCgHJVnyrSqZABNDfoJ9YDYwL40aa+9+BQT8APt+RlcEcT1LqoviXKbFE2oUrM5 A6TNbXLy+FCyJh3m9e+GKt0AQjpe8j4U/6F8VzuvtlDBT8V3Rwia+/IRpjb0wVq0X85Xt12k fGStYey0h6V+rkxVG/dlt+KEKwhCQBemgZIGpqfEZWYtXLqtAzQD98r9Ge/JphEn8la+9G8A QC/baNcsPYLDsxFyiQ9hzd2Sn4g5meeUkskjSy6qPuIBxcH1hHfN5Ws8nqBgaS3sMMXE8WWN zIYcMpCKjyVQEqgyfPE6zxb70dEHWLe
- Ironport-hdrordr: A9a23:D84Dd64doTdx3r1TbgPXwZCBI+orL9Y04lQ7vn2ZFiY4A7Slfp GV8YVj6farslxhPk3I/urwRpVoIEmsiqKdhLN/AV7MZniUhILFFvAf0WKm+UyVJ8URntQtlZ uJXcBFeZzN5BtB/IvHCDDRKadv/DD/ytHquQ9qpE0dBz2CFZsQmDuRezzrY3GeHzM2TqbRfa D0jqE3w0vaCAkqg9yAdwM4tqr41q/2ffTdEFY77jEciTVm5gnYmIISfSLoqyv3klt0sNIfGK v+8zARJJ/MjxkKoSWsmFM7I64m++cIx7B4dYWxYjh/EESbtu9gXvUCKtq/lQFwmvim7BIBkd XHoRsse+R1r13LeH2tyCGdlzXd7A==
- Ironport-sdr: Qb/Ckf/5cRSpixPI9QmPRfeDFpDX66KX16AkcLLLUv8Zg04LGKeSDPLoif/VgR2CUgmZV5ecPX vatsjBQqVg0Zwykpru6oriFOPGj+CP+SaPum0eENcoN81/Dmjfi8evJ0lvpwzz7eyGtLoAVJVv qgFx1RKNSeuLfAi4izFHfti/XswcqAh1cUo8FG9WEMU0OqbKN8RCk0thtR12Va+QwUl/VHwmia ZWWy0m8VL0ANKFyWmKIi0IFVh5Usawb2A5MYI4reMFJsjgqt0y8RxJxrg3YPlhKhrb0q31BzW3 oW97ZYti+rVkQXo+kzHI6e6g
- References: <eb2647bb-ebef-4361-9b1c-965580239635n@googlegroups.com>
Hi Zeinab,
is it possible that you ran out of disk space? If that's not it, please open a Github issue at https://github.com/tlaplus/tlaplus/issues/.
Markus
> On Feb 22, 2022, at 8:27 AM, Zeinab Nehaï <zeinab.nehai@xxxxxxxxx> wrote:
>
> Hello everyone,
>
> I am a PhD student, and I use the TLA+ tool to apply verification methods to my distributed model. I encountered a problem when I ran the TLC model checker, and although I researched the reason for this error, I did not find anything.
> My model represents a system with senders and recipients, and there may be Byzantines. Therefore, my study aims not to increase or decrease the number of processes but to vary the share of Byzantines processes in my system and check if my liveness properties are still valid.
> I don't know if giving details of my model is necessary to understand my problem, but if it is, please let me know.
> So, I run TLC on a docker using :
> java -cp tla2tools.jar tlc2.TLC -nowarning -deadlock -workers 30 model.tla.
> Runs with a small number of Byzantine processes are not a problem, and TLC manages to finish.
> However, I got the following error with one correct process and five Byzantine processes after 10 hours of running.
>
> Error: 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.EOFException
> java.io.EOFException
> at java.base/java.io.RandomAccessFile.readInt(RandomAccessFile.java:837)
> at java.base/java.io.RandomAccessFile.readLong(RandomAccessFile.java:870)
> at tlc2.util.BitVector.read(BitVector.java:216)
> at tlc2.tool.liveness.GraphNode.read(GraphNode.java:388)
> at tlc2.tool.liveness.AbstractDiskGraph.getNodeFromDisk(AbstractDiskGraph.java:246)
> at tlc2.tool.liveness.AbstractDiskGraph.getNode(AbstractDiskGraph.java:225)
> at tlc2.tool.liveness.LiveWorker.checkSccs(LiveWorker.java:351)
> at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:1257)
> at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:41)
> at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
> at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
> at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
> at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
> at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
> at java.base/java.lang.Thread.run(Thread.java:829)
>
> Could you please help with this error and tell me what it means? I have the last version of TLC, and the docker has enough memory.
>
> Thank you for your help,
> Zeinab
--
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/02D8F81A-AAEF-49FB-BC0F-3EFD93D0FACB%40lemmster.de.