mb structures Sections GenAutomata Doc

Def loc(E) == 1of(2of(2of(2of(E))))

is mentioned by

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

mb structures Sections GenAutomata Doc