Ola Bini <obini@thoughtworks.com> writes:

Hi,

...

So maybe the simple answer here is that if prop247 is enabled (this could be a NumGuards=N argument to our algorithm), instead of always returning the first reachable guard, we instead build a list of the first N reachable guards, and randomly choose one of them. Could this work? (see #12466 for a weird behavior that will make us skip bugs if NumEntryGuards != 1) Ah, I understand. We could definitely do that. I think the easiest way is to just have a parameter to the existing algorithm with ExcludeNodes. We can then repeat it N times sending in the previous nodes chosen as ExcludeNodes. This will generate the N reachable first guards. Then, we can just choose randomly from them.

Does that sound reasonable?

Yes, that sounds like a reasonable way to achieve this. Maybe N_PRIMARY_GUARDS should also scale up in that case, so that N_PRIMARY_GUARDS >= N.