Search code examples
tla+

TLA+ Trouble removing an element

Currently learning TLA+ and have gotten stuck on this simple method to remove a person from a register. Issue seems to be with the permission state from what I can see.

My TLA+ function looks like this and removes a person from the register along with the permissions. 

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

My typeok that I'm checking against has the following constraints

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

I get a model error that typeOK is violated. In the stack trace the error looks like this

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

Thanks for any insight

EDIT:

Previous state may be of some use which was

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

  • location \in [register -> SUBSET BUILDING] means (among other things) that DOMAIN location = register. After DeRegister, though, you have DOMAIN location = {"pq"} /\ register = {}, which violates your invariant.