\chapter{Installation}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{System Requirements}

MicroTESK is a set of Java-based utilities that are run from the command line.
It can be used on \textbf{\textit{Windows}}, \textbf{\textit{Linux}} and
\textbf{\textit{OS X}} machines that have \textbf{\textit{JDK 1.7 or later}}
installed. To build MicroTESK from source code or to build the generated
Java models, \textbf{\textit{Apache Ant version 1.8 or later}} is required.
To generate test data based on constraints, MicroTESK needs
the \textbf{\textit{Microsoft Research Z3}} or \textbf{\textit{CVC4}} solver that
can work on the corresponding operating system.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Installation Steps}

To install MicroTESK, the following steps should be performed:

\begin{enumerate}
  \item Download from \url{http://forge.ispras.ru/projects/microtesk/files} and unpack
        the MicroTESK installation package (the \texttt{.tar.gz} file, latest release) to your
        computer. The folder to which it was unpacked will be further referred to as
        the installation directory (\texttt{<installation dir>}).

  \item Declare the \texttt{MICROTESK{\_}HOME} environment variable and set its value to the path to
        the installation directory (see the \hyperref[Setting_Environment_Variables]
        {Setting Environment Variables} section).

  \item Set the \texttt{<installation dir>/bin} folder as the working directory (add the path to
        the \texttt{PATH} environment variable) to be able to run MicroTESK utilities from any path.

  \item Note: Required for constraint-based generation. Download and install constraint
        solver tools to the \texttt{<installation dir>/tools} directory (see the
        \hyperref[Installing_Constraint_Solvers]{Installing Constraint Solvers} section).
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Setting Environment Variables}
\label{Setting_Environment_Variables}

\paragraph{Windows}

\begin{enumerate}
  \item Open the \texttt{System Properties} window.
  \item Switch to the \texttt{Advanced} tab.
  \item Click on \texttt{Environment Variables}.
  \item Click \texttt{New..} under \texttt{System Variables}.
  \item In the \texttt{New System Variable} dialog, specify variable name as
        \texttt{MICROTESK{\_}HOME} and variable value as \texttt{<installation dir>}.
  \item Click \texttt{OK} on all open windows.
  \item Reopen the command prompt window.
\end{enumerate}

\paragraph{Linux and OS X} ~\\

Add the command below to the \texttt{\textasciitilde{}.bash{\_}profile} file
(\textbf{\textit{Linux}}) or the \texttt{\textasciitilde{}/.profile} file (\textbf{\textit{OS X}}):

\begin{lstlisting}[language=bash]
export MICROTESK_HOME=<installation dir>
\end{lstlisting}

To start editing the file, type \texttt{vi \textasciitilde{}/.bash{\_}profile}
(or \texttt{vi \textasciitilde{}/.profile}).
Changes will be applied after restarting the command-line terminal or reboot. You can also
run the command in your command-line terminal to make temporary changes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Installing Constraint Solvers}
\label{Installing_Constraint_Solvers}

To generate test data based on constraints, MicroTESK requires external constraint solvers.
The current version supports the \href{https://github.com/z3prover}{Z3} and
\href{http://cvc4.cs.nyu.edu}{CVC4} constraint solvers. Constraint executables should be
downloaded and placed to the \texttt{<installation dir>/tools} directory.

\paragraph{Using Environment Variables} ~\\

If solvers are already installed in another directory, to let MicroTESK find them, the following
environment variables can be used: \texttt{Z3{\_}PATH} and \texttt{CVC4{\_}PATH}. They specify
the paths to the Z3 and CVC4 excutables correspondingly.

\paragraph{Installing Z3}

\begin{itemize}
\item \textbf{\textit{Windows}} users should download Z3 (32 or 64-bit version) from the following
       page:\url{http://z3.codeplex.com/releases} and unpack the archive to the
      \texttt{<installation dir>/tools/z3/windows} directory. Note: the executable file path
      is \texttt{<windows>/z3/bin/z3.exe}.

\item \textbf{\textit{UNIX}} and \textbf{\textit{Linux}} users should use one of the links below
      and and unpack the archive to the \texttt{<installation dir>/tools/z3/unix} directory.
      Note: the executable file path is \texttt{<unix>/z3/bin/z3}.

      \begin{tabular} {| l | r |} \hline
      Debian  x64 & \url{http://z3.codeplex.com/releases/view/101916} \\ \hline
      Ubuntu  x86 & \url{http://z3.codeplex.com/releases/view/101913} \\ \hline
      Ubuntu  x64 & \url{http://z3.codeplex.com/releases/view/101911} \\ \hline
      FreeBSD x64 & \url{http://z3.codeplex.com/releases/view/101907} \\ \hline
      \end{tabular}

\item \textbf{\textit{OS X}} users should download Z3 from
      \url{http://z3.codeplex.com/releases/view/101918} and unpack the archive to the
      \texttt{<installation dir>/z3/osx} directory. Note: the executable file path is
      \texttt{<osx>/z3/bin/z3}.

\end{itemize}

\paragraph{Installing CVC4}

\begin{itemize}
\item \textbf{\textit{Windows}} users should download the latest version of CVC4 binary from
      \url{http://cvc4.cs.nyu.edu/builds/win32-opt/} and save it to the
      \texttt{<installation dir>/tools/cvc4/windows} directory as \texttt{cvc4.exe}.

\item \textbf{\textit{Linux}} users download the latest version of CVC4 binary from
      \url{http://cvc4.cs.nyu.edu/builds/i386-linux-opt/unstable/} (32-bit version) or
      \url{http://cvc4.cs.nyu.edu/builds/x86_64-linux-opt/unstable/} (64-bit version) and
      save it to the \texttt{<installation dir>/tools/cvc4/unix} directory as \texttt{cvc4}.

\item \textbf{\textit{OS X}} users should download the latest version of CVC4 distribution
      package from \url{http://cvc4.cs.nyu.edu/builds/macos/} and install it.
      The CVC4 binary should be copied to \texttt{<installation dir>/tools/cvc4/osx} as
      \texttt{cvc4} or linked to this file name via a symbolic link.

\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Installation Directory Structure}

The MicroTESK installation directory contains the following subdirectories: \\

\begin{tabular}{ | l | l |}
  \hline
  \textbf{arch} & Microprocessor specifications and test templates \\ \hline
  \textbf{bin}  & Scripts to run modeling and test generation tasks \\ \hline
  \textbf{doc}  & Documentation \\ \hline
  \textbf{etc}  & Configuration files \\ \hline
  \textbf{gen}  & Generated code of microprocessor models \\ \hline
  \textbf{lib}  & JAR files and Ruby scripts to perform modeling and \\
  ~             & test generation tasks \\ \hline
  \textbf{src}  & Source code of MicroTESK \\ \hline
\end{tabular}

