[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Modelling interactive systems (state machines)

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.