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

Re: Modelling interactive systems (state machines)

Many thanks Leslie. Honestly, I did read the PlusCal user manual (c-style) and watched most of your talks :)
I found the answer in the Hyperbook.

Best regards,

On Friday, August 8, 2014 9:45:58 AM UTC+10, Leslie Lamport wrote:

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.