Your original request was to be able to check if a string starts with
`A' and ends with 'a'. I believe this is done in TLA+ by the
following operator:
StartsWith_A_andEndsWith_a(s) ==
/\ Len(s) > 0
/\ s[1] = "A"[1]
/\ s[Len(s)] = "a"[1]
However, I'm not sure because TLC cannot evaluate this, and I suspect
TLAPS can't handle it either, though I haven't tried. TLC can handle
the following definition, and a few tests confirm that it is the
operator you wanted:
StartsWith_A_andEndsWith_a(s) ==
LET sx == s \o "x"
IN /\ SubSeq(sx, 1, 1) = "A"
/\ SubSeq(sx, Len(s), Len(s)) = "a"
There are lots of TLA+ expressions that TLC can't evaluate. For
example, consider this definition:
TheSetOfAllPrimes ==
LET IsAPrime(n) == ...
IN {n \in Nat : IsAPrime(n)}
If IsAPrime is properly defined, TLC could evaluate the expression
42 \in TheSetOfAllPrimes
However, it can't evaluate
{2*n : n \in Nat} \intersect TheSetOfAllPrimes
It would be hard to extend TLC to be able to evaluate this expression.
It would not be hard to extend it to handle the first definition of
StartsWith_A_andEndsWith_a. However, there are many other things that
seem to be more important for us to do.
Whether TLA+ is the best language for you to use depends on what you
want to do. If you want to check the correctness of a concurrent system
and you want to use a little bit of string manipulation in your spec,
it probably is. If you want to do something that requires complicated
string processing, it probably isn't.
Leslie