How can I check if a variable is stable if once set

Dear TLAplus group,

I would like to check the safety property of a byzantine fault tolerant consenus algorithm by specifying an invariant of the form :

CONSTANT View, Request, Server

Undef == -1

Init == ...
/\ decided = [ s \in Server |-> [ dv \in View |-> Undef ] ]

DecidedSafe == \A s \in Server: \A v_c \in View: decided[s][v_c] # Undef => decided[s][v_c] = decided[s][v_c]'

I think this should be equal to decided[s][v_c] # Undef -> UNCHANGED <<decided[s][v_c]>> which produces the same unwanted behavior.

For completeness: Undef == -1 because TLC runs into an error with my initial definition it like Leslie Lamport did in his proof of ByzPaxos BConProof.tla in an unbounded way (Undef == CHOOSE v \in Nat : v \notin Request OR Undef == CHOOSE v : v \notin Request} \) and TLC is forced to actually check it, but this is a different story and this "bug" is known if I read the TLC Website correctly.

Back to my approach: If I run TLC with the above stated invariant it stops execution every time decided[s][v_c] is initially set to some value != Undef. I unfortunately lack in depth understanding of TLA/TLC and so I failed to come up with a predicate which provides the expected invariant up to now. I also failed to state an invariant using a temporal formula e.g. by using the [] operator because I guess this operator does not work in a conditional way? Maybe someone can give me a pointer in the right direction. If I have to provide more Information I will try to create a more complete minimum working example without having to provide the complete spec.

Best regards,
Christian