Skip to content

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:

image