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

[tlaplus] Re: how to updating state and return in a definition

Simple logic shows that your definition of UpdateCounter is 
equivalent to

   UpDateCounter(participant, newCounter) ==
      /\ counters[participant] < newCounter
      /\ counters' = [counters EXCEPT ![participant] = newCounter]

(For example FALSE /\ UNCHANGED << counters >> is equivalent to FALSE.)
I don't see how to do what you're trying to do.  It's possible
that there's some clever way to express what you want to express.
However, I'm almost certain that TLC would not be able to handle the
resulting spec.  

I suggest that you stop thinking in terms of programming language
constructs and start thinking in terms of two separate physical
components that are trying to cooperate, with each of them revealing
to the other as little about their state as possible.

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/51cd1cbe-2f00-4f9a-aebf-67a0a4157bae%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.