Groups
Conversations
All groups and messages
Send feedback to Google
Help
Sign in
Groups
tlaplus
Conversations
About
tlaplus
1–30 of 1294
This is a discussion group for users of the TLA+ specification language, the PlusCal algorithm language, and their associated tools.
To find out about the languages and tools, see
The TLA Home Page
Posts by non-members are moderated.
We encourage you to join the group.
Mark all as read
Report abusive group
0 selected
Ugur Yagmur Yavuz
, …
Stephan Merz
3
Feb 4
Good TLAPS practices for reproducible verification of proofs
Hi Ugur, thanks for your feedback. I have seen similar problems when checking long proofs in a single
unread,
Good TLAPS practices for reproducible verification of proofs
Hi Ugur, thanks for your feedback. I have seen similar problems when checking long proofs in a single
Feb 4
Aman Shaikh
Jan 29
Specifying initial state of a spec while running TLC
Hi TLC usually computes the initial-state of a spec while performing model checking. Is it possible
unread,
Specifying initial state of a spec while running TLC
Hi TLC usually computes the initial-state of a spec while performing model checking. Is it possible
Jan 29
jack malkovick
,
Stephan Merz
2
Jan 29
checking that a pluscal spec implements another pluscal spec
In TLA+, the refinement that you want to prove is stated as RefinedSpec => \EE pc : GeneralSpec
unread,
checking that a pluscal spec implements another pluscal spec
In TLA+, the refinement that you want to prove is stated as RefinedSpec => \EE pc : GeneralSpec
Jan 29
jack malkovick
, …
Calvin Loncaric
4
Jan 29
A simple (distinct) states question
My mistake! I thought the total number of states could be affected by thread interleaving in parallel
unread,
A simple (distinct) states question
My mistake! I thought the total number of states could be affected by thread interleaving in parallel
Jan 29
Andrew Helwer
3
Jan 28
In TLC, what does the num parameter do given the -simulate flag?
Note that it appears the num=X parameter is multiplied by the number of workers On Saturday, January
unread,
In TLC, what does the num parameter do given the -simulate flag?
Note that it appears the num=X parameter is multiplied by the number of workers On Saturday, January
Jan 28
Samuel Miller
2
Jan 26
Metamodels and TLA+
I tried to investigate this a little further and ended up writing a blog post. I'm sure I got
unread,
Metamodels and TLA+
I tried to investigate this a little further and ended up writing a blog post. I'm sure I got
Jan 26
Khoa Goodwill
, …
hornace...@gmail.com
7
Jan 24
Parse Error
I see. I suggest you take a look at the chapter 5 in Leslie's book Specifying Systems, particular
unread,
Parse Error
I see. I suggest you take a look at the chapter 5 in Leslie's book Specifying Systems, particular
Jan 24
Stephan Merz
3
Jan 22
TLA+ Community Meeting 2023
We have already received a number of contributions to the Community Meeting, but a few more would be
unread,
TLA+ Community Meeting 2023
We have already received a number of contributions to the Community Meeting, but a few more would be
Jan 22
Andrew Helwer
2
Jan 21
Using formal methods to reason about probabilistic systems
After reading the Knuth-Yao spec that Ron Pressler & Markus Kuppe wrote (https://github.com/
unread,
Using formal methods to reason about probabilistic systems
After reading the Knuth-Yao spec that Ron Pressler & Markus Kuppe wrote (https://github.com/
Jan 21
Andrew Helwer
, …
Markus Kuppe
3
Jan 19
Monospace fonts no longer work on google groups
On 1/19/23 7:32 AM, Andrew Helwer wrote: > This makes specs here considerably harder to read and
unread,
Monospace fonts no longer work on google groups
On 1/19/23 7:32 AM, Andrew Helwer wrote: > This makes specs here considerably harder to read and
Jan 19
ns
Jan 18
TLC Error with Implementation Refinement of HourClock
Yes sorry for some reason all the formatting was removed after I posted it and despite multiple
unread,
TLC Error with Implementation Refinement of HourClock
Yes sorry for some reason all the formatting was removed after I posted it and despite multiple
Jan 18
ns
,
Andrew Helwer
3
Jan 18
TLC error with INSTANCE mechanism
es sorry for some reason all the formatting was removed after I posted it. And the displayed post
unread,
TLC error with INSTANCE mechanism
es sorry for some reason all the formatting was removed after I posted it. And the displayed post
Jan 18
Andrew Helwer
,
Stephan Merz
5
Jan 18
How can I modelcheck an angle-bracket action formula?
Ah, cracked open specifying systems - so you can only have [][A]_v or <><<A>>_v
unread,
How can I modelcheck an angle-bracket action formula?
Ah, cracked open specifying systems - so you can only have [][A]_v or <><<A>>_v
Jan 18
Ganesh Rapolu
,
Stephan Merz
2
Jan 17
Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)
Hello, the first problem that I have with this module is that it instantiates module Consensus, which
unread,
Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)
Hello, the first problem that I have with this module is that it instantiates module Consensus, which
Jan 17
hornace...@gmail.com
,
Markus Kuppe
3
Jan 15
Is the TLA+ Hyperbook down?
This one works, thanks! M. Dátum: nedeľa 15. januára 2023, čas: 20:02:51 UTC+1, odosielateľ: Markus
unread,
Is the TLA+ Hyperbook down?
This one works, thanks! M. Dátum: nedeľa 15. januára 2023, čas: 20:02:51 UTC+1, odosielateľ: Markus
Jan 15
Yeray Cabello
,
Andrew Helwer
4
Jan 13
I can't find why can't I make this process fair
Thanks a lot! El viernes, 13 de enero de 2023 a las 14:18:34 UTC+1, andrew...@gmail.com escribió:
unread,
I can't find why can't I make this process fair
Thanks a lot! El viernes, 13 de enero de 2023 a las 14:18:34 UTC+1, andrew...@gmail.com escribió:
Jan 13
Delta Striker
,
Stephan Merz
3
Jan 13
Some questions about writing 2D array with assignment and stack
Thank you very much,I'll try it now. :) 在2023年1月13日星期五 UTC+8 21:55:19<Stephan Merz> 写道: The
unread,
Some questions about writing 2D array with assignment and stack
Thank you very much,I'll try it now. :) 在2023年1月13日星期五 UTC+8 21:55:19<Stephan Merz> 写道: The
Jan 13
Markus Kuppe
Jan 12
Re: [tlaplus] Why same number of TLC distinct states occupys different disk space size
Besides the fingerprint set, TLC stores a state queue, a trace, and the liveness graph on disk, and,
unread,
Re: [tlaplus] Why same number of TLC distinct states occupys different disk space size
Besides the fingerprint set, TLC stores a state queue, a trace, and the liveness graph on disk, and,
Jan 12
Andrew Helwer
, …
Markus Kuppe
16
Jan 12
TLA+ tree-sitter grammar updates
I wrote a long blog post about my experience writing the tree-sitter grammar; it overlaps a fair bit
unread,
TLA+ tree-sitter grammar updates
I wrote a long blog post about my experience writing the tree-sitter grammar; it overlaps a fair bit
Jan 12
victor zhang
,
Stephan Merz
5
Jan 12
why I cannot compare Nat with 0
Got it, thanks! On Thursday, January 12, 2023 at 1:03:32 AM UTC-8 Stephan Merz wrote: TLC cannot
unread,
why I cannot compare Nat with 0
Got it, thanks! On Thursday, January 12, 2023 at 1:03:32 AM UTC-8 Stephan Merz wrote: TLC cannot
Jan 12
Vince Wu
Jan 12
Why same number of TLC distinct states occupy different disk space
I read from **Specifying Systems** that: >> In the actual implementation, the nodes of the
unread,
Why same number of TLC distinct states occupy different disk space
I read from **Specifying Systems** that: >> In the actual implementation, the nodes of the
Jan 12
Markus Kuppe
,
Andrew Helwer
4
Jan 11
TLA+ project meetings
Meeting Minutes January 10, 2023 Participants • Mamoun Filali • Martin Hornacek • Igor Konnov •
unread,
TLA+ project meetings
Meeting Minutes January 10, 2023 Participants • Mamoun Filali • Martin Hornacek • Igor Konnov •
Jan 11
Delta Striker
, …
Andrew Helwer
3
Jan 11
How to verify a parser in TLA+?
It's hard to say what a formal spec for a parser would even look like, other than an EBNF grammar
unread,
How to verify a parser in TLA+?
It's hard to say what a formal spec for a parser would even look like, other than an EBNF grammar
Jan 11
jayaprabhakar k
, …
Stephan Merz
12
Jan 10
Check eventual consistency
I'd read it as "WF sub count Tick". Also, if you really want to allow for these
unread,
Check eventual consistency
I'd read it as "WF sub count Tick". Also, if you really want to allow for these
Jan 10
jayaprabhakar k
Jan 7
List all the success and failure paths
Hi, When a model checker is run with the tla+ toolbox, it lists the number of states explored, and if
unread,
List all the success and failure paths
Hi, When a model checker is run with the tla+ toolbox, it lists the number of states explored, and if
Jan 7
Delta Striker
12/25/22
Few questions encountered when trying to implementing my spec in TLA+
External link below since it's a little bit long: https://stackoverflow.com/questions/74912408/
unread,
Few questions encountered when trying to implementing my spec in TLA+
External link below since it's a little bit long: https://stackoverflow.com/questions/74912408/
12/25/22
Delta Striker
,
Stephan Merz
3
12/25/22
How to get a set like this in TLA+?
Yes,that's exactly what I want,thank you. 在2022年12月22日星期四 UTC+8 23:57:08<Stephan Merz> 写道:
unread,
How to get a set like this in TLA+?
Yes,that's exactly what I want,thank you. 在2022年12月22日星期四 UTC+8 23:57:08<Stephan Merz> 写道:
12/25/22
Andrew Lygin
, …
Karl Ang
8
12/24/22
TLA+ for Visual Studio Code
Thank you Markus. Your link led me to the solution written in Caveats Section. The picture attached:
unread,
TLA+ for Visual Studio Code
Thank you Markus. Your link led me to the solution written in Caveats Section. The picture attached:
12/24/22
Sharon Kas
,
Stephan Merz
2
12/23/22
TCP Protocl model satisfies
Hello, a few quick comments on your spec: - all actions should determine the values of all state
unread,
TCP Protocl model satisfies
Hello, a few quick comments on your spec: - all actions should determine the values of all state
12/23/22
Deividas Bražėnas
,
Stephan Merz
13
12/22/22
Converting TLA+ spec to PlusCal
with m = [t |-> "PROPOSE", v |-> input] do msgs := [p \in peers |-> msgs[p] \cup {
unread,
Converting TLA+ spec to PlusCal
with m = [t |-> "PROPOSE", v |-> input] do msgs := [p \in peers |-> msgs[p] \cup {
12/22/22