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

*From*: Jedd Haberstro <jhaberstro@xxxxxxxxx>*Date*: Sun, 6 Sep 2020 02:11:02 -0700 (PDT)*References*: <734edefa-87e0-4f29-8cb4-f3d0e71c5672n@googlegroups.com> <10548514-4F31-45A5-B28E-47CD6103E566@gmail.com>

Hi Stephan,

Thanks for the guidance.

I do believe a refinement is possible. Wherever the implementation takes an atomic step that is not mandated by the API (i.e. allowed by the API's TLA+ spec), the implementation's spec could be written such that artificial steps are inserted that behave like stuttering steps for all variables except those used in the refinement mapping. There would be as many of these steps inserted into the implementation's behaviour as is necessary for the refinement mapping variables to eventually equal the implementation's actual state while still representing valid state transitions in the the API spec. Do you disagree?

Admittedly, this feels like it would be quite the tedious machinery to tack onto, what I anticipate to be, a non-trivial spec, so I am not keen to go down this path..

I think I agree that embracing the fact that several transitions may occur is the correct path forward. As for you specific suggestion, I suppose this would have several implications on how to write the operators that compute the result of the operation:

- No use of prime variables.
- Enabling predicates must be rewritten as IF or CASE expressions.

More importantly, I'm failing to see how to handle multiple primed variables.

Thanks,

Jedd

On Sunday, September 6, 2020 at 12:14:14 AM UTC-7 Stephan Merz wrote:

Hello,TLA+ actions describe atomic transitions, and this excludes the first option that you mention: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.The sequence of N transitions contains (visible) states that do not exist in the execution having a single transition. Therefore refinement simply does not hold.I'd recommend that your specification fully embrace the fact that several transitions may occur. In your toy example, you could do so by writingEXTENDS IntegersVARIABLES sInit ==s = [i \in 1..2 |-> 0]Inc(S) ==s' = [i \in 1..2 |-> IF i \in S THEN s[i]+1 ELSE s[i]]Next == \E S \in SUBSET (1..2) : Inc(S)In a more realistic example, you'd replace s[i]+1 by an operator that computes the result of the operation that the action represents, based on the current state.Regards,StephanOn 6 Sep 2020, at 05:32, Jedd Haberstro <jhabe...@xxxxxxxxx> wrote:Hello,Consider this simple moduleEXTENDS IntegersVARIABLES sInit ==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.. :D2. 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 IwishI 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 formcontrolState' = [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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/734edefa-87e0-4f29-8cb4-f3d0e71c5672n%40googlegroups.com.

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/26e4fbb6-100d-4d5c-8e23-da31d6d4bbf3n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Artificial coupling of variables***From:*Stephan Merz

**References**:**[tlaplus] Artificial coupling of variables***From:*Jedd Haberstro

**Re: [tlaplus] Artificial coupling of variables***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Artificial coupling of variables** - Next by Date:
**Re: [tlaplus] Artificial coupling of variables** - Previous by thread:
**Re: [tlaplus] Artificial coupling of variables** - Next by thread:
**Re: [tlaplus] Artificial coupling of variables** - Index(es):