From 60b3bc819e40b5e333fb9f608ad4d849601aa4d9 Mon Sep 17 00:00:00 2001
From: zhouzhezz <zorichzorich@gmail.com>
Date: Fri, 8 Mar 2024 20:13:21 -0500
Subject: [PATCH 01/40] fix

---
 README.md | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 43419e6..415d28d 100644
--- a/README.md
+++ b/README.md
@@ -97,8 +97,7 @@ The Coq proofs of our core language **λ<sup>E</sup>** are located in the `forma
 
 ## Step-by-Step Instructions
 
-In this section, we provide the instructions to evaluate our artifact. The [first half of this section](#running-benchmarks-of-poirot) describes the installation and use of **Marple**, an OCaml implementation of a refinement type checker that verifies the coverage property of the test input generators written in OCaml. The [rest of this section](#proof-readme) describes the Coq formalization of the core language **λ<sup>TG</sup>** in the paper and the corresponding soundness theorem.
-
+In this section, we provide the instructions to evaluate our artifact.
 
 ### Artifact Structure
 
@@ -108,7 +107,7 @@ This section gives a brief overview of the files in this artifact.
 * `coersion` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
-  + `data/ri/ADT_LIBRARY/METHOD.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `METHOD.ml` that are methods of given `ADT` implementation, these folder also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
+  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folder also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
 * `desymbolic/`: minterm transfermation that convert SFA into FA.
 * `dtree/`: the decision tree data structure used in instantiation and minterm generation.
 * `env/`: the universal environment of **Marple** which is loaded from the configuration files.

From dbae056dced5b96cf7d9751788ef919fad776d3c Mon Sep 17 00:00:00 2001
From: zhouzhezz <zorichzorich@gmail.com>
Date: Sun, 10 Mar 2024 18:39:49 -0400
Subject: [PATCH 02/40] fix

---
 README.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index 415d28d..2e731c3 100644
--- a/README.md
+++ b/README.md
@@ -133,32 +133,32 @@ The following scripts run the benchmark suite displayed in Table 1 of the paper.
 
 The following scripts run the preprocess on all benchmark suite displayed in Table 1 of the paper, and store the result into statfile file (defined in config file `meta-config.json`, the default location is `.stat`).
 
-    $ python3 scripts/comprehensive.py silent ntyping data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py silent ntyping data/ri
 
 Then, the following prints the first part of table 1 (as markdown table). The printed table is in _GitHub_ markdown format, the reader can visualize the table via `https://gist.github.com/` or any other markdown visualizer.
 
-    $ python3 scripts/comprehensive.py silent show-md-table1 data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
 ##### Step 2: Type Check
 
 The following scripts run typecheck on all benchmark suite displayed in Table 1 of the paper, and store the result into statfile file (defined in config file `meta-config.json`, the default location is `.stat`). It will take about `15` mins:
 
-    $ python3 scripts/comprehensive.py silent typing data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py silent typing data/ri
 
 Then, the following prints the two parts of table 1 (please first performs preporcess to get the statistics result for the first part of the table). The printed table is in _GitHub_ markdown format, the reader can visualize the table via `https://gist.github.com/` or any other markdown visualizer.
 
-    $ python3 scripts/comprehensive.py silent show-md-table1 data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
 (Optional) The reader can also print the table 2 shown in the supplemental material (again, please first performs preporcess to get the statistics result for the first part of the table).
 
-    $ python3 scripts/comprehensive.py silent show-md-table2 data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table2 data/ri
 
 
 #### Detailed Steps
 
 By add commanding the line argument `verbose`, all of the scripts above will show the actual command sent to **Marple** on each benchmark. For example, by running:
 
-    $ python3 scripts/comprehensive.py verbose ntyping data/ri
+    $ ../.venv/bin/python scripts/comprehensive.py verbose ntyping data/ri
 
 The script will print the following commands:
 
