Efficient recognition of trace languages defined by repeat-until loops