My original definitions of safe, regular, and atomic (for a single
writer) were given in a formalism whose semantics is not the trace
semantics of TLA, a direct translation of those concepts into TLA+ is
not nice. But it's not difficult. Here's one way. Just let the
writer have a variable that contains the current value of the
register, and let have each reader have a data structure including a
sequence of writer operations to which, when the reader is currently
writing, the writer appends something when it begins and finishes each
write operation.
I believe the following simpler TLA+ implementations can be
proven to be equivalent. For an atomic register, just make the reads
and writes atomic. For safe and regular, here are implementations of
a register r to which a single writer can write a value in a set T of
possible values and any number of readers can read the value.
Safe Register - Method 1
--------------------------
Define notValue == CHOOSE t : t \notin T
Write(v) a: r := notValue ;
b: r := v ;
Read c: with (v \in IF r = notValue THEN T ELSE {r})
{ result := v }
Safe Register - Method 2
--------------------------
Write(v) a: with (v \in T) {r := v}
either goto a
or await r = v ;
Read result := r
Regular Register
----------------
Write(v) r := v ;
Read Seen := {}
a: either { Seen := Seen \cup {r};
goto a }
or with (v \in Seen)
{ return v }
Leslie