Merge pull request #253 from sammsaski/formalise25-AEfixes

Addressing AE reviewer feedback for FormaliSE25 submission

Author: ttj

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "code/nnv/engine/cora"]
 	path = code/nnv/engine/cora
 	url = https://github.com/verivital/CORA.git
+[submodule "code/nnv/examples/Submission/FORMALISE2025/npy-matlab"]
+	path = code/nnv/examples/Submission/FORMALISE2025/npy-matlab
+	url = https://github.com/verivital/npy-matlab.git

code/nnv/examples/Submission/FORMALISE2025/README.md

@@ -2,67 +2,132 @@
 
 This artifact is used to reproduce the results in _Robustness Verification of Video Classification Neural Networks_.
 
+Included in the artifact are the NNV tool, datasets, and scripts used to produce all of the results in the aforementioned paper. The paper introduces a novel abstract set representation for handling layer types common to video classification neural network architectures (3D convolutional, 3D pooling, etc.). The implementation of this abstract set representation is done within the NNV tool, which results in its inclusion in the artifact. Specifically, there exists a subdirectory (`nnv/code/nnv/examples/Submission/FORMALISE2025`) of the artifact which contains the scripts necessary to using the NNV tool for verification and producing the results in the paper.
+
 All results from _Robustness Verification of Video Classification Neural Networks_ were captured using an `Apple M1 Max 10-core [email protected]×10` with 64GB of RAM.
 
 # Requirements
 
 The following resources are required to run this artifact:
 
