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

[tlaplus] Re: Question regarding Two Phase Commit spec and the enabling condition of one of its definitions

When writing specs, should UNCHANGED <<>> condition be applied to all variables which have not been explicitly changed? Should we apply UNCHANGED to all such variables by default or should it be used when UNCHANGED has a strong significance in the context of the definition?

You always have to specify what next state of each variable is going to be.

  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

is shorthand for

  /\ tmState' = tmState
  /\ tmPrepared' = tmPrepared
  /\ msgs' = msgs

If you comment out UNCHANGED <<...>> part, you get following error.

Successor state is not completely specified by action RMChooseToAbort of the next-state relation. The following variables are not assigned: msgs, tmPrepared, tmState.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3b6bda77-b26a-4cfb-8a31-a7b33e4f33e9%40googlegroups.com.