GenAutomata
Sections
NuprlLIB
Doc
Def
No-dup-deliver(E)(tr) ==
i,j:
||tr||.
(is-send(E)(tr[i]))
(is-send(E)(tr[j]))
(tr[j] =msg=(E) tr[i])
loc(E)(tr[i]) = loc(E)(tr[j])
i = j
is mentioned
In prior sections:
mb
hybrid
GenAutomata
Sections
NuprlLIB
Doc