mb automata 3 Sections GenAutomata Doc

Def guarded_trace(da;e;I) == r:rel(). r I (k:Label. affects_trace_rel(e;k;r) (t:dec(). t da & t.lbl = k))

is not mentioned in this or prior sections.

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc