Hi Steven,
sorry for replying so late: I had a look at your PlusCal model of the algorithm, and I think that it is very competently written. (I have not tried to understand the algorithm, though.)
A (standard) suggestion for mitigating state space explosion is to reduce labels as much as you can, and of course as far as it doesn't impact the verdict of model checking. For example, I noticed some patterns like the following:
if Acquired then
RET: return;
end if;
UPDATE_COUNTER:
Counter := Counter + 1;
and I believe that the only reason for having label UPDATE_COUNTER is syntactic, since PlusCal needs a label at the statement following a conditional statement. However, you can rewrite your code to the semantically equivalent
if Acquired then
RET: return;
else
Counter := Counter + 1;
end if;
and save a label. This is relevant because TLC will non-deterministically schedule any executable thread at every label.
Of course, state explosion will set in despite these changes, and then you should think about how many threads you would like to check in order to be reasonably confident about correctness.
Best regards,
Stephan