In Module USER Transition NON_DETERMINISTIC_IDLE_OR_ENTERING has non-deterministic assignment to user_state with {idle,entering}
In Module USER Transition NON_DETERMINISTIC_CRITICAL_OR_EXITING has non-deterministic assignment to user_state with {critical,exiting}