[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] How can I check all histories about the TLA+ execution in toolbox?
- From: 钱晨 <allenhandora@xxxxxxxxx>
- Date: Thu, 16 Jun 2022 19:06:48 -0700 (PDT)
- Ironport-data: A9a23:wJCEoaKJOxEPyzQwFE+RdZAlxSXFcZb7ZxGr2PjKsXjdYENS0GdRn GYZUGDQO/6KZTH2cth3bt7g808OuMKEz9ZnSgod+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M58wIFqtQw24LhXVrT4 Y+aT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhn/xT8 MhWm42KTCgbFPbNqrsnazNdOnQrVUFG0OevzXmXtMWSywjfcCKpzaw/VAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmuj9E7g07iggBJGD0Ic3pnVp1TXEFrUsR5vpaIPyx/po5AYdpPpkOtHyW ZQ6UB9AVTnvQkBmC3s+IJ05m+isi3bldCBAsxSeoq9fD237lVMpiOm1bYG9ltqiT9xKn0ORi mD/0D66HQ47JoaH+xPGyyf57gPItXqjBNh6+KeD3vJrm1aO3Xc7FBkfE16gu7y4jFS/UpReL VYV82wgt8APGFeDS9D8W1ihoyfBsEdNA5xfFOo17AzLwa3Ri+qEOoQaZj5tSuQ7r+EnfzkF5 HXSnuG2PwRFtZTAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3C7q8FIt/IFh+Ou 38Ln8XY5+cLZX1sqMBvaLpQdF1Kz6zdWNE5vbKJN8R7n9hK0yLyFb28GBkkeC9U3j8sIFcFm nP7twJL/4N0N3C3d6JxaI/ZI510kPW8TYi/DayMM4Umjn1NmOmvrHEGiam4jzCFraTQufxX1 WqzKprwVylCV8yLMhLvGLxGj9fHORzSNUuKHcyhp/hW+bWZY3GRRN843KimP4gEAFe/iFyNq 753bpPUoz0GCbGWSnSJrOY7cA5bRVBmVcGeg5EGK4arf1s2cEl/UaO56e16IeRNwf8F/tokC 1n4BCe0PnKh1SeeQehLA1g4AI7SsWFX9i5iZXZ9ZQ32hRDOo++Htc8iSnf+RpF/nMQL8BK+Z 6NtlxyoDqsdRzLZ1S4aaJWh/oVueA7y21CBOC2qZDUwZZl9XxeP8djhJ1O9+C4LByuxlM0/v 7zxhliAGMFcGVtvXJTMdfai71KtpnxByuh8aE3Ff4tIc0L2/Yk2diH816dlI8wFJRjZ6CGd0 gKaXUURqeXX8t069dDIgeaPqILwS7lyGU9THm/667eqNHmCrjDzn9MYCOvRJGLTTmL5/qmmd N559fCkPa1VhktOvqp9D61vkvAz6t7pkLlQkVZpEXDNWFK0U+8yL3SD2/5Pga1D3LpuvwW7B xCU8d5ANLTVYc7oHQdKdgooZ+iOz8sZgj3D8fMxLBmo7SN75uPZA0pVOBaIhSNHK6ZtK8Uux uJ44Jwa7Am2ixwLNNeaj3EErD/VdSNeDKh35IsHBILLixYwzg0Qa5LrDCKrsoqEbM9BMxV3L zKZ2PjCirBbyhaQenY/DyKRj+9UhJBLoRMTiVFbdgzPld3Cifs6mhZW9G1vHAhSyxxG1cN1O 3RqZxIpf/TQp28wiZgRRX2oFiFAGAadph77xWwPmTCLVEKvTGHMcDAwNLff+EEC719aZSVR+ L3Emm/pXSy0LJP01yo2RUk3pPvkQth8+RfFhdi8WsGMGZA1bHm+3f//OTdW+0S+WJ1ymUvcu ONx9/xxY6DTOikXrKk2BJOdyKwLDhuDITUaE/1m+aoIG0DaeS2ziGjVcBnqJZ0SKqyY61K8B uxvOtlLC0a02hGIo21JHqULObJ1wKMk6dZeKLrnKXRa4umfsiZxq8CXsSfkg3IzWJNhlsEyL o6XfDWHVWOKgmZM3HPJpdFAJ3H/esQOfwbm3eq4/ehVRYgPtvpgLRM73reu5SnHNQJm+1eNv 1qGafaHl6ptzoNjm4aqGaJGXl3mJdT2XeWO0Qayr9UeMo+VYJmW71sY+gv9IgBbHboNQNArx 76Dh9j6gRHet7EsXmGFxpSMGsGlPylpsDa77y42EJVbocdGcMrl4h9G4mPhbJIQwYsb6c6gS A+1LsC3cLb5njubKGJ9M0Bj/9Q1UswbrZsMYQuyqPODDhUSywvaNMjh/njsBY2eXjFdIIXwU 2cYpN73ju21b+1w6NssCPZhDJt1L0XkRLM9Mdb2sFF0y4Vubkyq4tPfqPbr1d0H5rRo3io3D VIpiyUSrCiPhZw=
- Ironport-hdrordr: A9a23:/8zfZKqJkJE7XkPQD4r60dwaV5q0eYIsimQD101hICG9E/bo7f xG+c5wuCMc5wxhPE3I9erwX5VprxvnhOpICad4B8bWYOCkghrYEGlahbGSsQEIYheOgdK1tp 0QCJSXvbbLfCZHZLjBkXCF+o0bsaa6GcmT7I+0vhVQpGdRGt1dBihCZTpzeXcGPDWua6BJcq Z1J6J81lmdkLcsAPhTxENoYwByzOe7564OrSRmO/bWgzP+8A9AIYSbYn2l9yZbaSpGxfMJ8G TOkQD1ooWl99+hzAPEvlWjn6hrpA==
- Ironport-sdr: Wvp3o4dM5+aNBk1+ZdSavpEFLRaKrsFSK3QRiZ03TpsLTJlI6WuG2w2FfDQQn9TXKVu7K1jRug DhEMTUNwxzio6bYa6pTDJlUpRVv5w+hUfUmBs5p4cQRxH2CoelDrZchzuj1EUlAiZsg3ONpG3J bFQLz8T38tiN9TpDoZnnhXe9CJzHbxRN5uikow91AXKC3PhY8SHvbpb5TogPTcp3lzGgki2JIo nWfyQgRy6B1KW3UqdVp/fqGYqj0XtVxYjXT18/LOfAyjkPCJEucNnuiVJ+Ezj0vYaKZZSSnzFp 656o5/nBOv0l7LP/z/BL++/l
I have recently written a 2PC specification in the toolbox, run a simple model on it(run a model with 3 participants) and successfully passed the model.
While I cannot know whether all history goes to the end that satisfies the liveness requirement(such as all goes to commit state). So can I record all histories of the model check without writing a fairness function
--
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/8701ca11-e5c4-4354-9885-d877a3b81caen%40googlegroups.com.