Skip to content

Installation #

Prerequisites #

Install Hanfor #

To get Hanfor either download the .zip file or clone the repository.

Download .zip file #

Download Hanfor and unzip it. Rename the root folder hanfor-master to hanfor.

mv hanfor-master hanfor

move hanfor-master hanfor

Clone the repository #

git clone https://github.com/ultimate-pa/hanfor.git -b master --single-branch

Install dependencies #

We recommend using a virtual environment.

cd hanfor/hanfor
python -m venv hanfor_venv
source hanfor_venv/bin/activate

cd hanfor\hanfor
python -m venv hanfor_venv
hanfor_venv\Scripts\activate.bat

Install all Python dependencies. 

pip install -r requirements.txt

Install the Z3 Theorem Prover. 

pysmt-install --z3

Configuration #

Copy the default config file config.dist.py to config.py.

cp config.dist.py config.py

copy config.dist.py config.py

The config file config.py allows you to change various parameters -- see the comments in config.dist.py.

Copy the default ultimate config file configuration/ultimate_config.dist.py to configuration/ultimate_config.py.

cp configuration/ultimate_config.dist.py configuration/ultimate_config.py

copy configuration\ultimate_config.dist.py configuration\ultimate_config.py

The config file ultimate_config.py allows you to change various parameters for the ultimate backend -- see the comments in ultimate_config.dist.py.

Launch a Hanfor session #

Launch a new session #

python app.py <tag> -c <path_to_input_csv>
1. This creates a new session named by <tag> in the SESSION_BASE_FOLDER. 2. It asks the user for a mapping of the following .csv header names. * "ID" * "Description" * "Formalized Requirement" * "Type" 3. It reads requirements from the .csv file and stores them in separate files in the SESSION_BASE_FOLDER. 4. It serves the web interface on HOST and PORT.

Open the web interface in your web browser at http://<HOST>:<PORT>.

Launch an existing session #

python app.py <tag>
To see all available tags use the -L switch. 
python app.py -L
Open the web interface in your web browser at http://<HOST>:<PORT>.

ReqAnalyzer #

With Hanfor you can formalize requirements and export them. Ultimate ReqAnalyzer is a tool to analyze the formalized requirements and part of the released tools of Ultimate.

Variant 1: Use the latest release #

  1. Install Java JRE (11)
  2. Download one of the latest nightly builds.
    Depending on your OS, you need to download UReqCheck-linux.zip or UReqCheck-win32.zip.

Variant 2: Build the latest development version #

  1. Install Java JDK (11) and Maven (>=3.6)
  2. Clone the repository: git clone https://github.com/ultimate-pa/ultimate.
  3. Navigate to the release scripts cd ultimate/releaseScripts/default
  4. Build the latest binaries by executing ./makeFresh.sh. This also works on Windows if you use a bash shell (e.g., from WSL or GitBash).

After a successful build, the binaries are located in UReqCheck-linux and UReqCheck-win32, respectively.

In the Workflow section we explain how to use the tool.