--- a/ChengsongTanPhdThesis/main.tex	Tue Oct 04 00:25:09 2022 +0100
+++ b/ChengsongTanPhdThesis/main.tex	Tue Oct 11 13:09:47 2022 +0100
@@ -295,10 +295,10 @@
 linear with respect to the input. 
 However with some regular expressions and inputs, existing implementations 
 often suffer from non-linear or even exponential running time, 
-allowing for example ReDoS (regular expression denial-of-service ) attacks. 
+giving to for example ReDoS (regular expression denial-of-service ) attacks. 
 To avoid these attacks, lexers with formalised correctness and running time related
-properties become appealing because the guarantee applies to all inputs, not just 
-a few empirical test cases.
+properties become appealing because the guarantee applies to all inputs, not a finite
+number of empirical test cases.
 
 Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string—that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an “aggressive” simplification function that keeps the size of derivatives finitely bounded. Without simplification the size of some derivatives can grow arbitrarily big resulting in an extremely slow lexing algorithm.