Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?

[Hillel Wayne <hwayne@xxxxxxxxx>]

Another thing you can do is use the "leads to" operator (~>), where P ~> Q ≡ [](P => <>Q):

succeeded ~> accomplished_work

This is useful if you want to express that something might not ever succeed, but if it does, then you will eventually accomplish work.

I'd also recommend spending some time building an intuition for the difference between weak fairness and strong fairness.

H

On 2/23/19 10:10 AM, A. Jesse Jiryu Davis wrote:

Hello! I'm modeling a process that will retry indefinitely until it succeeds. A toy version of the process looks like:

variables

    succeeded = FALSE;

fair process retry_example = "retry_example"

begin

    RETRY_BEGIN:

        either

            RETRY_SUCCEED:

                succeeded := TRUE;

        or

            RETRY_ERROR:

                goto RETRY_BEGIN;

        end either;

end process;

Is there a useful way to test that such a process "eventually" succeeds? Right now, the following temporal property fails because the process could retry forever:

[]<>(succeeded)

It seems like I should be able to modify this spec so that TLC can check useful things about it. For example I could add a counter to the process, just for TLC's sake, that limits the number of times it fails.

Or I could assert that if it has ever succeeded at its first step, then it has accomplished some subsequent work:

variables

    succeeded = FALSE,

    accomplished_work = FALSE;

fair process retry_example = "retry_example"

begin

    RETRY_BEGIN:

        either

            RETRY_SUCCEED:

                succeeded := TRUE;

            DO_MORE_WORK:

                \* Imagine further steps between these lines.

                accomplished_work := TRUE;

        or

            RETRY_ERROR:

                goto RETRY_BEGIN;

        end either;

end process;

And then test this property, that if the process ever succeeded then it accomplished work:

<>[](succeeded => accomplished_work)

My general question is this: there are lots of algorithms that include indefinite retries, I'm curious how people test that they are correct, if there is a concept like "eventually succeeds" that can be tested with such specs?

--
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.
For more options, visit https://groups.google.com/d/optout.

--
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.
For more options, visit https://groups.google.com/d/optout.