@@ -194,7 +194,7 @@ See [Pretty Printing](#pretty-printing).
 
 The following command performs the basic (OCaml) type check (and normalization which converts code into A-normal form, converts LTLf formulae into symbolic regular language) for a given ADT implementation.
 
-    $ python3 scripts/comprehensive.py silent ntyping-one data/ri/FileSystem_Tree
+    $ ../.venv/bin/python scripts/comprehensive.py silent ntyping-one data/ri/FileSystem_Tree
 
 The following command performs the basic type check  (and normalization which convert code into A-normal form, converts LTLf formulae into symbolic regular language) for one interface of a given ADT implementation.
 
@@ -271,7 +271,7 @@ fun (u : unit) ->
 
 The following command performs the HAT type check for a given ADT implementation. It will take about `3` min:
 
-    $ python3 scripts/comprehensive.py silent typing-one data/ri/FileSystem_Tree
+    $ ../.venv/bin/python scripts/comprehensive.py silent typing-one data/ri/FileSystem_Tree
 
 The following command performs the HAT type check for a interface of a given ADT implementation.
 

From 8a679e8053769b0a17fa7ccae8939d63b1981a73 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:03:58 -0400
Subject: [PATCH 03/40] autoamata -> automata

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 2e731c3..0b31474 100644
--- a/README.md
+++ b/README.md
@@ -55,11 +55,11 @@ successfully:
 
 ##### Pretty Printing
 
-As another way to verify the tool operating successfull, the following command pretty prints the content of given files, which may contains source code, autoamata predicates, and HATs:
+As another way to verify the tool operating successfull, the following command pretty prints the content of given files, which may contains source code, automata predicates, and HATs:
 
     $ ./main.exe print-raw meta-config.json data/ri/FileSystem_KVStore/ri.ml
 
-The script will print the following autoamata predicates:
+The script will print the following automata predicates:
 
 ```
 val[@pred] rI: (p : Path.t) = ☐⟨is_root p⟩ ∨ (¬aliveP(p) ∨ dirP(parent p))

From 20da09e4f4c80575add3b4d38f9d281760c910ba Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:06:38 -0400
Subject: [PATCH 04/40] consistent dir naming

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 0b31474..273abd5 100644
--- a/README.md
+++ b/README.md
@@ -104,7 +104,7 @@ In this section, we provide the instructions to evaluate our artifact.
 This section gives a brief overview of the files in this artifact.
 
 * `bin/main.ml`: the main entry point of **Marple**.
-* `coersion` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
+* `coersion/` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
   + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folder also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.

From e0a6b42fe6cce5dab52d9d2bc403271ed16746bd Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:08:36 -0400
Subject: [PATCH 05/40] plural

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 273abd5..2742980 100644
--- a/README.md
+++ b/README.md
@@ -107,7 +107,7 @@ This section gives a brief overview of the files in this artifact.
 * `coersion/` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
-  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folder also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
+  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
 * `desymbolic/`: minterm transfermation that convert SFA into FA.
 * `dtree/`: the decision tree data structure used in instantiation and minterm generation.
 * `env/`: the universal environment of **Marple** which is loaded from the configuration files.

From 2166e6bb50dfffe5329f1d54f1e5bd5fea12f0b4 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:09:08 -0400
Subject: [PATCH 06/40] transfermation -> transformation

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 2742980..44f7265 100644
--- a/README.md
+++ b/README.md
@@ -108,7 +108,7 @@ This section gives a brief overview of the files in this artifact.
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
   + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
-* `desymbolic/`: minterm transfermation that convert SFA into FA.
+* `desymbolic/`: minterm transformation that convert SFA into FA.
 * `dtree/`: the decision tree data structure used in instantiation and minterm generation.
 * `env/`: the universal environment of **Marple** which is loaded from the configuration files.
 * `formalization/`: the Coq proofs of our core language **λ<sup>E</sup>**.

From f8006dbd92e97e9678a2773e3d5a457148ec0e09 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:09:42 -0400
Subject: [PATCH 07/40] invaraint -> invariant

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 44f7265..40c0902 100644
--- a/README.md
+++ b/README.md
@@ -107,7 +107,7 @@ This section gives a brief overview of the files in this artifact.
 * `coersion/` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
-  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invaraint `ri.ml`.
+  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invariant `ri.ml`.
 * `desymbolic/`: minterm transformation that convert SFA into FA.
 * `dtree/`: the decision tree data structure used in instantiation and minterm generation.
 * `env/`: the universal environment of **Marple** which is loaded from the configuration files.

From 93f6c5c0253e8602e60cf9b8ca8b5d5a80dc8b31 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:11:05 -0400
Subject: [PATCH 08/40] represention -> representation

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 40c0902..591aafe 100644
--- a/README.md
+++ b/README.md
@@ -107,7 +107,7 @@ This section gives a brief overview of the files in this artifact.
 * `coersion/` and `normalization/`: the normalization procedure that normalizes the code into the Monadic Normal Form (a variant of the A-Normal form).
 * `data/`: the predefined types and the benchmark input files.
   + `data/predefined/`: the predefined types.
-  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and represention invariant `ri.ml`.
+  + `data/ri/ADT_LIBRARY/INTERFACE.ml`: the benchmark input files. For each `ADT` that is implemented by different underline library `LIBRARY`, There is a folder under path `data/ri/`. Besides `INTERFACE.ml` that are methods of given `ADT` implementation, these folders also provide the basic and refinement types for underline library (`lib_nty.ml` and `lib_rty.ml`), automata predicates (`automata_preds.ml`) and representation invariant `ri.ml`.
 * `desymbolic/`: minterm transformation that convert SFA into FA.
 * `dtree/`: the decision tree data structure used in instantiation and minterm generation.
 * `env/`: the universal environment of **Marple** which is loaded from the configuration files.

From 538756100a4245431d9dba019faf4417788c3943 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:13:03 -0400
Subject: [PATCH 09/40] displays -> display

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 591aafe..7276102 100644
--- a/README.md
+++ b/README.md
@@ -123,7 +123,7 @@ This section gives a brief overview of the files in this artifact.
 
 ### Running Benchmarks of Marple
 
-In this section, we discuss the scripts that displays the tables in the evaluation section of the paper.
+In this section, we discuss the scripts that display the tables in the evaluation section of the paper.
 
 #### Comprehensive Scripts
 

From 208cdd3c0f50c9ef2c569b444d2ef74435f4d8e5 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:14:41 -0400
Subject: [PATCH 10/40] preprocess section

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 7276102..63ae50a 100644
--- a/README.md
+++ b/README.md
@@ -131,7 +131,9 @@ The following scripts run the benchmark suite displayed in Table 1 of the paper.
 
 ##### Step 1: Preprocess
 
-The following scripts run the preprocess on all benchmark suite displayed in Table 1 of the paper, and store the result into statfile file (defined in config file `meta-config.json`, the default location is `.stat`).
+The following scripts run the preprocess step on all benchmark suite displayed
+in Table 1 of the paper, and store the result into a statfile file (defined in
+config file `meta-config.json`, the default location is `.stat`).
 
     $ ../.venv/bin/python scripts/comprehensive.py silent ntyping data/ri
 

From 5b7a2d768a276b2287ce8c2e4bdd56a052aac3f7 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:17:23 -0400
Subject: [PATCH 11/40] markdown -> Markdown

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 63ae50a..03b7688 100644
--- a/README.md
+++ b/README.md
@@ -137,7 +137,7 @@ config file `meta-config.json`, the default location is `.stat`).
 
     $ ../.venv/bin/python scripts/comprehensive.py silent ntyping data/ri
 
-Then, the following prints the first part of table 1 (as markdown table). The printed table is in _GitHub_ markdown format, the reader can visualize the table via `https://gist.github.com/` or any other markdown visualizer.
+Then, the following prints the first part of table 1 (as Markdown table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
@@ -147,7 +147,7 @@ The following scripts run typecheck on all benchmark suite displayed in Table 1
 
     $ ../.venv/bin/python scripts/comprehensive.py silent typing data/ri
 
-Then, the following prints the two parts of table 1 (please first performs preporcess to get the statistics result for the first part of the table). The printed table is in _GitHub_ markdown format, the reader can visualize the table via `https://gist.github.com/` or any other markdown visualizer.
+Then, the following prints the two parts of table 1 (please first performs preporcess to get the statistics result for the first part of the table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 

From d01c2042f5d44d78dbdea5deafc81bda5264adad Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:19:41 -0400
Subject: [PATCH 12/40] preporcess -> preprocess

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 03b7688..7abf4e3 100644
--- a/README.md
+++ b/README.md
@@ -147,11 +147,11 @@ The following scripts run typecheck on all benchmark suite displayed in Table 1
 
     $ ../.venv/bin/python scripts/comprehensive.py silent typing data/ri
 
-Then, the following prints the two parts of table 1 (please first performs preporcess to get the statistics result for the first part of the table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
+Then, the following prints the two parts of table 1 (please first performs preprocess to get the statistics result for the first part of the table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
-(Optional) The reader can also print the table 2 shown in the supplemental material (again, please first performs preporcess to get the statistics result for the first part of the table).
+(Optional) The reader can also print the table 2 shown in the supplemental material (again, please first performs preprocess to get the statistics result for the first part of the table).
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table2 data/ri
 

From 3115f16e16b27bc844fea1a65a4ba418b1406b23 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:23:09 -0400
Subject: [PATCH 13/40] performs preprocess -> perform preprocessing

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 7abf4e3..9a9ae81 100644
--- a/README.md
+++ b/README.md
@@ -147,11 +147,11 @@ The following scripts run typecheck on all benchmark suite displayed in Table 1
 
     $ ../.venv/bin/python scripts/comprehensive.py silent typing data/ri
 
-Then, the following prints the two parts of table 1 (please first performs preprocess to get the statistics result for the first part of the table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
+Then, the following prints the two parts of table 1 (please first perform preprocessing to get the statistics result for the first part of the table). The printed table is in _GitHub_ Markdown format, the reader can visualize the table via `https://gist.github.com/` or any other Markdown visualizer.
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
-(Optional) The reader can also print the table 2 shown in the supplemental material (again, please first performs preprocess to get the statistics result for the first part of the table).
+(Optional) The reader can also print the table 2 shown in the supplemental material (again, please first perform preprocessing to get the statistics result for the first part of the table).
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table2 data/ri
 

From 89040997ccb73d7a7607d373af6e65e794f46b11 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:24:16 -0400
Subject: [PATCH 14/40] scripts above -> above scripts

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 9a9ae81..027f7fd 100644
--- a/README.md
+++ b/README.md
@@ -158,7 +158,7 @@ Then, the following prints the two parts of table 1 (please first perform prepro
 
 #### Detailed Steps
 
-By add commanding the line argument `verbose`, all of the scripts above will show the actual command sent to **Marple** on each benchmark. For example, by running:
+By add commanding the line argument `verbose`, all of the above scripts will show the actual command sent to **Marple** on each benchmark. For example, by running:
 
     $ ../.venv/bin/python scripts/comprehensive.py verbose ntyping data/ri
 

From bf21da035bd35924b36322b63e69186e5d50478b Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:31:04 -0400
Subject: [PATCH 15/40] Some code formatting

---
 README.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 027f7fd..e649898 100644
--- a/README.md
+++ b/README.md
@@ -71,7 +71,7 @@ Another example:
 
 The script will print the following source code and refinement types:
 
-```
+```ocaml
 let add = fun (path : Path.t) ->
   fun (content : Bytes.t) ->
     (if exists path
@@ -206,11 +206,11 @@ By enable the `preprocess` option in the config file `meta-config.json`, **Marpl
 
 **Requirements:** We use bold and coloring printting in command line, make sure your terminal supports escape sequences.
 
-> For example,
+For example,
 
     $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
 
-> will print
+will print
 
 ```
 Top Operation Normal Type Context:
@@ -454,7 +454,7 @@ let[@assertRty] add ((p : Path.t) [@ghost]) ?l:(path = (true : [%v: Path.t]))
 
 can be desugared as
 
-```
+```ocaml
 let[@assertRty] add =
     fun ((p : Path.t) [@ghost]) ->
     fun ?l:(path = (true : [%v: Path.t])) ->

From deb5ba259b89fba213240a2007426f652fce395c Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:32:41 -0400
Subject: [PATCH 16/40] resuablility -> reusability

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e649898..78fe760 100644
--- a/README.md
+++ b/README.md
@@ -186,7 +186,7 @@ Readers can try these commands to execute each step individually.
 
 ### Detail Usage of Marple
 
-For resuablility, we introduce the detail usage of Marple. Using **Marple**, you can
+For reusability, we introduce the detail usage of Marple. Using **Marple**, you can
 
 #### Pretty Printing
 

From 369dd56e75e6405361b4e39de8836551e1df1a3f Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:34:25 -0400
Subject: [PATCH 17/40] Complete sentence with something

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 78fe760..c3a9006 100644
--- a/README.md
+++ b/README.md
@@ -186,7 +186,8 @@ Readers can try these commands to execute each step individually.
 
 ### Detail Usage of Marple
 
-For reusability, we introduce the detail usage of Marple. Using **Marple**, you can
+For reusability, we introduce the detail usage of Marple. Using **Marple**, you
+can do the following.
 
 #### Pretty Printing
 

From 946a016a4a4ceaa2aa2d2b9419f76e222948bac5 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:35:39 -0400
Subject: [PATCH 18/40] typecheck -> type check for consistency

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index c3a9006..2d0e5dd 100644
--- a/README.md
+++ b/README.md
@@ -143,7 +143,7 @@ Then, the following prints the first part of table 1 (as Markdown table). The pr
 
 ##### Step 2: Type Check
 
-The following scripts run typecheck on all benchmark suite displayed in Table 1 of the paper, and store the result into statfile file (defined in config file `meta-config.json`, the default location is `.stat`). It will take about `15` mins:
+The following scripts run type check on all benchmark suite displayed in Table 1 of the paper, and store the result into statfile file (defined in config file `meta-config.json`, the default location is `.stat`). It will take about `15` mins:
 
     $ ../.venv/bin/python scripts/comprehensive.py silent typing data/ri
 

From e2c4ab5d82ceb354c5e5ec9fb770503440bfcfc7 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:37:24 -0400
Subject: [PATCH 19/40] desguaring -> desugaring

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 2d0e5dd..af2d5cf 100644
--- a/README.md
+++ b/README.md
@@ -203,7 +203,7 @@ The following command performs the basic type check  (and normalization which co
 
     $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
 
-By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desguaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
+By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
 
 **Requirements:** We use bold and coloring printting in command line, make sure your terminal supports escape sequences.
 

From ff386f705945d343b9dbc7db0ff34e47521f31fe Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:38:11 -0400
Subject: [PATCH 20/40] printting -> printing

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index af2d5cf..88dc851 100644
--- a/README.md
+++ b/README.md
@@ -205,7 +205,7 @@ The following command performs the basic type check  (and normalization which co
 
 By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
 
-**Requirements:** We use bold and coloring printting in command line, make sure your terminal supports escape sequences.
+**Requirements:** We use bold and coloring printing in command line, make sure your terminal supports escape sequences.
 
 For example,
 
@@ -282,7 +282,7 @@ The following command performs the HAT type check for a interface of a given ADT
 
 By enable the `typing` option in the config file `meta-config.json`, **Marple** will print the typing rules and subtyping rules used during type check.
 
-**Requirements:** We use bold and coloring printting in command line, make sure your terminal supports escape sequences.
+**Requirements:** We use bold and coloring printing in command line, make sure your terminal supports escape sequences.
 
 > For example,
 

From 3c44e942b767b505593a8a458ec73a389fb28b1a Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:38:30 -0400
Subject: [PATCH 21/40] remove space

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 88dc851..aa6aaa4 100644
--- a/README.md
+++ b/README.md
@@ -199,7 +199,7 @@ The following command performs the basic (OCaml) type check (and normalization w
 
     $ ../.venv/bin/python scripts/comprehensive.py silent ntyping-one data/ri/FileSystem_Tree
 
-The following command performs the basic type check  (and normalization which convert code into A-normal form, converts LTLf formulae into symbolic regular language) for one interface of a given ADT implementation.
+The following command performs the basic type check (and normalization which convert code into A-normal form, converts LTLf formulae into symbolic regular language) for one interface of a given ADT implementation.
 
     $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
 

From 3ac4a7b2a4573a2711d462530e9051abc298a52a Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:39:17 -0400
Subject: [PATCH 22/40] coloring -> colored

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index aa6aaa4..45d9c30 100644
--- a/README.md
+++ b/README.md
@@ -205,7 +205,7 @@ The following command performs the basic type check (and normalization which con
 
 By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
 
-**Requirements:** We use bold and coloring printing in command line, make sure your terminal supports escape sequences.
+**Requirements:** We use bold and colored printing in the command line, make sure your terminal supports escape sequences.
 
 For example,
 

From 3c4b8025027718f228b36b2c5271bb472d283612 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:40:18 -0400
Subject: [PATCH 23/40] a interface -> an interface

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 45d9c30..d38e95d 100644
--- a/README.md
+++ b/README.md
@@ -276,7 +276,7 @@ The following command performs the HAT type check for a given ADT implementation
 
     $ ../.venv/bin/python scripts/comprehensive.py silent typing-one data/ri/FileSystem_Tree
 
-The following command performs the HAT type check for a interface of a given ADT implementation.
+The following command performs the HAT type check for an interface of a given ADT implementation.
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json data/ri/FileSystem_Tree/add.ml
 
@@ -330,7 +330,7 @@ OCaml primitives, including various arithmetic operators, and data constructors,
 
 #### Input File Formats
 
-As a verification tool for representation invaraint of datatypes that is impelemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invaraint shared by all interfaces. For example, when **Marple** can type check a interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
+As a verification tool for representation invaraint of datatypes that is impelemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invaraint shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json ADT_DIR/INTERFACE.ml
 

From 3a5d9c933b8a04516388eae8e75eb8fb09d441e0 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:41:29 -0400
Subject: [PATCH 24/40] preprocess -> preprocessed

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index d38e95d..6d24d3d 100644
--- a/README.md
+++ b/README.md
@@ -318,7 +318,7 @@ DT(FileSystem)  Task 1(add): exec time 19.768031(s), type check succeeded
 
 All commands of **Marple** will take a universal configuration file (`meta-config.json`) in JSON format as its first argument. Precisely, the JSON file outputs results in JSON format to some output directory.
 - the `debug_tags` field controls the debug information output. Precisely, we have the following options:
-  + if the `preprocess` field is true, **Marple** will print the preprocess result. It will print the given source code, type code, and the code in A-Normal Form.
+  + if the `preprocess` field is true, **Marple** will print the preprocessed result. It will print the given source code, type code, and the code in A-Normal Form.
   + if the `typing` field is set as true, **Marple** will print the type judgement of each step in the type check.
   + if the `result` field is set as true, **Marple** will print the type check result.
 - the `resfile` field indicates the path of the output file of type check.

From d5f6338d52e26562fac7f5688da6d69f89dd21de Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:42:09 -0400
Subject: [PATCH 25/40] type -> typed

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 6d24d3d..ddfe669 100644
--- a/README.md
+++ b/README.md
@@ -318,7 +318,7 @@ DT(FileSystem)  Task 1(add): exec time 19.768031(s), type check succeeded
 
 All commands of **Marple** will take a universal configuration file (`meta-config.json`) in JSON format as its first argument. Precisely, the JSON file outputs results in JSON format to some output directory.
 - the `debug_tags` field controls the debug information output. Precisely, we have the following options:
-  + if the `preprocess` field is true, **Marple** will print the preprocessed result. It will print the given source code, type code, and the code in A-Normal Form.
+  + if the `preprocess` field is true, **Marple** will print the preprocessed result. It will print the given source code, typed code, and the code in A-Normal Form.
   + if the `typing` field is set as true, **Marple** will print the type judgement of each step in the type check.
   + if the `result` field is set as true, **Marple** will print the type check result.
 - the `resfile` field indicates the path of the output file of type check.

From f9f26b3ebd9f0b90cd5837dcb80d20a2c9c99a75 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:42:36 -0400
Subject: [PATCH 26/40] type -> typing

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index ddfe669..00e2000 100644
--- a/README.md
+++ b/README.md
@@ -319,7 +319,7 @@ DT(FileSystem)  Task 1(add): exec time 19.768031(s), type check succeeded
 All commands of **Marple** will take a universal configuration file (`meta-config.json`) in JSON format as its first argument. Precisely, the JSON file outputs results in JSON format to some output directory.
 - the `debug_tags` field controls the debug information output. Precisely, we have the following options:
   + if the `preprocess` field is true, **Marple** will print the preprocessed result. It will print the given source code, typed code, and the code in A-Normal Form.
-  + if the `typing` field is set as true, **Marple** will print the type judgement of each step in the type check.
+  + if the `typing` field is set as true, **Marple** will print the typing judgement of each step in the type check.
   + if the `result` field is set as true, **Marple** will print the type check result.
 - the `resfile` field indicates the path of the output file of type check.
 - the `logfile` field indicates the path of the log file of type check.

From 6e9c96e31901708b99105c9df6752b534153315b Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:43:36 -0400
Subject: [PATCH 27/40] unintepreted -> uninterpreted

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 00e2000..60a26ba 100644
--- a/README.md
+++ b/README.md
@@ -326,7 +326,7 @@ All commands of **Marple** will take a universal configuration file (`meta-confi
 - the `statfile` field indicates the path of the statistics file of type check.
 - the `uninterops` field indicates the built-in operators and method predicates used in the current benchmarks.
 - the `prim_path` field indicates the predefined refinement types for a number of
-OCaml primitives, including various arithmetic operators, and data constructors, and axioms of unintepreted functions.
+OCaml primitives, including various arithmetic operators, and data constructors, and axioms of uninterpreted functions.
 
 #### Input File Formats
 

From b5a5ffd4da5eccc1a01d92d46eac71706d39116d Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:44:12 -0400
Subject: [PATCH 28/40] impelemented -> implemented

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 60a26ba..b3d16a4 100644
--- a/README.md
+++ b/README.md
@@ -330,7 +330,7 @@ OCaml primitives, including various arithmetic operators, and data constructors,
 
 #### Input File Formats
 
-As a verification tool for representation invaraint of datatypes that is impelemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invaraint shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
+As a verification tool for representation invaraint of datatypes that is implemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invaraint shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json ADT_DIR/INTERFACE.ml
 

From 41e3d58f19d53116c33a1025d97f5638422a7b9b Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:44:38 -0400
Subject: [PATCH 29/40] invaraint -> invariant

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index b3d16a4..622c47f 100644
--- a/README.md
+++ b/README.md
@@ -330,7 +330,7 @@ OCaml primitives, including various arithmetic operators, and data constructors,
 
 #### Input File Formats
 
-As a verification tool for representation invaraint of datatypes that is implemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invaraint shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
+As a verification tool for representation invariant of datatypes that is implemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invariant shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json ADT_DIR/INTERFACE.ml
 
@@ -340,7 +340,7 @@ a folder (`ADT_DIR`) should contain the following files:
   + `lib_nty.ml` (the basic (OCaml) typing for the underline stateful library)
   + `lib_rty.ml` (the HAT typing for the underline stateful library)
   + `automata_preds.ml` (automata predicates, e.g., 𝑃stored in Example 4.1, it is optional)
-  + `ri.ml` (representation invaraint shared by all interfaces)
+  + `ri.ml` (representation invariant shared by all interfaces)
   + `INTERFACE.ml` (source code and HAT of this interface)
 
 #### Format of `lib_nty.ml`

From 98f5fe8f86de65b218690b4ec82e358e85729cc5 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:45:27 -0400
Subject: [PATCH 30/40] an

---
 README.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 622c47f..7b5e3b1 100644
--- a/README.md
+++ b/README.md
@@ -330,7 +330,12 @@ OCaml primitives, including various arithmetic operators, and data constructors,
 
 #### Input File Formats
 
-As a verification tool for representation invariant of datatypes that is implemented by underline stateful library, **Marple** expects input contains the specification of underline stateful library and a representation invariant shared by all interfaces. For example, when **Marple** can type check an interface `INTERFACE` via the following command (introduced in [HAT Type check](#hat-type-check)):
+As a verification tool for representation invariant of datatypes that is
+implemented by an underline stateful library, **Marple** expects input contains
+the specification of underline stateful library and a representation invariant
+shared by all interfaces. For example, when **Marple** can type check an
+interface `INTERFACE` via the following command (introduced in [HAT Type
+check](#hat-type-check)):
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json ADT_DIR/INTERFACE.ml
 

From ad11e79ce51943771e074086438b86c2954899af Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:46:13 -0400
Subject: [PATCH 31/40] that

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 7b5e3b1..79d4ce2 100644
--- a/README.md
+++ b/README.md
@@ -331,7 +331,7 @@ OCaml primitives, including various arithmetic operators, and data constructors,
 #### Input File Formats
 
 As a verification tool for representation invariant of datatypes that is
-implemented by an underline stateful library, **Marple** expects input contains
+implemented by an underline stateful library, **Marple** expects input that contains
 the specification of underline stateful library and a representation invariant
 shared by all interfaces. For example, when **Marple** can type check an
 interface `INTERFACE` via the following command (introduced in [HAT Type

From 40d3d72c6df314a9cc54b6ac74d6ee2e7b6af8a4 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:47:31 -0400
Subject: [PATCH 32/40] functions -> function

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 79d4ce2..95007fd 100644
--- a/README.md
+++ b/README.md
@@ -384,7 +384,7 @@ let INTERFACE = OCAML_EXPR
 let[@assertRty] INTERFACE = HTY
 ```
 
-The source code `OCAML_EXPR` expected by **Marple** is simply an OCaml functions listing. Currently, **Marple** handles only a subset of OCaml, it does not handle features involving references and effects, parametric polymorphism, or concurrency. Additionally, all functions should be annotated with precise input and output type; all left-hand-side variables in a let binding should be annotated with its precise type.
+The source code `OCAML_EXPR` expected by **Marple** is simply an OCaml function listing. Currently, **Marple** handles only a subset of OCaml, it does not handle features involving references and effects, parametric polymorphism, or concurrency. Additionally, all functions should be annotated with precise input and output type; all left-hand-side variables in a let binding should be annotated with its precise type.
 
 #### Syntax of HAT
 

From 9913a1943c8b91fd0e7246b7cd7ed4d42e553e5b Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:49:19 -0400
Subject: [PATCH 33/40] feild -> field

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 95007fd..22ce98f 100644
--- a/README.md
+++ b/README.md
@@ -449,7 +449,7 @@ The definition of the coverage type is consistent with Figure 4. Precisely,
 + the qualifier is defined as `PROP`.
 + the refinement type is defined as `RTY`.
 + the Symbolic Finite Automata is defined as `SFA`. Notice that, the type alias `∼𝑣𝑥` is notated by `[@d]`. We also accept the automata predicates application, e.g., `𝑃exists (k)` in Example 4.2.
-+ the Hoare Automata Types is defined as `HAT`, we use an abbreviation with `newadding` feild when the postcondition automata just appending new events to the precondition automata.
++ the Hoare Automata Types is defined as `HAT`, we use an abbreviation with `newadding` field when the postcondition automata just appending new events to the precondition automata.
 + Our syntax share the same syntax sugar with OCaml program, thus, for example
 
 ```

From ec8c884fe09b553c004832b4e3c14a97c45debe2 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:50:06 -0400
Subject: [PATCH 34/40] grammar

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 22ce98f..892f03f 100644
--- a/README.md
+++ b/README.md
@@ -449,7 +449,9 @@ The definition of the coverage type is consistent with Figure 4. Precisely,
 + the qualifier is defined as `PROP`.
 + the refinement type is defined as `RTY`.
 + the Symbolic Finite Automata is defined as `SFA`. Notice that, the type alias `∼𝑣𝑥` is notated by `[@d]`. We also accept the automata predicates application, e.g., `𝑃exists (k)` in Example 4.2.
-+ the Hoare Automata Types is defined as `HAT`, we use an abbreviation with `newadding` field when the postcondition automata just appending new events to the precondition automata.
++ the Hoare Automata Types is defined as `HAT`, we use an abbreviation with the
+  `newadding` field when the postcondition automata is just appending new events
+  to the precondition automata.
 + Our syntax share the same syntax sugar with OCaml program, thus, for example
 
 ```

From 64ce230b612ffc1bfa79959abd2d842786971057 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 19:50:40 -0400
Subject: [PATCH 35/40] program -> programs

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 892f03f..58a7d07 100644
--- a/README.md
+++ b/README.md
@@ -452,7 +452,7 @@ The definition of the coverage type is consistent with Figure 4. Precisely,
 + the Hoare Automata Types is defined as `HAT`, we use an abbreviation with the
   `newadding` field when the postcondition automata is just appending new events
   to the precondition automata.
-+ Our syntax share the same syntax sugar with OCaml program, thus, for example
++ Our syntax share the same syntax sugar with OCaml programs, thus, for example
 
 ```
 let[@assertRty] add ((p : Path.t) [@ghost]) ?l:(path = (true : [%v: Path.t]))

From 9c0d277697e77d6de3a4e9ec7c40edb8bc16115e Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 21:37:53 -0400
Subject: [PATCH 36/40] enable -> enabling

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 58a7d07..75745ff 100644
--- a/README.md
+++ b/README.md
@@ -203,7 +203,7 @@ The following command performs the basic type check (and normalization which con
 
     $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
 
-By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
+By enabling the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
 
 **Requirements:** We use bold and colored printing in the command line, make sure your terminal supports escape sequences.
 

From ced94e34fbba329a83d2dd53a4e73c25218f4f62 Mon Sep 17 00:00:00 2001
From: zhouzhezz <zorichzorich@gmail.com>
Date: Sun, 10 Mar 2024 21:40:06 -0400
Subject: [PATCH 37/40] update test machine settinng

---
 README.md | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 58a7d07..8faf3d5 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ A docker image of this repo with all required dependecies is available on: `http
 
 We recommend machines have at least 8 GB of memory and 8 GB of hard
 disk space available when building and running Docker images. All
-benchmarks were tested on MacBook Pro 14-inc, 2021, which has an Apple M1 Pro CPU with 16 GB RAM. The estimated execution time in the rest of the document also fits this setting.
+benchmarks were tested on a Linux machine having Intel i7-8700 CPU @ 3.20GHz with `64GB` of RAM. The estimated execution time in the rest of the document also fits this setting.
 
 ### Requirements
 
@@ -151,10 +151,6 @@ Then, the following prints the two parts of table 1 (please first perform prepro
 
     $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table1 data/ri
 
-(Optional) The reader can also print the table 2 shown in the supplemental material (again, please first perform preprocessing to get the statistics result for the first part of the table).
-
-    $ ../.venv/bin/python scripts/comprehensive.py silent show-md-table2 data/ri
-
 
 #### Detailed Steps
 

From 96aae6c9b32ad77ceed13e385ebb89cb9b8f82b0 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Sun, 10 Mar 2024 21:42:41 -0400
Subject: [PATCH 38/40] lised -> listed

---
 formalization/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formalization/README.md b/formalization/README.md
index 0d469d6..3cb4c04 100644
--- a/formalization/README.md
+++ b/formalization/README.md
@@ -45,7 +45,7 @@ opam pin coq-stdpp 1.9.0
 opam pin coq-hammer-tactics 1.3.2+8.18
 ```
 
-> Notice: We have installed all dependencies lised above in our docker image.
+> Notice: We have installed all dependencies listed above in our docker image.
 
 To build and check the Coq formalization, simply run `make` in the
 `formalization` directory. The command `Print Assumptions soundness` at the end

From 570797c0fc343d3f2d625c0c499510ff22bc2b67 Mon Sep 17 00:00:00 2001
From: zhouzhezz <zorichzorich@gmail.com>
Date: Mon, 11 Mar 2024 18:41:59 -0400
Subject: [PATCH 39/40] fix typo

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 8faf3d5..8dbb994 100644
--- a/README.md
+++ b/README.md
@@ -197,7 +197,7 @@ The following command performs the basic (OCaml) type check (and normalization w
 
 The following command performs the basic type check (and normalization which convert code into A-normal form, converts LTLf formulae into symbolic regular language) for one interface of a given ADT implementation.
 
-    $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
+    $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/init.ml
 
 By enable the `preprocess` option in the config file `meta-config.json`, **Marple** will print the result of preprocess: desugaring, basic type check, and normalization. The details can be found in [Configuration of Marple](#configuration-of-marple).
 
@@ -205,7 +205,7 @@ By enable the `preprocess` option in the config file `meta-config.json`, **Marpl
 
 For example,
 
-    $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/add.ml
+    $ ./_build/default/bin/main.exe ri-ntype-check meta-config.json data/ri/FileSystem_Tree/init.ml
 
 will print
 

From 02e615bd003076f82cfcae2d532e1b68687a789b Mon Sep 17 00:00:00 2001
From: Qianchuan Ye <yeqianchuan@gmail.com>
Date: Mon, 11 Mar 2024 18:52:18 -0400
Subject: [PATCH 40/40] Typo

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index b813cd8..1704a70 100644
--- a/README.md
+++ b/README.md
@@ -280,11 +280,11 @@ By enable the `typing` option in the config file `meta-config.json`, **Marple**
 
 **Requirements:** We use bold and coloring printing in command line, make sure your terminal supports escape sequences.
 
-> For example,
+For example,
 
     $ ./_build/default/bin/main.exe ri-type-check meta-config.json data/ri/FileSystem_Tree/add.ml
 
-> will print
+will print
 
 ```
 ...