the only way to escape the 'while 1' loop was depending on changes on the state
variable, which was, before this fix, using the invariant tdef instead of
transition