TLA+建模中如何检查值不在集合？报错问题求助

问题代码 #

我用TLA+对系统建模，简化后的模型代码如下：

---- MODULE demonstrate_question ----

VARIABLE msg_queue

vars == <<msg_queue>>

request == {"request"}
response == {"response"}

InsertToQueue(message, queue) ==
    queue \union message

RemoveFromQueue(message, queue) ==
    queue \ message

IsMessageInQueue(message, queue) ==
    message \in queue

MessageNotInQueue(message, queue) ==
(* Also tried ~(IsMessageInQueue(message, queue)); also failed *)
    message \notin queue

NewMessage(message, queue) ==
(* Also tried /\ message \notin queue; failed *)
    MessageNotInQueue(message,msg_queue)

Init ==
    /\ msg_queue = {}


RequestReceived(message) ==
    /\ NewMessage(message, msg_queue)
    /\ msg_queue' = InsertToQueue(message, msg_queue)

Next ==
    \/ RequestReceived(request)

Spec == Init \/ [][Next]_vars    
====

错误信息 #

模型检查时触发如下异常：

The exception was a java.lang.RuntimeException
: Attempted to compare the set {"request"} with the value:
"request"

堆栈追踪指向RequestReceived中的NewMessage调用，注释该调用后无错误。需求是实现“检查特定值是否不在集合中”的逻辑，同时怀疑VSCode或TLC缓存是否影响。

问题原因与解决方案 #

核心问题 #

你混淆了集合和元素的类型：

• 定义request == {"request"}时，这是一个单元素集合，但msg_queue的设计目标是存储单个消息值（比如字符串"request"）。
• 执行message \notin queue时，实际是把集合{"request"}和msg_queue中的元素"request"做比较，类型不匹配导致报错。

修正步骤 #

1. 调整消息定义：把集合改为单个字符串值

   request == "request"
   response == "response"
   

2. 修正插入函数：union是集合间操作，单个元素需转为集合后再加入队列

   InsertToQueue(message, queue) ==
       queue \union {message}
   

3. 修正删除函数：同理，单个元素要转成集合才能从队列中移除

   RemoveFromQueue(message, queue) ==
       queue \ {message}
   

完整修正代码 #

---- MODULE demonstrate_question ----

VARIABLE msg_queue

vars == <<msg_queue>>

request == "request"
response == "response"

InsertToQueue(message, queue) ==
    queue \union {message}

RemoveFromQueue(message, queue) ==
    queue \ {message}

IsMessageInQueue(message, queue) ==
    message \in queue

MessageNotInQueue(message, queue) ==
    message \notin queue

NewMessage(message, queue) ==
    MessageNotInQueue(message, msg_queue)

Init ==
    /\ msg_queue = {}

RequestReceived(message) ==
    /\ NewMessage(message, msg_queue)
    /\ msg_queue' = InsertToQueue(message, msg_queue)

Next ==
    \/ RequestReceived(request)

Spec == Init /\ [][Next]_vars    
====

补充说明 #

• 缓存问题不会导致这个错误，这是明确的类型不匹配逻辑问题。如果之后遇到奇怪的缓存异常，可重启VSCode或在TLC模型检查器中点击「Clear Cache」按钮。
• 原Spec中的Init \/ [][Next]_vars改为Init /\ [][Next]_vars，这是TLA+规范的标准写法（初始状态加所有后续状态的不变式）。

内容的提问来源于stack exchange，提问作者Onorio Catenacci