Groups
Sign in
Groups
tlaplus
Conversations
About
Send feedback
Help
tlaplus
Contact owners and managers
1–30 of 1490
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 group
0 selected
Isaac Dynamo
,
Markus Kuppe
2
1:09 PM
Recursion without StackOverflowError
Hi Isaac, you have identified a bug in TLC's handling of lazy values within the scope of ENABLED
unread,
Recursion without StackOverflowError
Hi Isaac, you have identified a bug in TLC's handling of lazy values within the scope of ENABLED
1:09 PM
Leslie Lamport
, …
Aman Shaikh
4
Jul 19
TLA+ Foundation Grants
The link works now. aman On Thursday, July 18, 2024 at 9:28:31 PM UTC-4 Leslie Lamport wrote:
unread,
TLA+ Foundation Grants
The link works now. aman On Thursday, July 18, 2024 at 9:28:31 PM UTC-4 Leslie Lamport wrote:
Jul 19
Ugur Y. Yavuz
, …
Damien Doligez
7
Jul 12
Parsing issues with prime operator in user-defined operators
In your lemma, IdxSet is indeed under a quantifier and thus a constant, so your lemma is true. But in
unread,
Parsing issues with prime operator in user-defined operators
In your lemma, IdxSet is indeed under a quantifier and thus a constant, so your lemma is true. But in
Jul 12
Markus Kuppe
,
Leslie Lamport
2
Jul 9
Possible TLC soundness bug when checking temporal properties
Should TLC be able to check such a property? I suspect that the error is that TLC should report that
unread,
Possible TLC soundness bug when checking temporal properties
Should TLC be able to check such a property? I suspect that the error is that TLC should report that
Jul 9
A. Jesse Jiryu Davis
,
Markus Kuppe
6
Jul 7
Distributed model-checking
Note that TLC's simulation mode also supports the `-continue` parameter, which causes the
unread,
Distributed model-checking
Note that TLC's simulation mode also supports the `-continue` parameter, which causes the
Jul 7
Stephan Merz
3
Jul 7
TLA+ Community Meeting 2024
Due to a user error, posts to tla...@inria.fr were not received. In case you already sent an
unread,
TLA+ Community Meeting 2024
Due to a user error, posts to tla...@inria.fr were not received. In case you already sent an
Jul 7
Andrew Helwer
Jul 1
OpenSSH CVE due to race condition - specify it in TLA+?
If anybody is looking for a fun project, there was recently a fairly severe bug in OpenSSH caused by
unread,
OpenSSH CVE due to race condition - specify it in TLA+?
If anybody is looking for a fun project, there was recently a fairly severe bug in OpenSSH caused by
Jul 1
Shahbaz Ahmad
Jun 24
PlusCal algorithm for pH for Smart Agriculture
Hello to all, I am student of PhD in Pakistan. I have proposed the following algorithm to check pH at
unread,
PlusCal algorithm for pH for Smart Agriculture
Hello to all, I am student of PhD in Pakistan. I have proposed the following algorithm to check pH at
Jun 24
Viktor Danylenko
Jun 22
Trapping Rain Water (simple TLA spec)
Hi All, As part of my TLA+ learning, I wrote a spec for a Leetcode problem (https://leetcode.com/
unread,
Trapping Rain Water (simple TLA spec)
Hi All, As part of my TLA+ learning, I wrote a spec for a Leetcode problem (https://leetcode.com/
Jun 22
Lee
, …
Finn Hackett
5
Jun 21
Question: how to describe the network message from ewd687a/EWD687aPlusCal.tla in Rust?
Thanks for the tip Finn, i now better understand the approach. Cheers! /Lee On Thu, 20 Jun 2024, 23:
unread,
Question: how to describe the network message from ewd687a/EWD687aPlusCal.tla in Rust?
Thanks for the tip Finn, i now better understand the approach. Cheers! /Lee On Thu, 20 Jun 2024, 23:
Jun 21
Jack Vanlightly
, …
Roman Bondar
8
Jun 20
Send/receive message passing or atomic communication in distributed systems
Hello Jack, You mentioned above that you worked with the new Kafka consumer group protocol from KIP
unread,
Send/receive message passing or atomic communication in distributed systems
Hello Jack, You mentioned above that you worked with the new Kafka consumer group protocol from KIP
Jun 20
Leslie Lamport
, …
Nine Fingers
12
Jun 20
Draft of New TLA Book
Hi Leslie, I'd like to provide a suggestion of including some of the concepts of your "
unread,
Draft of New TLA Book
Hi Leslie, I'd like to provide a suggestion of including some of the concepts of your "
Jun 20
Hillel Wayne
Jun 18
A new technique for composing TLA+ Specs
Wrote about it here: https://www.hillelwayne.com/post/composing-tla/. Thanks to Murat and Andrew for
unread,
A new technique for composing TLA+ Specs
Wrote about it here: https://www.hillelwayne.com/post/composing-tla/. Thanks to Murat and Andrew for
Jun 18
ovidiu...@gmail.com
,
Leslie Lamport
3
Jun 17
Dedalus versus TLA+
Dear Leslie, Thank you for your feedback. Looks like their comparison is unfortunately missleading
unread,
Dedalus versus TLA+
Dear Leslie, Thank you for your feedback. Looks like their comparison is unfortunately missleading
Jun 17
Andrew Helwer
,
C. M. Sperberg-McQueen
2
Jun 13
Seeking community feedback: keep or remove some Unicode symbols?
Andrew Helwer <andrew...@gmail.com> writes: > .... I am seeking peoples' feedback on
unread,
Seeking community feedback: keep or remove some Unicode symbols?
Andrew Helwer <andrew...@gmail.com> writes: > .... I am seeking peoples' feedback on
Jun 13
Loi Nguyen
Jun 5
PL and Software Verification projects that use TLA+
I would like to learn more about research projects related to programming languages (PL) or software
unread,
PL and Software Verification projects that use TLA+
I would like to learn more about research projects related to programming languages (PL) or software
Jun 5
Hillel Wayne
Jun 5
Prophecy variables for distributed checking?
A prophecy variable is an auxiliary variable that encodes into a nondeterministic action the spec
unread,
Prophecy variables for distributed checking?
A prophecy variable is an auxiliary variable that encodes into a nondeterministic action the spec
Jun 5
Prashant Deva
, …
Markus Kuppe
6
Jun 4
which tla+ ide to get started?
At the TLC level, https://github.com/tlaplus/tlaplus/issues/835, https://github.com/tlaplus/tlaplus/
unread,
which tla+ ide to get started?
At the TLC level, https://github.com/tlaplus/tlaplus/issues/835, https://github.com/tlaplus/tlaplus/
Jun 4
zacattackftw
,
Andrew Helwer
3
Jun 4
Examples For Draining Updates
Thanks for the response Andrew! At the least I can forward this advise along (or make a toy spec
unread,
Examples For Draining Updates
Thanks for the response Andrew! At the least I can forward this advise along (or make a toy spec
Jun 4
Chris Ortiz
Jun 3
Cross-Features possibility determination
Hi TLAplus google group, Is it correctly to say that the CONSTANT and VARIABLES of SpecA (which
unread,
Cross-Features possibility determination
Hi TLAplus google group, Is it correctly to say that the CONSTANT and VARIABLES of SpecA (which
Jun 3
Chris Ortiz
May 31
Spec Explorer...Link it back into Editor
Hi, Using the TLA+ Toolbox, have you guys try to drag the Spec Explorer out from the Editor and be
unread,
Spec Explorer...Link it back into Editor
Hi, Using the TLA+ Toolbox, have you guys try to drag the Spec Explorer out from the Editor and be
May 31
Grundmann, Matthias (KASTEL)
,
Stephan Merz
3
May 31
Proving temporal property in TLAPS
Hi Stephan, Thank you for the explanation which helped me to better comprehend how the prover
unread,
Proving temporal property in TLAPS
Hi Stephan, Thank you for the explanation which helped me to better comprehend how the prover
May 31
Michal Jaszczyk
,
Earnshaw
2
May 29
Invariant violated, no state trace
You can try to get the error trace log file by using TLC command line instead of ToolBox GUI as the
unread,
Invariant violated, no state trace
You can try to get the error trace log file by using TLC command line instead of ToolBox GUI as the
May 29
Martin
,
Hillel Wayne
2
May 28
Re: [tlaplus] ToolBox GraphViz encountered problem after cleaning .tlaplus folder
I believe you should be able to `winget graphviz` to install it on windows. On Tue, May 28, 2024, 10:
unread,
Re: [tlaplus] ToolBox GraphViz encountered problem after cleaning .tlaplus folder
I believe you should be able to `winget graphviz` to install it on windows. On Tue, May 28, 2024, 10:
May 28
marta zhango
, …
Andrew Helwer
20
May 21
Statements in TLA
Leslie emailed me to tell me that he actually covered this exact topic in section 3.4.2.7 of his new
unread,
Statements in TLA
Leslie emailed me to tell me that he actually covered this exact topic in section 3.4.2.7 of his new
May 21
Max Neverov
,
Andrew Helwer
3
May 20
Definitions inside and outside of an algorithm and macros
Hi Andrew, Thanks for the clarification! On Sunday, May 19, 2024 at 9:29:08 PM UTC+2 Andrew Helwer
unread,
Definitions inside and outside of an algorithm and macros
Hi Andrew, Thanks for the clarification! On Sunday, May 19, 2024 at 9:29:08 PM UTC+2 Andrew Helwer
May 20
Gabriela Moreira
May 18
An Emacs package for Unicode input
Hi all! I wrote a simple Emacs package [1] to enable input of Unicode symbols. It's pretty
unread,
An Emacs package for Unicode input
Hi all! I wrote a simple Emacs package [1] to enable input of Unicode symbols. It's pretty
May 18
A. Jesse Jiryu Davis
,
Markus Kuppe
3
May 16
Model-checking the Raft spec
Hi Jesse, you should be able to reuse much from https://github.com/microsoft/CCF/blob/main/tla/
unread,
Model-checking the Raft spec
Hi Jesse, you should be able to reuse much from https://github.com/microsoft/CCF/blob/main/tla/
May 16
moshe kravchik
, …
Alex Porter
6
May 13
TLA+ for parser correctness
Thanks a lot! I will indeed look into EverPArse as it meets my requirements! On Mon, May 13, 2024 at
unread,
TLA+ for parser correctness
Thanks a lot! I will indeed look into EverPArse as it meets my requirements! On Mon, May 13, 2024 at
May 13
Pavel Kalinnikov
, …
Jones Martins
11
May 11
Consensus spec safety in Paxos example
Hi Markus and Jones, Yeah, I am talking about safety. Markus, "stays chosen" is a safety
unread,
Consensus spec safety in Paxos example
Hi Markus and Jones, Yeah, I am talking about safety. Markus, "stays chosen" is a safety
May 11