Installation Guide¶

• Table of contents
• Installation Guide
  • Before we start: setting environment variables
    • Windows
    • Linux
  • Retrascope Installation
  • What's next?

Before we start: setting environment variables¶

Several steps below require environment variable to be set in your OS. When you encounter such step in the guide, do the following (substitute NAME and VALUE by the name and value of your environment variable respectively):

Windows¶

1. Open the System Properties window.
2. Switch to the Advanced tab.
3. Click on Environment Variables.
4. Click New... under System Variables.
5. In the New System Variable dialog specify variable name as NAME and variable value as VALUE.
6. Click OK on all open windows.
7. Reopen the command prompt window.

Linux¶

Add the command below to the ~/.bash_profile or ~/.bashrc file (Linux):

export NAME=VALUE

Changes will be applied after restarting the command-line terminal or reboot. You can also execute the command in your command-line terminal to make temporary changes.

Retrascope Installation¶

1. Download and install JDK 11 (use AdoptOpenJDK for Windows and openjdk-11-jdk for Ubuntu Linux based OS).
2. Download and install SMT-LIBv2 solver Z3 version 4.3 or higher.
3. Set SMT_SOLVER_PATH environment variable to a full path to SMT-solver executable (like "/home/user/z3/bin/z3" or "C:\tools\z3\bin\z3.exe").
4. Retrascope uses *nuXmv* or *NuSMV* to perform model checking.
   Due to license limitations, we recommend to use NuSMV for commercial projects and nuXmv for non-commercial ones.
   Choose the most suitable model checker and do the following:
   1. To use nuXmv:
      1. Download and install nuXmv model checker.
      2. Set NUXMV_PATH environment variable to a full path to nuXmv executable (like "/home/user/nuxmv/nuXmv" or "C:\tools\nuxmv\nuXmv.exe").
   2. To use NuSMV:
      1. Download and install NuSMV model checker.
      2. Set NUSMV_PATH environment variable to a full path to NuSMV executable (like "/home/user/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").
5. For VHDL designs elaboration:
   1. Set ZAMIA_LOCKING environment variable to true.
   2. Download and install Python interpreter.
6. Download and unpack the Retrascope.

To make sure the tool is successfully installed use '--check' command line option.
Enter the retrascope installation directory and run the following command for Windows OS:

>bin\retrascope.bat --check
Retrascope version: 1.1.3-beta-SNAPSHOT

2020.02.17 17:11:30.258. INFO: SMT solver is installed here: C:\Program Files\z3\bin\z3.exe
2020.02.17 17:11:30.298. INFO: Z3 version 4.3.2

2020.02.17 17:11:30.308. WARNING: 'NUSMV_PATH' env variable is not set.
2020.02.17 17:11:30.308. INFO: nuXmv is installed here: C:\Program Files\nuxmv\nuXmv.exe
2020.02.17 17:11:31.288. INFO: *** This is nuXmv 1.0.1 (compiled on Mon Nov 17 16:54:49 2014)

2020.02.17 17:11:31.288. WARNING: Set 'ZAMIA_LOCKING' environment variable to 'true' for VHDL designs processing
2020.02.17 17:11:31.318. INFO: Python 3.8.1

For Linux-based OS:

$ ./bin/retrascope --check
Retrascope version: 1.1.3-beta-SNAPSHOT

2020.02.14 17:20:23.717. INFO: SMT solver is installed here: /home/tools/z3-4.7.1-x64-ubuntu-16.04/bin/z3
2020.02.14 17:20:23.759. INFO: Z3 version 4.7.1 - 64 bit

2020.02.14 17:20:23.759. WARNING: 'NUSMV_PATH' env variable is not set.
2020.02.14 17:20:23.760. INFO: nuXmv is installed here: /home/tools/nuxmv-1.0.1-linux-x86_64/nuXmv
2020.02.14 17:20:23.774. INFO: *** This is nuXmv 1.0.1 (compiled on Mon Nov 17 16:49:54 2014)

2020.02.14 17:20:23.774. INFO: 'ZAMIA_LOCKING' environment variable is set to 'true'
2020.02.14 17:20:23.776. INFO: Python 2.7.17

It is ok to have only one model checker installed (NuSMV or nuXmv).

What's next?¶

1. To understand the main concept of the Retrascope architecture see Overview
2. For quick overview of common use cases see Getting Started
3. For full guide of the tool options see Command Line Options
4. To understand the scientific foundations of the tool see Retrascope-Related Publications