distributed-computing - 将 TLA+ 模块中的运算符导入另一个文件

Question

假设我们在tools.tla文件中有这些运算符：

---- MODULE PT ----
Max(x, y) == IF x > y THEN x ELSE y
Min(x, y) == IF x < y THEN x ELSE y
===== 

我们想传递值（如python等编程语言中的参数）并在另一个文件中使用它们，调用它use.tla，只使用Max和Min而不重新实现它们；这怎么可能？

Answer 1

我遇到了类似的问题，这就是我的解决方案：

文件 -> 打开模块 -> 添加 TLA+ 模块 -> tools.tla

将创建空的 tools.tla，编写您的代码。

返回到另一个文件并

扩展工具