distributed-system - 关于 TLA+ 中的常量运算符的问题

Question

我最近正在阅读“指定系统”一书。在第 5 章中，Leslie 定义了常量运算符 Send( , , , )。

我对如何为这个常量表达式赋值（真/假）感到困惑？我们是否需要为 TLC 模型检查器中的每个 (p, v, m, m') 分配真/假？

标签： distributed-systemtla+formalize

Answer 1

Send您可以通过两种方式分配给：

1. 如果你在另一个模块中实例化它，你可以传入你想要的操作符WITH：Instance Foo WITH Send <- Op \*...
2. 您可以在 TLC 中的“型号是什么？”下分配一个操作员。