\ in起作用，而\ subseteq给出"identifier undefined".错误 [英] \in works, while \subseteq gives a "identifier undefined" error

问题描述

我具有以下规格:

------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members

Init == members \subseteq People

Next == members' = members

Group == Init /\ [][Next]_members

=============================================================================

(我将此规范简化为没有任何用处的地方.)

(I simplified this spec to the point where it's not doing anything useful.)

当我尝试通过TLC运行它时，出现以下错误:

When I try to run it through TLC, I get the following error:

在评估中，标识符成员未定义或不是运算符.

In evaluation, the identifier members is either undefined or not an operator.

错误指向Init行.

当我将Init行更改为:

Init == members \in People

可以验证.

我想要以前的功能，因为我的意思是members是个人的集合，而不是一个人.

I want the former functionality because I mean for members to be a collection of People, not a single person.

根据 Leslie Lamport的指定系统 ，"TLA +在集合上提供以下运算符:"并列出\in和\subseteq.

为什么TLA +不让我使用\subseteq?

Why is TLA+ not letting me use \subseteq?

推荐答案

虽然是有效的TLA +表达式，但TLC只能通过语句x' = e或x' \in S将下一状态值分配给变量x.有关详细信息，请参见第14.2.6节.这也适用于初始分配.就您而言，您可能需要members \in SUBSET People.

While that is a valid TLA+ expression, TLC can only assign next-state values to a variable x by the statements x' = e or x' \in S. See section 14.2.6 for details. This holds for the initial assignment, too. In your case, you probably want members \in SUBSET People.

这篇关于\ in起作用，而\ subseteq给出"identifier undefined".错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！