Binary file Literature/counting-automata.pdf has changed
--- a/thys3/Paper.thy Sun Jul 17 20:09:38 2022 +0100
+++ b/thys3/Paper.thy Sun Jul 17 20:28:04 2022 +0100
@@ -276,9 +276,9 @@
\cite{CountingSet2020}). Therefore regular expression matching
libraries that rely on the classic notion of DFAs often impose
adhoc limits for bounded regular expressions: For example in the
- regular expression matching library in the Go language the regular expression
+ regular expression matching library in the Go language and also in Google's RE2 library the regular expression
@{term "NTIMES a 1001"} is not permitted, because no counter can be
- above 1000, and in the built-in Rust regular expression library
+ above 1000; and in the built-in regular expression library in Rust
expressions such as @{text "a\<^bsup>{1000}{100}{5}\<^esup>"} give an error
message for being too big. These problems can of course be solved in matching
algorithms where automata go beyond the classic notion and for