问题标签 [tla+]

请给我一些关于TLA+语言项目主题的建议。我正在学习一门语言课程，这是我学习规范和验证的第一年，我不知道在两周内选择实施什么。有任何想法吗？

我试过了

但 TLC 给了我一个语法错误：

错误：TLC 在第 1 行的配置文件中发现错误。它需要 = 或 <-，但没有找到。

我也尝试将Sequences模块包含在配置文件中，但无济于事。

那么......我必须做些什么来分配一个序列？

我想在Erlang中翻译TLA中指定的一些操作。你能想到直接在 Erlang 中执行此操作的任何自然方式或任何可用的框架吗？简而言之（非常小的一个），TLA 动作是对变量的条件，其中一些是已启动的，这意味着它们代表下一个状态中变量的值。例如：

这个动作意味着，只要系统的状态PredicateA对于 variable为 truex并且对于PredicateB为 truey或PredicateC对于 为 true z，那么系统可能会改变它的状态，以便除了x更改为当前值加 1之外，一切都保持不变.

在 Erlang 中表达这一点需要大量的管道，至少以我发现的方式。例如，通过在触发条件之前评估条件的循环，例如：

我正在考虑编写一个框架来隐藏这种管道，将消息传递合并到get_new_info()函数中，并希望仍然使其符合 OTP。如果您知道任何已经这样做的框架，或者您可以想到一种简单的实现方式，我将很高兴听到它。

到目前为止，我已经为我的项目做了一点代码，但不知道它是真是假。你们能看到我的代码吗？首先，我应该发布要求以更好地理解..

在计算机科学中，互斥是指确保没有两个进程或线程同时处于其临界区的要求。临界区是指进程访问共享资源（如共享内存）的一段时间。互斥问题由 Edsger W. Dijkstra 于 1965 年在他的论文《并发编程控制问题的解决方案》中首次发现并解决。

有关问题的直观描述，请参见图。在链表中，节点的删除是通过将前一个节点的“下一个”指针更改为指向后续节点来完成的（例如，如果节点 i 正在被删除，那么节点 i-1 的“下一个”指针将是改为指向节点 i+1)。在多个进程之间共享这样一个链表的执行中，两个进程可能会尝试同时删除两个不同的节点，从而导致以下问题：设节点 i 和 i+1 为要删除的节点；此外，不要让他们成为头或尾；节点 i-1 的 next 指针将更改为指向节点 i+1，节点 i 的 next 指针将更改为指向节点 i+2。尽管两个删除操作都成功完成，节点 i+1 保留在列表中，因为 i-1 指向 i+1 跳过节点 i（该节点通过将下一个指针设置为 i+2 来反映 i+1 的删除）。可以使用互斥来避免此问题，以确保不会同时更新列表的同一部分。

这是我的代码：

我目前正在写我的硕士论文，并面临着在时间逻辑中指定和验证我的方法。

在我的情况下，哪种时间逻辑最适合使用？我真的很想得到一些关于我的方法以及如何进行的反馈

我的模型由参与者组成，这些参与者将同时执行。对于每个参与者，可以注册规则。它们看起来像这样：

例如

这意味着 c 必须收到来自 b 的消息和来自 c 的消息，才能被允许向 d 发送消息。

在其中一个参与者发送或接收消息之前，我的原型会检查参与者是否被允许执行该操作。到目前为止，我想验证该算法是否执行以下操作：

1. 如果不存在其条件成立的规则：禁止该操作

2. 如果存在条件成立且禁止该操作的规则：禁止该操作

3. 如果存在条件成立的规则，则它允许该操作，并且不存在其条件成立且禁止该操作的其他规则：允许该操作

这是Leslie Lamport的文章教学并发中的一个简单的并发程序。

考虑N从 0 到N-1每个进程i执行的进程

并停止，每个x[i]初始等于 0。（每个的读取和写入x[i]都假定是原子的。）

该算法满足以下性质：在每个进程停止后，y[i]至少有一个进程等于 1 i。很容易验证：最后i写入的进程y[i]必须设置为 1。

然后，兰波特评论说

但是该进程没有设置y[i]为 1，因为它是最后一个 write 进程y。

该算法满足此属性，因为它保持一个归纳不变量。你知道那个不变量是什么吗？如果不是，那么您并不完全理解该算法为什么满足此属性。

所以，

并发程序的归纳不变量是什么？

我已经编写了关于河内塔问题的 TLA+ 规范：

TEX

ASCII

Invariant当我将公式指定为不变量时，TLA 模型检查器将为我解决难题。

我想让它变得不那么冗长，理想情况下我不想将未更改的变量传递给Move()，但我不知道如何。我想做的是写

我如何用 TLA 语言表达它？

我尝试在 TLA+ Toolbox（工具箱）中建模 Paxos（ Paxos 示例）。我应该在模型中输入什么数字才能使其工作？或者还有其他方法可以在这个工具箱中确认这个算法吗？

基于此代码：

我尝试这样的数字：

接受者 <- [11,12,13,14,15];

法定人数 <- [11,12,13,14,15,16,17,18,19];

值 <- [0,1]；

但我收到 ArrayIndexOutOfBoundsException 错误。

对不起，标题有点神秘。我有一个 TLA+ 规范，它定义了两组：

我有一组工人添加请求，另一组或工人满足它们并写信给Outcomes. 每个请求都有一个唯一Id的，匹配的Outcome条目也将包含它。

我想保证添加到Requests集合中的任何请求最终都与集合中具有相同的结构Id匹配Outcomes。我一直在尝试使用 "leads to", ~>, 运算符来执行此操作，但无法弄清楚如何解决Id匹配部分。

我天真地尝试过类似的东西：

但这显然会中断，因为req在第二个表达式中没有定义。我已经考虑过第二个表达的内容是“然后有一个状态，所有请求项都与结果项匹配”，但这不起作用，因为系统永远不会终止 - 很可能总是有更多的请求中Requests盘，自是Outcomes一直在追赶。

我有什么方法可以断言请求最终与具有相同 ID 的结果匹配？

TLA+ 是否将 xor 运算符定义为语言本身的一部分，还是我必须自己定义？