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)
```
issue