In automated verification of protocols, one source of complications is that channels may have unbounded capacity, in which case a naive model of the protocol is no longer finite state. Symbolic techniques have therefore been developed for representing the contents of unbounded channels. In [AJ01a], some of these techniques are surveyed and applied to a simple leader election protocol. The protocols that are considered have entities modeled as finite state machines which communicate by sending messages from a finite alphabet over unbounded channels; this is a framework for which many techniques have been developed. A more general model is also considered, in which messages may belong to an unbounded domain of values which may be compared according to a total ordering relation: The motivation is to study protocols with timestamps or priorities. The authors show how techniques from the previous setting can be extended to this more general model, but also show that reachability quickly becomes undecidable if channels preserve the ordering between messages.