Update README (not done yet)

README.md

@@ -1,73 +1,80 @@
-Neo
-===
+# Neo
 
-[![GitHub workflow](https://github.com/netarch/neo/workflows/test/badge.svg)](https://github.com/netarch/neo/actions)
-[![Codecov](https://img.shields.io/codecov/c/github/netarch/neo.svg)](https://app.codecov.io/gh/netarch/neo)
-[![GitHub repo size](https://img.shields.io/github/repo-size/netarch/neo.svg)](https://github.com/netarch/neo)
+Neo is a network testing tool that implements concolic network execution. It
+combines symbolic model checking and container-based emulation techniques to
+achieve high-quality network-wide testing for networks that involve stateful
+software components (e.g., software network functions, middleboxes).
 
-Neo is a network testing tool based on the Plankton verification framework. It
-combines explicit-state model checking and emulation techniques to achieve
-high-coverage testing for softwarized networks with middlebox components.
-
-## Table of Contents
+> [!NOTE]
+> For artifact evaluation of JSys, please start at
+> [Artifact Evaluation](/doc/artifact-evaluation.md).
 
+<!--toc:start-->
 - [Neo](#neo)
-  - [Table of Contents](#table-of-contents)
-  - [Environment setup](#environment-setup)
+  - [Dependencies](#dependencies)
   - [Build and install Neo](#build-and-install-neo)
-  - [Usage](#usage)
-  - [Running the examples]
-  - [Understanding the output]
+  - [Basic usage](#basic-usage)
+    - [Running the examples](#running-the-examples)
+    - [Running through run.sh](#running-through-runsh)
+    - [Running Neo directly](#running-neo-directly)
+    - [Understanding the output](#understanding-the-output)
+<!--toc:end-->
+
+## Dependencies
 
+We provide a convenience script `depends/setup.sh` to automatically set up all
+dependencies required to build and run Neo. Currently the script only supports
+Arch Linux and Ubuntu 24.04. Though Neo should also work on other Linux
+distributions, we don't provide official support. Please read `depends/setup.sh`
+for all dependency details if you want to install them manually.
 
-## Environment setup
+After cloning the repository, enter the directory and run:
 
-The following dependencies are needed for Neo.
+```sh
+$ ./depends/setup.sh
+```
 
-- Clang
-- LLVM
-- libnl
-- libelf
-- zlib
-- [spin](https://github.com/nimble-code/Spin)
-- Docker
+(To-do: record the approximate time and memory usage.)
+
+> [!IMPORTANT]
+> After running the setup script, it is crucial to logout and re-login again for
+> the new group configuration to take effect. Otherwise, there may be permission
+> errors from Docker. Alternatively, you could also just reboot the OS and
+> things should just work.
+
+## Build and install Neo
 
-`depends/setup.sh` can be used to automatically set up the environment, but it
-only supports Arch Linux and Ubuntu at the moment. Pull requests are
-appreciated.
+To configure Neo, please run:
 
-After running `depends/setup.sh`, please `logout` and log in again in order to apply the system group configuration modified by the script. If you install the dependencies manually, you can configure the group by running 
 ```sh
-sudo gpasswd -a $USER docker
-logout
+$ ./scripts/configure.sh
 ```
-and logging in again.
 
-Since Neo requires Linux version to be at least 5.4 for [per-packet drop
-monitoring](https://github.com/torvalds/linux/commit/ca30707dee2bc8bc81cfd8b4277fe90f7ca6df1f),
-and Ubuntu 18 ships Linux 4.15 by default, it is recommended to use at least
-Ubuntu 20.04. Otherwise newer kernel versions will need to be manually
-installed.
+(To-do: show the configure options as a drop-down menu.)
+
+> [!NOTE]
+> Running this step for the first time may take a while, because all vcpkg
+> dependencies will have to built during configuration.
+
+To build Neo, simply run:
 
-## Build and install Neo
-To build Neo(excluding the tests), run:
 ```sh
-cd neo
-./scripts/configure.sh
-./scripts/build.sh
+$ ./scripts/build.sh
 ```
+
 The executable will be at `build/neo`.
 
-If you want to build unit tests together with the debug info, replace `./scripts/configure.sh` with `./scripts/configure.sh -t -d`. 
+If you want to build unit tests together with the debug info, replace
+`./scripts/configure.sh` with `./scripts/configure.sh -t -d`.
 
 After building Neo, you can install Neo to system
 paths if desired, with the following command.
 
 ```sh
-sudo DESTDIR=/ ./scripts/install.sh --prefix /usr
+$ sudo DESTDIR=/ ./scripts/install.sh --prefix /usr
 ```
 
-## Usage
+## Basic usage
 
 ```
 Neo options:
@@ -82,17 +89,18 @@ Neo options:
   -o [ --output ] arg          Output directory
 ```
 
-##Running the examples
+### Running the examples
 The examples can be found in `examples/` directory. You can test the examples by running `run.sh` included in the example directories, or optionally by feeding the configuration files directly to Neo.
 
-#Running through run.sh
+### Running through run.sh
 You can try the examples by running `run.sh` in each example directory. This may trigger Neo multiple times with different configurations. The output can be found in `result` directory inside the example directory. For instance, you can try `00-reverse-path-filtering` by executing:
 ```sh
 examples/00-reverse-path-filtering/run.sh
 ```
 The output can be found in `examples/00-reverse-path-filtering/results`.
 
-#Running Neo directly
+### Running Neo directly
+
 If you want to have more control on the execution, you can run the examples by directly feeding Neo the configuration files. Each example either contains TOML configuration files or contains a confgen.py file which generates a TOML file. For instance, `00-reverse-path-filtering` contains two different TOML files, `network.fault.toml` and `network.toml`. Each TOML file corresponds to a network configuration to be tested as well as the invariants of interest. To run Neo with `examples/00-reverse-path-filtering/network.toml` as the input, execute:
 ```sh
 sudo neo -afj8 -i examples/00-reverse-path-filtering/network.toml -o output
@@ -103,12 +111,11 @@ If the example contains `confgen.py` instead, the TOML file must be generated us
 python3 examples/01-subnet-isolation/confgen.py -s 2 -H 2 > examples/01-subnet-isolation/network.toml
 sudo neo -afj8 -i examples/01-reverse-path-filtering/network.toml -o output
 ```
-The output can be found in `output/` directory in the Neo home directory. 
-
-##Understanding the output
+The output can be found in `output/` directory in the Neo home directory.
 
+### Understanding the output
 
-> **Note** <br/>
+> [!NOTE]
 > Note that root privilege is needed because the process needs to create virtual
 > interfaces, inject packets, manipulate namespaces, and modify routing table
 > entries within respective namespaces.