Installation Guide

This document contains instructions to install following software/libraries on Ubuntu OS:

Lustre/Heptagon

The installation of all software/libraries has been tested on Ubuntu 16.04, 18.04 and 22.04. We recommend you to use one of these versions of Ubuntu OS. These software have to be installed ONLY ON 64-bit OS.

Refer the Video for installing Ubuntu on Virtual Machine

Lustre/Heptagon:

Lustre v4 Installation

Please download the appropriate distribution of Lustre V4 from here.

NOTE: For Ubuntu 20, you can use lustre-v4-III-dc-linux64.tgz from this link

Once you download the distribution, extract the folder and make sure to copy the folder in following directory using command given below:
```
sudo cp -R lustre-v4-IV.2023.293-linux64 /usr/local/
```
Now after unzipping and copying the tarball file, installation will be completed by setting up two environment variables.
- You can go through the instructions provided in this README.
- Or follow the following steps:
- Add Lustre V4 to your shell's configuration, considering that your shell type is Bash enter the below lines in ~/.bashrc file as below. First open the .bashrc file in any editor like Nano, Gedit, etc.
```
export LUSTRE_INSTALL=/usr/local/lustre-v4-IV.2023.293-linux64
source $LUSTRE_INSTALL/setenv.sh
```
- After configuring Lustre in your shell, run the following command to source the configuration.
```
source ~/.bashrc
```
That was alll for Lustre V4 installation.

Heptagon Installation

First step is to install opam which is a source-based package manager for OCaml. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

To install opam run the following command in your terminal.

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

Next we will have to install some prerequisite libraries, to install same run the below command in your terminal.
```
sudo apt-get install -y m4 make wget patch unzip bubblewrap git g++
```
If you cannot find Bubblewrap (ISSUE on 16.04), install it from http://ftp.ubuntu.com/ubuntu/pool/universe/b/bubblewrap/ and then continue with the rest of the steps.
After this we need to install Heptagon and it's dependencies. To do the same run the following commands:

NOTE: You have to execute all these commands in the same terminal session.
```
opam init
```
- After running the above command it should automatically source ~/.bash_profile or ~/.profile by defualt. If it doesn't you need to source either of the file manually. It will be specified in the text you get after running opam init.
```
eval $(opam env)
```
```
opam switch create 4.03.0
```
```
eval $(opam env)
```
- Install few more libraries using following commands:
```
sudo apt-get install libgtk2.0-dev
```
```
opam install menhir lablgtk ocamlgraph ocamlbuild camlp4
```
Next we need to download Hetpagon and unzip it.

After unzipping the folder, run the following commands in your terminal:

cd </path/to/where/you/unzipped>/heptagon-1.05.00/

./configure && make

sudo make install

You have Heptagon installed in your system. You should have “heptc” and “hepts” binaries linked to your path. You can verify that by autocompleting on “heptc” or “hepts” or by typing it on the terminal.

Note: The simulator “hepts” depends on “sim2chro” so you must have Lustre v4 installed to be able to use it.

Testing

Now to test installation follow the steps given below.
- Download the following files:
  1. try1.ept
  2. simulate.sh
  simulate.sh is utility script for simulating Heptagon nodes.
- After downloading above files make sure to run following in the directory where you have downloaded simulate.sh.
```
chmod u+x simulate.sh
```
- After everything is in place let's simulate our heptagon node. To do same we need to execute simulate.sh with name of the node and path to heptagon file.
```
./simulate.sh -s <name-of-node> -p </path/to/heptagon/code.ept>
```
Example:
```
./simulate.sh -s minsquare -p try1.ept
```
- Optionally you can put this script in your path and use it from anywhere. At the end of your ~/.bashrc or ~/.bash_profile, add following.
```
export PATH="$PATH:/home/erts/Course/Test/"
```
- where simulate.sh is contained in /home/erts/Course/Test directory
- Finally run the following command to simulate our heptagon node.
Example:
```
simulate.sh -s minsquare -p try1.ept 
```

Troubleshooting

If you are facing issues with executing heptagon node, first check whether the below two lines are present inside the bashrc, if not then manually add the lines to bashrc.
```
 export LUSTRE_INSTALL=/usr/local/lustre-v4-IV.2023.293-linux64
 source $LUSTRE_INSTALL/setenv.sh   
```

Heptagon Patch for Reset

There were two initialization related bugs in the reset phase after state machine.
Please replace the file in the folder heptagon-1.05.00/compiler/heptagon/trasnformation/reset.ml with the attached reset.ml file.
Once done, recompile the heptagon by following running following commands inside heptagon-1.05.00 directory:
```
./configure && make
```
```
sudo make install
```

Type Conversion in Heptagon

To use type conversion in heptagon, follow the following steps:

Copy paste the following files inside the working directory, where you have your .ept file.
In your .ept,
- Include mc_ext by using: open Mc_ext
- For int to float conversion use: float_of_int(val)
- For float to int conversion use: int_of_float(val)
Use the updated simulate.sh to run the heptagon code.

For reference, example is provided here: type_convesion.tar.gz Download the file. Extract it and run the following command:

./simulate.sh -s main -p type_conversion.ept

CS684 Spring 2024-25