Skip to content

Recursive process calls fails because of too strict checking

When running the code below, we get the following error: figure-3-15-process_decl.modest:(16,28): error: Cannot read local variables or process parameters immediately before a recursive process call.

If I interpreted Arnd's critique correctly, in this case we should be able to make a recursive process call since we don’t change the variable.

//---Property which should always hold---
const int check = 1;
property Term = Pmin(<> (check == 1)) == 1;
//---------------------------------------

action snd_data, rcv_ack, timeout;
exception err;
int n = 3;

process Sender(int n)
{
    snd_data {= n = n - 1 =};
    alt {
        :: rcv_ack
        :: timeout; alt {
            :: when(n > 0) Sender(n)
            :: when(n == 0) throw(err)
        }
    }
}

Sender(2)