upd readme

Author: Chronosymbolic

README.md

@@ -36,26 +36,26 @@ Python (3.7.0 or higher, and [Anaconda](https://www.anaconda.com/) recommended)
     - 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 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`
+    - Or specify a file list using `-b -f FILELIST` (run files specified in the file list whose format is one file path in each line)
+        - e.g. `python test.py -a -v -b -f tests/filtered.txt -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 the 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 result summary log file using `-o FILE_NAME`; Export an additional result summary CSV `FILE_NAME_prefix.csv` (with success and timing statistics) using `-a`; The summary is only available when running multiple instances (directory mode or file list mode)
 
     - Start testing from the file index k in the folder `-s K` (`K` is the index starting from zero)
 
-    - 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)
+    - If you want to run multiple instances, make sure to use different `FILE_NAME`-s in the config file to avoid clash (`config.yml` in default)
 
     - More options see `--help`
 
 - After finishing running, the `./tmp` directory can be deleted safely
 
 # 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 minor randomness that may slightly affect the performance.
+Please refer to the configuration in `./experiment/result_summary.log`. Using the default config in `config.yml` 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`
 
@@ -89,15 +89,15 @@ In `test.py` `guess_manually` function:
 
 - Run `learner/enumerate.py` that enumerates through a context-free grammar
 
-## Benchmarks
+# Benchmarks
 [CHC-COMP](https://github.com/chc-comp)
 
 [Freqhorn](https://github.com/freqhorn/freqhorn)
 
 [LinearArbitrary](https://github.com/GaloisInc/LinearArbitrary-SeaHorn/tree/master/test)
 
 
-## Reference
+# Reference
 [chc-tools](https://github.com/chc-comp/chc-tools/tree/master/chctools)
 
 [libsvm](http://www.csie.ntu.edu.tw/~cjlin/libsvm)

experiment/README.md

@@ -5,7 +5,7 @@ The structure of the log is as follows:
 
 1. The first 2 lines are the modules used.
 
-2. The "Hyperparameters" section shows all the hyperparameters in `config.yaml`.
+2. The "Hyperparameters" section shows all the hyperparameters in `config.yml`.
 
 3. The "CHC Solving" part shows the results of solving all instances in the test suite. For each instance, it shows the file names, the size of the `*.smt2` or `*.smt` instance, the overall running time and time of each component, auxiliary info generated when running our tool (not important), the satisfiability of the CHC (correctness of corresponding program) and the proof (solution interpretation of predicates), and the double check procedure ensuring the correctness of the proof.