How to model transient network/service failures with eventual success (TLA+ fairness equivalent)?

[GilbertBckr]

I am wondering how to model a situation where the network might fail sometimes but never indefinitely - i.e., failures are transient and eventually succeed with retries.

In TLA+, I could use strong fairness (SF_vars(Action)) to guarantee eventual transition to a state where the network delivers messages. However, in P, when I use:

if ($) send target, event, payload;

with retry logic using a Timer, it seems the model checker could legally explore a trace where nondeterminism always chooses false, leading to infinite retries. Even though the probability of this trace is low, with sufficient exploration and a low step count it might appear and violate liveness properties.

My questions:

1. Is my understanding correct that if($) allows unbounded failure sequences?
2. What is the recommended pattern in P to model transient (not permanent) network failures?
3. Does using choose(N) with bounded probabilities (e.g., if (choose(100) >= 5)) combined with retry counters adequately capture "eventual success" semantics similar to TLA+ fairness? Or does it introduce a flawed model that prioritizes happy paths and might ignore errors as discussed in Adding Probabilistic Choose() in P #526

Context: I’m verifying an outbox pattern with at-least-once delivery guarantees and liveness specs that require eventual completion under the assumption of transient errors.