Comment by nrfulton

Maybe I'm missing something here, but the last type matches 2 pretty well. For example,

> None of that mattered at the scope we were modeling, so we abstracted it all away: "on receiving message, nondeterministically enter state A, B, or C."

That sounds like the author is describing an NFA.

> whereby we execute all the future possibilities... e.g. "amb" operator

Isn't "execute all possibilities" closer to the dual of amb than it is to amb? At least in terms of how the denotation of amb is operationalized.

But it is a good point that sometimes you want to give an actual operational meaning to a literal non-determinism operator.