tla+ - 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"}