Questions about FailureInjector.p

[dtornow]

Hello,

I have two questions about the FailureInjector, specifically about the FailOneState

state FailOneNode 
{
    entry 
    {

        var fail: machine;

        if(nFailures == 0)
        {
            raise halt; // done with all failures
        }
        else
        {
            if($)
            {
                fail = choose(nodes);
                send fail, eShutDown, fail;
                nodes -= (fail);
                nFailures = nFailures - 1;
            }
            else 
            {
                send this, eDelayNodeFailure;
            }
        }
    }

    on eDelayNodeFailure goto FailOneNode;
  
}

Missing Loop

AFAIU the state machine does not loop i.e. if the FailureInjector fails one node it will never fail another node again. We could rectify this situation by raising another eDelayNodeFailure in the if($) clause.

That leads me to my second, more nuanced question

Unnecessary Requeue

AFAIU a p state machine has its own inbox, the delivery of events is managed by the p runtime to control the interleaving of messages.

Looks to me like the code implements the idea of "randomly fail or do not fail".

Since the p runtime delivers event "randomly", we are encoding on an application level what is already encoded on a runtime level, increasing the state space exploration necessary without increasing the coverage?

Conclusion

Would this code be sufficient?

state FailOneNode 
{
    entry 
    {

        var fail: machine;

        if(nFailures == 0)
        {
            raise halt; // done with all failures
        }
        else
        {
            fail = choose(nodes);
            send fail, eShutDown, fail;
            // nodes -= (fail); // uncomment to ensure a node may failure at most once
            nFailures = nFailures - 1;

            // the p runtime already ensures this will be delivered sometimes in the future, no need to "busy loop"
            send this, eDelayNodeFailure;
        }
    }

    on eDelayNodeFailure goto FailOneNode;
  
}