\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Cloning a Model}
\makeindex
\file{clone-model}
\begin{popup}
  \ctindex{1}{model!cloning}{model-cloning}%
  \tindex{1}{cloning a model}%
  \vspace{-2\baselineskip}%
\subsection*{Cloning a Model} 

On the Toolbox's \textsf{TLC Model Checker} menu, choose \textsf{Clone
Model}.  Choose the model you want to make a copy of, and give it any
name you wish.  Then click \textsf{OK}.
\end{popup}
\makepopup