[tlaplus] Artificial coupling of variables

[Jedd Haberstro <jhaberstro@xxxxxxxxx>]

Hello,

Consider this simple module

EXTENDS Integers

VARIABLES s   

Init ==

    s = [i \in 1..2 |-> 0]

Inc(i) ==

    s' = [s EXCEPT ![i] = s[i] + 1]

           

Next == Inc(1) /\ Inc(2)

Next can never be enabled because Inc(i) is enabled when just 1 element of the array increments. This artificial coupling is a byproduct of my choice to represent logically independent variables with a function(/array).

In this particular module the coupling could be removed by replacing s with variables s1 and s2 and using an IF or CASE conditioned on i to select which variable to increment. In the general case, however, this is not a practical solution as the number of variables may be parameterized by a CONSTANT. 

To contextualize the issue, I am writing a specification for an API and trying to show that a particular system implements this API. The implementation allows for multiple processes to take "steps of execution" in parallel (e.g. two processes blocked on the same condition may unblock in one state transition), whereas the API is defined only in terms of local steps of execution each process may take; the potential for parallelism of the system has no impact on semantics of the API.

The way I see it, I have two options:

1. Define a refinement mapping that somehow shows that, e.g., 1 state transition of the implementation that unblocks N processes, is equivalent to N state transitions in the API spec where the transitions unblock processes one by one. Being new to TLA+, I'm not confident in my ability to figure out how to actually express this.. :D

2. At the cost of clarity, model the potential for parallelism explicitly in the API spec, which will mean changing the definition of every sub-action. 

What I wish I could do is change my API spec without having to change its sub-actions by formulating the top-level Next state action like this:

\E stepping \in SUBSET Threads :

        /\ stepping # {}

        /\ \A t \in stepping :

              \/ MethodA(t)

              \/ MethodB(t)

              \/ .... etc ...

but, of course, this does not work because each Method sub-action contains a predicate of the form

controlState' = [controlState EXCEPT ![t] = .... ]

So, to recap, unless there is some other option I haven't thought of, I am forced to introduce complexity into my spec to workaround syntactic deficits of the TLA+ language. It seems that if there were a macro system built into the language, it would be possible to express what I wish without the additional complexity.

Have I correctly understood the situation or is there an idiom or feature of the TLA+ language that will help my situation?

Thank you,

Jedd

-- 
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/734edefa-87e0-4f29-8cb4-f3d0e71c5672n%40googlegroups.com.