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?