Self-loop goes to state -1 in DOT export
Description:
When exporting the following model to DOT, we obtain an incorrect visualization. We should have a self loop in state 6, not a transition to state -1.
Model:
action act;
int reward = 0;
int global_state = 0;
bool final = false;
property dummy = Pmin(<> (global_state == 5));
process Server(int state)
{
alt {
:: when(state == 0) act palt {
:0.5: {= state = 1, global_state = 1 =}
:0.5: {= state = 2, global_state = 2 =}
}
:: when(state == 1) act {= state = 3, global_state = 3 =}
:: when(state == 2) act {= state = 3, global_state = 3 =}
:: when(state == 3) act;
palt {
:0.4: {= state = 3, global_state = 3 =}
:0.4: {= state = 4, global_state = 4 =}
:0.2: {= state = 2, global_state = 2 =}
}
:: when(state == 4) act palt {
:0.5: {= state = 4, global_state = 4 =}
:0.5: {= state = 5, global_state = 5 =}
}
:: when(state == 5) act {= final = true =} //self loop
};
Server(state)
}
Server(0)
Image: