Colours of enabled operations

The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is taken:

blue  
The operation does not change the state (behaves like skip).
green  
The operation leads to a new, not yet explored state.
red  
The operation leads to a state where the invariant is violated.
orange 
The operation leads to a deadlock state, i.e. a state where no operation is enabled.
black 
Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither an invariant violating or deadlock state.