1
条回答
写回答
写回答
-
对于串行算法来说，算法中的动作是Totally Ordered，本身就是一个串行的状态机，很容易构造状态图。但并发算法或者分布式算法中的动作是Partially Ordered，不是一个串行的状态机，如何构造出状态图呢？ 如果并发算法或者分布式算法中的动作也能变成Totally Ordered，则也可以看作是一个串行的状态机，构造出状态图。 事实上TLA+大放异彩的地方正是在并发算法和分布式算法领域，因为在这些领域算法的行为多种多样，容易疏漏，因此需要TLA+全面检查算法的所有路径，不漏掉任何一种行为。
2022-05-10 18:13:33赞同 展开评论 打赏
版权声明：本文内容由阿里云实名注册用户自发贡献，版权归原作者所有，阿里云开发者社区不拥有其著作权，亦不承担相应法律责任。具体规则请查看《阿里云开发者社区用户服务协议》和《阿里云开发者社区知识产权保护指引》。如果您发现本社区中有涉嫌抄袭的内容，填写侵权投诉表单进行举报，一经查实，本社区将立刻删除涉嫌侵权内容。
相关问答
