[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] how TLA+ verify the crash model?
- From: 杨超 <magicsupery@xxxxxxxxx>
- Date: Mon, 29 Nov 2021 00:08:06 -0800 (PST)
- Ironport-data: A9a23:OUqPkKjZi2hr4PBdUxeGwwz8X161RBEKZh0ujC45NGQNrF6WrkUBzmJMCGqBP/yKNmanKtFxOo629UIBvp7Qm9BlSAJlqVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t51GAjX4wXFdokb0/n9BCZC86ykjvU20buCkUredY3ohHVQMpBoJ0HqPpcZp2uaEvvDiW2thifuqyyHuEAfNNwxcagr42IrfwP9bh8kejRtD1rAIiV+ni3eF/5UdJMp3yahctBIUSKEMdgKxb76rIL1UYgrkExkR5tONyt4Xc2UPS7/WeA+J0z9YBvXkjR9FqSg/lK08MZLwa28N02TPz403kYsU88HtIesqFvWkdOA1Tx1RCyVjJu5M/rTtDSWegeK04XP7XlHG8alTN2IZBKg3w8stIVhqz6cpAD8KaR+Hiu2sx6+jUa9ngcFLwMzDYtxC5yk8kVk1Ct5/GcyZK0nQ3vdU3Sw7m9tVNerabowcciAqbRLaYhQJO1ENCZt4kv3Au5VVWykA/RfN4/Yjuj2LilRliu21doeFJ4GeHpAN2BuM+Tfv4ULSBzc2NPi+wB+56FSSh8rbxHuuAMZJANVU7dZviVyXg2sUUVgYCAb9rv6+hUqzHdlYLiQpFuMVhfBa3CSWohPVBnVUYUJovyLwn/JVGuw+rQaKk+/avlvfCW8DQTpMLtchsafagBRCOkChx7vU6f5H6dV5ik5xMp+bqjS9PSUaN2gffTRCRgwAizUmiJ9mlQrBF76PD4bs5uAY2ljML/Sioy85iLEegtQMyr2gu1vAhlpAY7ChohEdvm3qY45u0u+1iENJqWBlBZg3IMus9Lqkc2Q=
- Ironport-hdrordr: A9a23:mHBcjKltLbBMgf9RakGvjnlZrt/pDfIn3DAbv31ZSRFFG/FwWfre/8jzpiWUtN9xYhodcL+7VZVoLUmskKKdpLNhWYtKPzOLhILLFutfBOLZqlXd8m/Fh4xgPMxbHZSWZueRMbE3t6nH3DU=
fair process config = CONFIG
begin
Ctor:
Tick:
CrashOrContinue:
if sthDone then
goto Done;
else
either
goto Tick;
or
goto Ctor;
end either;
end if;
end process;
my system has 4 process, the config process maybe crash, i want to verify that after the config crash, the whole system can eventually stable.
but i found the "either or" not make sure that goto Ctor will happen!
How can i do that, the crash will happen at some time, but the time not sure?
--
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/62e4f654-bdaf-473b-bc7a-18ad3d1e9f7dn%40googlegroups.com.