is mentioned by

Thm* E:EventStruct. msg(E) |E||MS(E)|	[event_msg_wf]
Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2))	[event_msg_eq]
Def < A,evt,tg > (E) == < A,MS(E),msg(E) o evt,loc(E) o evt,is-send(E) o evt,tg, >	[induced_tagged_event_str]
Def induced_event_str(E;A;f) == < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, >	[induced_event_str]

Try larger context: GenAutomata