When exploring the untimed state space of a CIF file that includes requirements, I don't think you'd necessarily get the 'safe' state space (i.e., the state space of only safe behavior wrt. the requirements) but rather the full state space. It may be good to give a warning about this when exploring the state space.