Hello,
please check Section 16.1.10 of Specifying Systems, which discusses strings and characters and even contains a function to convert lower-case letters to ASCII. In short, TLA+ has no hardwired definition of what characters are. In your representation, the variables in_pattern and in_text are sequences of strings, not characters.
As far as I can tell, the algorithm is independent of any concrete representation of characters. I suggest that you make the set of characters as well as the inputs to the algorithm parameters of your specification, i.e. introduce (at the top of the module)
CONSTANT Character, text, pattern
ASSUME text \in Seq(Character) /\ pattern \in Seq(Character)
When you use TLC to check your algorithm, you can instantiate these constants by concrete values, e.g.
Character <- {a,b,c} \* a set of model values
text <- << a, a, b, a, c >>
pattern <- << b, a >>
In this way, you'll also alleviate the effect of state explosion. If you want to go further than testing the algorithm on concrete inputs, you can replace the parameters `text' and `pattern' by variables and nondeterministically assign them finite (bounded-length) sequences of characters by writing something like
define {
\* sequences of characters of length at most n
CharSeq(n) == UNION { [1 .. k -> Character] : k \in 0 .. n }
}
[...]
variables text \in CharSeq(5), pattern \in CharSeq(3);
[...]
In this way, TLC will check the algorithm for all text / pattern strings of bounded length.
Remember that TLA+ is a language for specifying algorithms at a high level of abstraction, not a programming language.
Hope this helps,
Stephan