TLA+ 无法删除元素

Question

目前正在学习 TLA+，并且一直坚持使用这种从登记簿中删除人员的简单方法。从我所见，问题似乎与许可状态有关。

我的 TLA+ 函数如下所示，它从注册表中删除了一个人以及权限。

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

我正在检查的我的 typeok 具有以下限制

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 = {}，这违反了您的不变量。

TLA+ 无法删除元素

TLA+ Trouble removing an element

tla+