how to updating state and return in a definition

[Balaji Arun]

I am trying to have a specification with a definition for Calculate()

module A:

VARIABLE val

Calculate() ==
   val' = val + 1
   (*return [v: val] here*)

How do I return that val to whoever is calling it (even another module that instantiates module A)? Assuming multiple processes call Calculate concurrently.

[Amir A.H.S.A]

It is important to note that Calculate() is not a "function" that we use everyday in programming languages.

Calculate() is an action that changes the current state to the next state by changing the value of variable val.

AmirHossein

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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/d6598cfb-609a-4f6c-98a6-b12d58e6c6b4%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hello,

if you remove the empty pair of parentheses, your definition is correct TLA+. It defines an operator whose effect it is to increment the state variable val and in can be used inside an action like so:

MyAction ==

  /\ ...

  /\ Calculate   \* update variable val

  /\ ...

There is no notion of "returning" an update of a variable.

If you'd rather compute a value that can be used within an expression you can define

ValPlusOne == val + 1

and have something like

f' = [f EXCEPT ![p] = ValPlusOne]

for updating an array at a certain position.

Regards,

Stephan

[Balaji Arun]

Thanks for the reply. Is there a way to emulate "returning" a value? My module A is being used as an instance in another module B, but I want A to be as isolated as possible.

I came up with something like below. Is this acceptable?

CONSTANTS Participants
VARIABLE counters

Init == counters = [i \in Participants |-> 0]

UpdateCounter(participant, newCounter) ==

   IF /\ counters[participant] < newCounter THEN

      /\ counters' = [counters EXCEPT ![participant] = newCounter]

      /\ TRUE

   ELSE

      /\ FALSE

      /\ UNCHANGED << counters >>

UpdateAndGet(participant, newCounter) ==

   IF UpdateCounter(participant, newCounter) THEN

      [p |-> participant, c |-> newCounter]

   ELSE

      [p |-> participant, c |-> counters[participant]]

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Leslie Lamport]

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.