-- MATLAB 2024a with NNV and `npy-matlab` installed and added to the path.
+- MATLAB 2024a with the NNV tool and `npy-matlab` packages installed and added to the path as well as the following toolboxes installed:
+  - Computer Vision
+  - Control Systems
+  - Deep Learning
+  - Image Processing
+  - Optimization
+  - Parallel Computing
+  - Statistics and Machine Learning
+  - Symbolic Math
+  - System Identification
+  - [Deep Learning Toolbox Converter for ONNX Model Format](https://www.mathworks.com/matlabcentral/fileexchange/67296-deep-learning-toolbox-converter-for-onnx-model-format)
 - A conda environment with Python v3.11. Install rquirements from `requirements.txt`. Make sure to install the source files.
+- The datasets which are available for download here: https://doi.org/10.5281/zenodo.14721214
 
 # Installation
 
 This section describes all of the necessary steps for installing tools, dependencies, etc. needed to reproduce the artifact. For the remainder of these instructions when the `FORMALISE2025` directory is referred to we are really referring to the directory at the following path: `nnv/code/nnv/examples/Submission/FORMALISE2025`.
 
-1. Clone NNV and `npy-matlab` and install them ensuring that both have been added to the MATLAB path.
+1. Clone the NNV repository (or download artifact for reviewers accessing this way) and ensure all dependencies have been added to the MATLAB path.
 
-```
-# Clone NNV and npy-matlab
-git clone --recursive https://github.com/verivital/nnv.git
-git clone https://github.com/kwikteam/npy-matlab.git
-```
+   ```
+   # Clone NNV
+   git clone --recursive https://github.com/verivital/nnv.git
+   ```
 
-Follow the instructions under heading `# Installation:` on [NNV's README](https://github.com/verivital/nnv/blob/master/README.md). Note, if using a computer with an Apple silicon CPU, then it may be necessary to remove the following line from NNV's `install.m` script:
+   Next, we provide instructions for installing both pieces of software as needed for using the artifact. Note that it will be necessary to perform installations with administrator privileges for both pieces of software so that it is possible to `savepath` in MATLAB after completing their respective installation instructions.
 
-```matlab
-tbxmanager install lcp hysdel cddmex clpmex glpkmex fourier sedumi;
-```
+2. Install the NNV tool
 
-Either comment it out or remove it.
+   To setup the NNV tool, there are a number of toolboxes that we need to first install. Assuming you have already installed MATLAB R2024a, then you can use the `nnv/install_ubuntu.sh` if you are on an Ubuntu machine to speedup this process. Otherwise, you will need to ensure that the toolboxes mentioned under [Requirements](#requirements) are included in your MATLAB installation.
 
-For `npy-matlab`, add and save the path to MATLAB. Again, instructions are available on [`npy-matlab`'s README](https://github.com/kwikteam/npy-matlab/blob/master/README.md).
+   Additionally, you must install the following support package [Deep Learning Toolbox Converter for ONNX Model Format](https://www.mathworks.com/matlabcentral/fileexchange/67296-deep-learning-toolbox-converter-for-onnx-model-format).
 
-> NOTE: It will be necessary to perform installations with administrator privileges for both of these tools so that it is possible to `savepath` in MATLAB after completing their respective installation instructions.
+   > Note: Support packages can be installed in MATLAB's HOME tab > Add-Ons > Get Add-ons, search for the support package using the Add-on Explorer and click on the Install button.
 
-2. Download the following dataset files from [here](https://drive.google.com/drive/folders/1sXRtSObHLBTeKVss2IA-NGPKljirgD8D?usp=drive_link) into the `FORMALISE2025/data` folder so that the file tree now looks like
+   After completing the initial steps, the next step is to run the `nnv/code/nnv/install.m` script in MATLAB. If using a computer with an Apple silicon CPU, then it may be necessary to remove the following line from NNV's `install.m` script:
 
-```pseudo
-FORMALISE2025
-├── data
-│   ├── ZoomIn
-│   ├── ZoomOut
-│   ├── GTSRB
-│   └── STMNIST
-...
-```
+   ```matlab
+   tbxmanager install lcp hysdel cddmex clpmex glpkmex fourier sedumi;
+   ```
 
-Note that the `GTSRB` data folder is quite large, so it will likely be downloaded in separate parts. Please make sure the organization of the folder is the same as in the download link and that all filenames match.
+   Either comment it out or remove it.
 
-3. Create a conda environment with `Python v3.11` and install the requirements from `requirements.txt`. Instructions for installing conda can be found [here](https://docs.conda.io/projects/conda/en/latest/user-guide/install/) with links under `# Regular installation` to instructions for various operating systems. After confirming that conda has installed successfully by creating a conda environment and making it active, proceed to install the requirements as detailed below. In addition to installing from `requirements.txt`, you must install the source files to the environment. Both of these can be done by running the following commands from the root directory (`FORMALISE2025`):
+   > Note: if you restart Matlab, rerun either `install.m` or `startup_nnv.m`, which will add the necessary dependencies to the path; you alternatively can run savepath after installation to avoid this step after restarting Matlab, but this may require administrative privileges
 
-```bash
-# installing requirements
-pip install -r requirements.txt
+   All of these instructions are additionally included under heading `# Installation:` on [NNV's README](https://github.com/verivital/nnv/blob/master/README.md). Note, if using a computer with an Apple silicon CPU, then it may be necessary to remove the following line from NNV's `install.m` script:
 
-# before installing source files, make sure to navigate to this src directory, e.g.
-cd /path/to/FORMALISE2025/src
-pip install -e .
-```
+3. Install the `npy-matlab` package
+
+   For `npy-matlab`, add and save the path to MATLAB with the following commands from the MATLAB interface:
+
+   ```matlab
+   >> addpath('/path/to/npy-matlab/npy-matlab')
+   >> savepath
+   ```
+
+   For reference, the `npy-matlab` package is included in this artifact inside the `FORMALISE2025` directory.
+
+   Instructions are also available on [`npy-matlab`'s README](https://github.com/kwikteam/npy-matlab/blob/master/README.md).
+
+4. Download the `data.tar.gz` file which contains all variations of datasets needed for reproducing results in the desired file structure from the following link: https://doi.org/10.5281/zenodo.14721214.
+
+   After downloading the file, move it to the `FORMALISE2025` directory and unpack it there (`tar -xzf data.tar.gz` if possible, but can also extract files using whatever file explorer is available on machine) so that the file tree now looks like
+
+   ```pseudo
+   FORMALISE2025
+   ├── data
+   │   ├── ZoomIn
+   │   ├── ZoomOut
+   │   ├── GTSRB
+   │   └── STMNIST
+   │   └── data.tar.gz
+   ...
+   ```
+
+   after which the `data.tar.gz` file can be deleted. Please make sure the organization of the folder is the same as shown above.
+
+5. Create a conda environment with `Python v3.11` and install the requirements from `requirements.txt`.
+
+   For producing the results, the Anaconda distribution was used so its installation instructions are provided here; users can also follow general installation instructions [here](https://docs.conda.io/projects/conda/en/latest/user-guide/install/). When installing Anaconda in macOS, a `.pkg` file will be provided. Double-click the `.pkg` file and follow the prompts to install Anaconda. For Linux, a `.sh` script will be provided. Executing the command `bash anaconda-latest-Linux-x86_64.sh` and following the prompts will install Anaconda.
+
+   To activate conda in your terminal environment, you will have to restart it. Then, you can test that the installation was successful with
+
+   ```bash
+   conda list
+   ```
+
+   We can then create a `Python v3.11` environment with command
+
+   ```bash
+   conda create --name <env_name> python=3.11
+   ```
+
+   Then, activate the environment with and check its Python version
+
+   ```bash
+   conda activate <env_name>
+   python --version
+   ```
+
+   After the environment is activated, install the Python dependencies from `requirements.txt` along with the source files by running the following commands from the `FORMALISE2025` directory in your terminal
+
+   ```bash
+   cd /path/to/nnv/code/examples/Submission/FORMALISE2025
+
+   # install requirements
+   pip install -r requirements.txt
+
+   # before installing source files, make sure to navigate to the src directory e.g.
+   cd src/ # from FORMALISE2025 directory
+   pip install -e .
+   ```
+
+   Now all Python dependencies have been installed.
 
-4. Modify the `.env` file to add the path to your NNV and npy-matlab directories (the repositories that were cloned earlier). For the `npy-matlab` repository, you'll want to reference the subfolder in the directory also called `npy-matlab`, e.g. `/some/path/to/npy-matlab/npy-matlab`.
+6. Modify the `.env` file to add the path to your NNV and npy-matlab directories (the repositories that were cloned earlier). For the `npy-matlab` repository, you'll want to reference the subfolder in the directory also called `npy-matlab`, e.g. `/some/path/to/npy-matlab/npy-matlab`.
 
-5. With all of these steps done, you are now ready to begin reproducing the artifacts.
+7. With all of these steps done, you are now ready to begin reproducing the artifacts.
 
 # Smoke Test Instructions (~1min)
 
@@ -93,7 +158,7 @@ Assuming the average runtime for the experiments remains as shown in the paper,
 3. Run the following command to begin reproducing a subset of the artifacts:
 
 ```bash
-chmod +x run_subset_vvn.sh && run_subset_vvn.sh
+chmod +x run_subset_vvn.sh && ./run_subset_vvn.sh
 ```
 
 # Reproducing a Subset of the Results pt. 2
@@ -105,7 +170,7 @@ There is additionally a script to reproduce a single sample from all variations
 3. Run the following command to begin reproducing a subset of the artifacts:
 
 ```bash
-chmod +x run_single_sample_vvn.sh && run_single_sample_vvn.sh
+chmod +x run_single_sample_vvn.sh && ./run_single_sample_vvn.sh
 ```
 
 # Reproducing the Full Results