If possible, some more
questions (should I create new topics for it?):
- how TLC distinguish between
assignment and comparison? E.g. use of x` = 1 in the action definition will be
considered as assignment, but as comparison in a temporal property? Can primed
variables be used in condition statements in the definition of actions?
- what is necessity of
if-then-else operator if conditionality can be naturally expressed with FOL?
- work of print function is
quite confusing. I understand that output depends on internal TLC algorithm, so
please advise where I may read more about print?
- how TLA+ supports modelling
of concurrent systems - parallelism, synchronisation, atomic operations? There
are no corresponding keywords in TLA+.
Hi, is it possible in TLA to specify and check the property linking values of current and next states, like Prop == (x = 1) => (y` = 2). Seems to be the operation "=" for primed variables (as e.g. y') will be considered as assignement, but not comparison? Tq.