For a brief answer to your question about how to represent
nondeterminism in TLA+ specs, look up "CHOOSE, is deterministic" in
the index of the Hyperbook. To answer your question about modeling
events in one variable: The state of a system is represented by the
values of variables. Since TLA+ expressions can describe any kind of
data structure you want, you can if you wish write any specification
using only a single variable.It sounds like you are trying to learn to write TLA+ specs by trial
and error. There is an easier way: read the Hyperbook.