问题描述
我具有以下规格:
------------------------------ 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:
错误指向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".错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！