删除元素的TLA+故障

Question

目前正在学习TLA+，并且被困在这个简单的方法上，从寄存器中删除一个人。从我所能看到的情况来看，问题似乎与许可状态有关。

我的TLA+函数如下所示，并从寄存器中删除一个人以及权限。

DeRegister(p) == 
/\ p \in register
/\ register' = register \ {p}
/\ permission' = [x \in DOMAIN permission \ {p} |-> permission[x]]
/\ UNCHANGED <<location>>

我正在检查的类型有以下约束

TypeOk 
    /\ register \subseteq PERSON
    /\ permission \in [register -> SUBSET BUILDING]
    /\ location \in [register -> (BUILDING \union {OUTSIDE})]

我得到一个模型错误，typeOK被违反了。在堆栈跟踪中，错误如下所示

/\  location = [p1 |-> OUTSIDE]
/\  permission = << >>
/\  register = {}

谢谢你的洞察力

编辑：

以前的状态可能有一些用处

/\  location = [p2 |-> OUTSIDE]
/\  permission = [p2 |-> {}]
/\  register = {"p2"}

Answer 1

location \in [register -> SUBSET BUILDING]的意思(除其他外)是指DOMAIN location = register。但是，在DeRegister之后，您有了DOMAIN location = {"pq"} /\ register = {}，这违反了您的不变式。