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
Comments
Fun fact, because the |
There is indeed a bug here--the one reported by hwayne. TLC incorrectly evaluates The semantics of TLA+ do not specify the value of Now, TLC should be able to evaluate any expression that can be written without explicitly describing any character, but not an expression like |
Adresses comment #717602371 in Github issue #512 #512 (comment) [Regression][TLC]
I started working on this (after flooding you with issues, today I thought I'd try something nice).
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. |
Closing given Please reopen providing a PR that adds a proper character data type as mentioned by @xxyzzn above. |
Sad to report that |
TLC2 Version 2.18 of Day Month 20?? (rev: 05381d2) (tla+) Tail("abc")
"bc" |
Ah I suppose
|
Head's behavior has indeed been reverted to |
The value of Head("abc") is not specified by the semantics of TLA+.
From: Andrew Helwer ***@***.***>
Sent: Friday, March 24, 2023 12:38
To: tlaplus/tlaplus ***@***.***>
Cc: Leslie Lamport ***@***.***>; Mention ***@***.***>
Subject: Re: [tlaplus/tlaplus] application and DOMAIN of strings in TLC (#512)
Ah I suppose Tail still works, I just assumed it didn't. Head does not:
***@***.*** 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"
-
Reply to this email directly, view it on GitHub<#512 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AEUS3OWOA33QRPM6BQQUVADW5XZ2LANCNFSM4SAGLOOA>.
You are receiving this because you were mentioned.Message ID: ***@***.******@***.***>>
|
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? |
They are 1-indexed sequences, but what they are sequences of is unspecified. This implies that <<Head("abc")>> equals "a", but it doesn't say what Head("abc") equals. Unfortunately, TLC is not smart enough to realize it can evaluate <<Head("abc")>> without evaluating Head("abc"). But there are lots of expressions TLC can't evaluate even though it can express their values.
From: Andrew Helwer ***@***.***>
Sent: Friday, March 24, 2023 14:06
To: tlaplus/tlaplus ***@***.***>
Cc: Leslie Lamport ***@***.***>; Mention ***@***.***>
Subject: Re: [tlaplus/tlaplus] application and DOMAIN of strings in TLC (#512)
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?
-
Reply to this email directly, view it on GitHub<#512 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AEUS3OQSD42LWHMRXXUEPPLW5YEB5ANCNFSM4SAGLOOA>.
You are receiving this because you were mentioned.Message ID: ***@***.******@***.***>>
|
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 |
That sounds like a nice community module.
From: Andrew Helwer ***@***.***>
Sent: Friday, March 24, 2023 14:26
To: tlaplus/tlaplus ***@***.***>
Cc: Leslie Lamport ***@***.***>; Mention ***@***.***>
Subject: Re: [tlaplus/tlaplus] application and DOMAIN of strings in TLC (#512)
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.
-
Reply to this email directly, view it on GitHub<#512 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AEUS3OQO4ZJNG45RQ55SQKTW5YGNVANCNFSM4SAGLOOA>.
You are receiving this because you were mentioned.Message ID: ***@***.******@***.***>>
|
It would be nice if TLC supported function application
f[i]
andDOMAIN f
whenf
is a string and wheni \in DOMAIN f
. Currently errors are raised, for example the following module:results in the following errors (the second error arises after commenting the first
ASSUME
above):and
This issue is relevant to #159.
The text was updated successfully, but these errors were encountered: