PlusCal

Nov 13 2024

Procedure必须用return来退出，否则在运行时TLA+会认为有Deadlock，如果勾选了Deadlock检测则会报错。

comments powered by Disqus