/* ------------------------------------------------------------------------
MODEL, SPECIFICATION, AND VERIFICATION OF MUSIC
------------------------------------------------------------------------ */

open util/ordering [Time] as trace
open util/integer
open util/ordering [LockRef] as queue
/* ========================================================================
TEMPORAL STRUCTURE
Note that if time has a scope of x, there will be exactly x times and
x-1 real events.
======================================================================== */

...