1
条回答
写回答
写回答
-
TLA+的运行是完全串行的，运行的的过程即在状态图上做图的遍历，每遍历到一个状态，就检查一下当前状态是否满足事先设定的不变式，满足则继续遍历，不满足则立即报错。TLA+会尝试所有的遍历路径，不错过任何一种行为。我们知道图的遍历方式有深度优先和广度优先两种，TLA+默认广度优先遍历，也可配置成深度优先模式或者随机行为模式，深度优先模式需要给定一个最大深度。
2022-05-10 18:13:33赞同 展开评论 打赏
版权声明：本文内容由阿里云实名注册用户自发贡献，版权归原作者所有，阿里云开发者社区不拥有其著作权，亦不承担相应法律责任。具体规则请查看《阿里云开发者社区用户服务协议》和《阿里云开发者社区知识产权保护指引》。如果您发现本社区中有涉嫌抄袭的内容，填写侵权投诉表单进行举报，一经查实，本社区将立刻删除涉嫌侵权内容。
相关问答
