must be set to true only after elaboration (complete execution of the
first transition).