Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

application and DOMAIN of strings in TLC #512

Closed
johnyf opened this issue Oct 1, 2020 · 13 comments · May be fixed by #685
Closed

application and DOMAIN of strings in TLC #512

johnyf opened this issue Oct 1, 2020 · 13 comments · May be fixed by #685
Labels
enhancement Lets change things for the better help wanted We need your help Tools The command line tools - TLC, SANY, ...
Projects

Comments

@johnyf
Copy link

johnyf commented Oct 1, 2020

It would be nice if TLC supported function application f[i] and DOMAIN f when f is a string and when i \in DOMAIN f. Currently errors are raised, for example the following module:

---- MODULE Strings ----
EXTENDS Integers


ASSUME "abc"[2] = "b"[1]

ASSUME (DOMAIN "ab") = 1..2

========================

results in the following errors (the second error arises after commenting the first ASSUME above):

Error: Evaluating assumption line 5, col 8 to line 5, col 24 of module Strings failed.
A non-function (a string) was applied as a function.
line 5, col 8 to line 5, col 15 of module Strings

and

Error: Evaluating assumption line 7, col 8 to line 7, col 27 of module Strings failed.
Attempted to apply the operator DOMAIN to a non-function
(a string)
line 7, col 9 to line 7, col 19 of module Strings

This issue is relevant to #159.

@hwayne
Copy link

hwayne commented Oct 27, 2020

Fun fact, because the Sequences module uses Java overrides, you can use operators from that module on strings. So like Head(str) works.

@xxyzzn
Copy link

xxyzzn commented Oct 27, 2020

There is indeed a bug here--the one reported by hwayne. TLC incorrectly evaluates Head("abc") to equal "a". Head("abc") equals "abc"[1]. Since TLC reports that it can't evaluate "abc"[1], it should produce the same error message when evaluating Head("abc").

The semantics of TLA+ do not specify the value of "abc"[1], just as they do not specify the value of "abc"[5]. They do specify that "abc"[1] is unequal to "abc"[3], and TLAPS will prove that. To allow TLC to compute "abc"[1] # "abc"[3], it would have to be modified to handle a completely new "character" data type and print out the character 'a' as "a"[1]. If TLC were carefully designed, that should not be too difficult. But I doubt if it was that carefully designed. Anyone is welcome to give it a try. If it's possible to do it in a way that we can be sure will not introduce bugs in anything it now does, we'd be happy to add that feature to TLC.

Now, TLC should be able to evaluate any expression that can be written without explicitly describing any character, but not an expression like {"abc"[1]} whose value must be written in terms of the character "b"[1]. For example, TLC can evaluate Tail("abc") because its value, "bc", can be written without explicitly writing any character.

@lemmy lemmy added this to TODO (Engineering) in mku via automation Oct 27, 2020
@lemmy lemmy added enhancement Lets change things for the better help wanted We need your help Tools The command line tools - TLC, SANY, ... labels Oct 27, 2020
lemmy added a commit that referenced this issue Jul 2, 2021
Adresses comment #717602371 in Github issue #512
#512 (comment)

[Regression][TLC]
@zwergziege
Copy link

I started working on this (after flooding you with issues, today I thought I'd try something nice).
Here is what I have tested so far:

a == "abcd"
b == [x \in DOMAIN a |-> a[x]]
c == "bcd"
A == "a"[1]

ASSUME a = b
ASSUME DOMAIN a = 1..4
ASSUME a[2] = c[1]
ASSUME (a \o c) = (b \o c)
ASSUME <<A,A>> = "aa"
ASSUME <<A,A>> \in Seq({A})

Care to look at it? Be warned though. It's only a day's work of a Java noob who started looking at your codebase only yesterday.

@lemmy
Copy link
Member

lemmy commented Nov 2, 2021

Closing given 1..Len("abc") from Sequences as the slightly more verbose alternative to DOMAIN "abc". Supporting the latter would require for StringValue to implement tlc2.value.impl.Applicable.

Please reopen providing a PR that adds a proper character data type as mentioned by @xxyzzn above.

@ahelwer
Copy link
Contributor

ahelwer commented Mar 24, 2023

Sad to report that Head and Tail no longer work on strings on nightly. RIP.

@lemmy
Copy link
Member

lemmy commented Mar 24, 2023

TLC2 Version 2.18 of Day Month 20?? (rev: 05381d2)

(tla+) Tail("abc")
"bc"

@ahelwer
Copy link
Contributor

ahelwer commented Mar 24, 2023

Ah I suppose Tail still works, I just assumed it didn't. Head does not:

[ahelwer@node LeastCircularSubstring]$ java tlc2.REPL
Welcome to the TLA+ REPL!
TLC2 Version 2.18 of Day Month 20??
Enter a constant-level TLA+ expression.
(tla+) Head("abc")
Error evaluating expression: 'Head("abc")'
tlc2.tool.EvalException: The argument of Head should be a sequence, but instead 
it is:
"abc"

@lemmy
Copy link
Member

lemmy commented Mar 24, 2023

Head's behavior has indeed been reverted to EvalException for the reasons stated above.

@xxyzzn
Copy link

xxyzzn commented Mar 24, 2023 via email

@ahelwer
Copy link
Contributor

ahelwer commented Mar 24, 2023

I thought TLA+ strings were 1-indexed sequences, and it's only by shortfall of TLC that they are not actually able to be used that way?

@xxyzzn
Copy link

xxyzzn commented Mar 24, 2023 via email

@ahelwer
Copy link
Contributor

ahelwer commented Mar 24, 2023

Got it, so the language spec itself lacks the concept of a character type. I suppose this isn't the worst thing in the world, modern strings are best represented by ordinals with Seq(Nat) anyway. It might be nice to have a method (maybe in TLC or some other standard module?) to convert between strings and Seq(Nat) though, just for ease of input and reading output.

@xxyzzn
Copy link

xxyzzn commented Mar 24, 2023 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Lets change things for the better help wanted We need your help Tools The command line tools - TLC, SANY, ...
Projects
No open projects
mku
  
Done
Development

Successfully merging a pull request may close this issue.

6 participants