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 нарушен.В трассировке стека ошибка выглядит так*

Answer 1

location \in [register -> SUBSET BUILDING] означает (среди прочего), что DOMAIN location = register.Однако после DeRegister у вас есть DOMAIN location = {"pq"} /\ register = {}, что нарушает ваш инвариант.