Update README.md

Author: Rayluo-mila

README.md

@@ -1,9 +1,9 @@
 # Chronosymbolic Learning
-Artifact for paper "Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning"
+Artifact for the paper "Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning"
 
-- See `./experiment` for some important results and configurations
+- See `./experiment` for some significant results and configurations
 
-- See `./examples` for examples on how our tool works
+- See `./examples` for examples of how our tool works
 
 ## Requirement (To set up our environment)
 Python (3.7.0 or higher, and anaconda recommended)
@@ -16,7 +16,7 @@ pip install -r requirements.txt
 
 May have to manually set up `PYTHONPATH` and `PATH` properly,  `PYTHONPATH=$Z3_BIN/python`, `PATH=$PATH:$Z3_BIN`
 
-Then, prepare the dataset following the instruction in `data/` folder.
+Then, prepare the dataset following the instructions in `data/` folder.
 
 ## Chronosymbolic Learning
 - Support SMT-LIB2 format (check-sat) and Datalog format (rule-query) 
@@ -33,33 +33,31 @@ Then, prepare the dataset following the instruction in `data/` folder.
 
 - Run: `python test.py` with the parameters below:
 
-    - Specify instance file name using `-f FILE_NAME`
+    - Specify instance file name using `-f FILE_NAME` to run a single instance
 
-    - Specify log file (which records how the tool solves the CHC system) using `-l FILE_NAME`
+    - Specify the log file (which records how the tool solves the CHC system) using `-l FILE_NAME`
 
-    - Specify directory name using `-r -f DIR_NAME` (logs are automatically generated in log/DIR_NAME)
+    - Specify directory name using `-r -f DIR_NAME` to run a test suite (logs are automatically generated in log/DIR_NAME)
         - e.g. `python test.py -f tests/safe/ -a -r -v -t 360 -o result/result.log`
 
-    - Or specify a file list using `-b -f FILELIST` (run files specified in the filelist, whose format is the same as `tests/filtered`)
+    - Or specify a file list using `-b -f FILELIST` (run files specified in the file list, whose format is the same as `tests/filtered`)
         - e.g. `python test.py -a -v -b -f tests/filtered -a -t 360 -o result/result.log`
 
     - Increase log file verbosity using `-v` (not effective in output on screen)
 
     - Adjust timeout using `-t TIMEOUT`, only effective in directory mode
 
-    - Specify overall result file using `-o FILE_NAME`, export a result csv (with success and timing statistics) with the same file name using `-a`
+    - Specify the overall result file using `-o FILE_NAME`, export a result CSV (with success and timing statistics) with the same file name using `-a`
 
-    - Individual LOG files will be outputed in `./log/YOUR_INSTANCE_PATH`
+    - Start testing from the file index k in the folder `-s K` (`K` is the index starting from zero)
 
-    - Start testing from the file index k in the folder `-s k` (index start from zero)
-
-    - If you want to run multiple instances, make sure using different `FILE_NAME`-s in the config file to avoid clash (`config.yaml` in default)
+    - If you want to run multiple instances, make sure to use different `FILE_NAME`-s in the config file to avoid clash (`config.yaml` in default)
 
     - More options see `--help`
 
 # To reproduce Chronosymbolic-single
 
-Please refer to the configuration in `./experiment/result_summary.log`. The default config should also be decent. Even fixed random seeds can cause some minor randomness that may slightly affect the performance.
+Please refer to the configuration in `./experiment/result_summary.log`. The default config should also be decent. Even fixed random seeds can cause minor randomness that may slightly affect the performance.
 
 - `python test.py -f tests/safe -a -r -v -t 360 -o result/result_safe.log`
 
@@ -74,22 +72,22 @@ Please refer to the configuration in `./experiment/result_summary.log`. The defa
 
 - Specify the path of z3 (with GSpacer) binary in `utils/run_spacer.py` and `utils/run_spacer_filtered.py`
 
-- Specify a folder name and run `utils/run_spacer.py` or specify a filelist name and run `utils/run_spacer_filtered.py`
+- Specify a folder name and run `utils/run_spacer.py` or specify a file list name and run `utils/run_spacer_filtered.py`
 
 - Enable GSpacer: `enable_global_guidance = 1`
 
 ## LinearArbitrary and Freqhorn
 Refer to [LinearArbitrary](https://github.com/GaloisInc/LinearArbitrary-SeaHorn/tree/master/test) and [Freqhorn](https://github.com/freqhorn/freqhorn)
 For LinearArbitrary, you can also try our optimized data-driven learner implementation (set `ClassAgent = Chronosymbolic` to `ClassAgent = DataDrivenLearner` in `test.py` and run it in the same way as Chronosymbolic does)
 
-## Manually "guess" an inductive invariant
+## Manually "guess" an inductive invariant (hard to scale up)
 In `test.py` `guess_manually` function:
 - Modify `s = 'v_0 == v_1'` to indicate the inductive invariant
 
-- Modify `db = load_horn_db_from_file("/home/ssr/chc-tools/chctools/NL/nl-1-chc.smt2", z3.main_ctx())` to indicate SMTLIB2 file name
+- Modify `db = load_horn_db_from_file(args.file_name, z3.main_ctx())` or pass the parameter in through command line to indicate SMTLIB2 file name
 
 ## Enumeration
-- A simple implementation of enumeration-based invariant synthesizer
+- A simple implementation of an enumeration-based invariant synthesizer
 
 - Run `learner/enumerate.py` that enumerates through a context-free grammar