In this section, we will use an example TTM called SAMPLE to
illustrate the workings of the verifier. SAMPLE is a single simple
TTM, i.e. it is not the parallel composition of many TTMs.
An example involving the parallel composition of processes, and using
shared variables, may be found in [#Ost92a##1###]. VERIFY has a <#76#>compose<#76#> command which allows for TTMs to be composed in parallel. It
allows for the possibility of both (a) shared variables, and (b) shared
transitions. Thus, both asynchronous and synchronous communication can
be modelled. Concurrent and nondeterministic behaviour can also be
represented. TTMs can model most features of real-time programs, Petri
Nets, Statecharts and Communicating Sequential Processes. In
particular, TTMs have data variables that can be used to represent
program variables, arrays, records and other data structures.