Statespace contains unreachable states
Problem: In the following example, state should always be equal to global_state. However, the export shows this is not always the case. Interestingly, the problem dissapears when we move the safe and risk action from after the weights to before the palt,
Code:
action start, safe, risk, finish, close, reset;
int global_state = 0;
property p1 = Pmax(<> (global_state == 2));
process Server(int state)
{
alt {
:: when(state == 0) start {= state = 1, global_state = 1 =}
:: when(state == 1) alt {
:: palt {
:6: safe {= state = 0, global_state = 0 =}
:3: safe {= state = 2, global_state = 2 =}
:1: safe {= state = 3, global_state = 3 =}
}
:: palt {
:5: risk {= state = 2, global_state = 2 =}
:5: risk {= state = 3, global_state = 3 =}
}
}
:: when(state == 2) finish {= state = 2, global_state = 2 =}
:: when(state == 3)
alt {
:: close {= state = 3, global_state = 3 =}
:: reset {= state = 0, global_state = 0 =}
}
};
Server(state)
}
Server(0)
Image:
Code 2:
action start, safe, risk, finish, close, reset;
int global_state = 0;
property p1 = Pmax(<> (global_state == 2));
process Server(int state)
{
alt {
:: when(state == 0) start {= state = 1, global_state = 1 =}
:: when(state == 1) alt {
:: safe palt {
:6: {= state = 0, global_state = 0 =}
:3: {= state = 2, global_state = 2 =}
:1: {= state = 3, global_state = 3 =}
}
:: risk palt {
:5: {= state = 2, global_state = 2 =}
:5: {= state = 3, global_state = 3 =}
}
}
:: when(state == 2) finish {= state = 2, global_state = 2 =}
:: when(state == 3)
alt {
:: close {= state = 3, global_state = 3 =}
:: reset {= state = 0, global_state = 0 =}
}
};
Server(state)
}
Server(0)
Image 2: