When analysing the behavior of complex networked systems, it is often the
case that some components within that network are only known to the extent
that they belong to one of a set of possible ``implementations''---e.g.,
versions of a specific protocol, class of schedulers, etc. In this report
we augment the specification language considered in [BUCS-TR-2004-021],
[BUCS-TR-2005-014], [BUCS-TR-2005-015], and [BUCS-TR-2005-033], to include
a non-deterministic multiple-choice let-binding, which allows us to
consider compositions of networking subsystems that allow for looser
component specifications.