Diverging behavior due to terminal state detection

[AlexBork]

The detection of terminal states in the model building leads to unexpected, diverging behavior. Consider for example the following MDP

mdp

module model
    s : [0..4] init 0;
    
    [a] s=0 -> 0.5 : (s'=1)+ 0.5 : (s'=2) ;
    [a] s=1 -> 1 : (s'=3);
    [a] s=2 -> 1 : (s'=3);

    [a] s=3 -> 1 : (s'=4);
    [a] s=4 -> 1 : true;
    [b] true -> 1 : true;

endmodule

label "bad" = s=1;

For property Pmax=? [(!(s = 1)) U (s=3)], the resulting MDP has 4 states, while for property Pmax=? [(! "bad") U (s=3)] it has 5. This is due to the states (s=1) and (s=3) being detected as terminal in the former case but not the latter, causing (s=4) to be explored in the latter case.

In particular, in function getTerminalStatesFromFormula in src/storm/builder/TerminalStatesGetter.cpp, the formula (! "bad") is not detected to be atomic while (!(s = 1)) is. This can be confusing as such cases can result in large differences in model size while semantically the formulae are equivalent.