Groups
Sign in
Groups
tlaplus
Conversations
About
Send feedback
Help
tlaplus
Contact owners and managers
1–30 of 1464
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
moshe kravchik
, …
Alex Porter
6
3:26 AM
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
3:26 AM
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
Maroš Orsák
,
Paul Eipper
4
May 9
Developing a TLA+ Model for the KafkaRoller in the Strimzi Project
So after a few iterations of the model...I was able to run verification on safety properties States
unread,
Developing a TLA+ Model for the KafkaRoller in the Strimzi Project
So after a few iterations of the model...I was able to run verification on safety properties States
May 9
Miguel Frutos
, …
Andrew Helwer
4
May 9
TLC Development
If you only care about the java command-line tools and not the eclipse-based java toolbox GUI, you
unread,
TLC Development
If you only care about the java command-line tools and not the eclipse-based java toolbox GUI, you
May 9
Murat Demirbas
May 3
Videos from TLA+ conference 2024
Hi Everyone, The talk videos from the TLA+ Conference 2024 are being released gradually. I've
unread,
Videos from TLA+ conference 2024
Hi Everyone, The talk videos from the TLA+ Conference 2024 are being released gradually. I've
May 3
Mariusz Ryndzionek
,
Jones Martins
2
May 2
General help with a simple spec
Hi Mariusz, Regarding the `AlwaysReset` property, this property is satisfied only in the first state
unread,
General help with a simple spec
Hi Mariusz, Regarding the `AlwaysReset` property, this property is satisfied only in the first state
May 2
marta zhango
,
Stephan Merz
11
Apr 29
Defining State_I as the state at energy level \epsilon(I)
Basically what I have is this macrostates == {k \in 1..m} \* macrostate k, microstates[k] == {j \in 1
unread,
Defining State_I as the state at energy level \epsilon(I)
Basically what I have is this macrostates == {k \in 1..m} \* macrostate k, microstates[k] == {j \in 1
Apr 29
marta zhango
Apr 29
Defining Energy Levels
If each macrostate s_k has n energy levels Ei for i=1 to n, how can I define define the energy
unread,
Defining Energy Levels
If each macrostate s_k has n energy levels Ei for i=1 to n, how can I define define the energy
Apr 29
marta zhango
, …
Martin
11
Apr 28
TLA+ for testing computational algorithms rather than verify mathematical proofs
No wonder I could not find anything useful to me. Will see how I can go with Coq. Regarging TLA, I
unread,
TLA+ for testing computational algorithms rather than verify mathematical proofs
No wonder I could not find anything useful to me. Will see how I can go with Coq. Regarging TLA, I
Apr 28
Andrew Helwer
Apr 28
Compatibility breakage: anybody still running the tools on Java 8?
For a few years now the java tools have had partial compatibility with the Java 8 VM: the tools were
unread,
Compatibility breakage: anybody still running the tools on Java 8?
For a few years now the java tools have had partial compatibility with the Java 8 VM: the tools were
Apr 28
marta zhango
,
Andrew Helwer
2
Apr 28
Installing Ulpian Release on Ubunte Machine
What have you tried to do and how has it not worked? For this kind of tech support people are usually
unread,
Installing Ulpian Release on Ubunte Machine
What have you tried to do and how has it not worked? For this kind of tech support people are usually
Apr 28
Muhammad El-Hindi
2
Apr 27
Best practices / advise on (de)structuring specs (modularize)
I'll try to update/answer my own question as I learn more things, maybe learners of TLA+ will
unread,
Best practices / advise on (de)structuring specs (modularize)
I'll try to update/answer my own question as I learn more things, maybe learners of TLA+ will
Apr 27
marta zhango
, …
Hillel Wayne
13
Apr 26
Defining Cardinality with TLA
Ok, So I can define. But just not with | Is that right ? On Saturday, April 27, 2024 at 4:19:34 AM
unread,
Defining Cardinality with TLA
Ok, So I can define. But just not with | Is that right ? On Saturday, April 27, 2024 at 4:19:34 AM
Apr 26
marta zhango
, …
Stephan Merz
10
Apr 26
TLA and TLAPIS
TLAPM is the proof manager, the central component of TLAPS. (The other components are the backend
unread,
TLA and TLAPIS
TLAPM is the proof manager, the central component of TLAPS. (The other components are the backend
Apr 26
marta zhango
Apr 25
Writing a proof in TLA
How can I write the proof for the number of permutations of n distinct objects using TLA ? In the
unread,
Writing a proof in TLA
How can I write the proof for the number of permutations of n distinct objects using TLA ? In the
Apr 25
Andrew Helwer
Apr 22
Lighthearted: TLA+ Syntax Puzzle
Lighthearted challenge - explain why this is valid TLA+ syntax: ---- MODULE Test ---- op == !!!!!!!!!
unread,
Lighthearted: TLA+ Syntax Puzzle
Lighthearted challenge - explain why this is valid TLA+ syntax: ---- MODULE Test ---- op == !!!!!!!!!
Apr 22
Dmitry Kulagin
,
divyanshu ranjan
2
Apr 22
Refinement Mappings and Fairness
Hello, 1. It is mentioned in section 8.9.4 of Specifying Systems that substitution does not
unread,
Refinement Mappings and Fairness
Hello, 1. It is mentioned in section 8.9.4 of Specifying Systems that substitution does not
Apr 22
Tung Nguyen
, …
Stephan Merz
7
Apr 20
Deadlock reach without invocation of main actions.
Another advice: in the initial condition, instead of /\ txRequest = [tx \in txs |-> RandomElement(
unread,
Deadlock reach without invocation of main actions.
Another advice: in the initial condition, instead of /\ txRequest = [tx \in txs |-> RandomElement(
Apr 20
Shahbaz Ahmad
,
Stephan Merz
2
Apr 17
how we can used the temporal properties in PlusCal algorithm and also removed the termination
Proving temporal properties such as termination requires adding fairness conditions to the
unread,
how we can used the temporal properties in PlusCal algorithm and also removed the termination
Proving temporal properties such as termination requires adding fairness conditions to the
Apr 17
hwa...@gmail.com
,
Markus Kuppe
2
Apr 12
MC file naming convention?
If the files MCSpec.tla and MCSpec.cfg exist, the VSCode extension will automatically check them when
unread,
MC file naming convention?
If the files MCSpec.tla and MCSpec.cfg exist, the VSCode extension will automatically check them when
Apr 12
jayaprabhakar k
, …
Stephan Merz
5
Apr 12
Liveness check with at least once message delivery
For this particular example one thing that can be tried is change spec to EmptyNetwork ==
unread,
Liveness check with at least once message delivery
For this particular example one thing that can be tried is change spec to EmptyNetwork ==
Apr 12
Jack Vanlightly
, …
Guo Hua
7
Apr 10
Send/receive message passing or atomic communication in distributed systems
Hi Jack, I read the MongoRaftReconfig (https://arxiv.org/pdf/2102.11960.pdf), and I like this idea. I
unread,
Send/receive message passing or atomic communication in distributed systems
Hi Jack, I read the MongoRaftReconfig (https://arxiv.org/pdf/2102.11960.pdf), and I like this idea. I
Apr 10
Samuel Miller
Apr 9
TLA+ Community Survey 2024 Results
Thank you to those who participated in the community survey. Attached are the results. There's a
unread,
TLA+ Community Survey 2024 Results
Thank you to those who participated in the community survey. Attached are the results. There's a
Apr 9
Georgios Kafanas (gkaf)
, …
Felipe Oliveira Carvalho
3
Apr 5
Analysis of a PlusCal algorithm is sensitive to placement of labels
> I would expect that the presence of labels would not affect liveness properties. Am I missing
unread,
Analysis of a PlusCal algorithm is sensitive to placement of labels
> I would expect that the presence of labels would not affect liveness properties. Am I missing
Apr 5
Shahbaz Ahmad
,
Stephan Merz
3
Mar 28
Using of PlusCal in smart agriculture to write specification for potential of hydrogen(ph) in soil
thanks for your good response. Ok, I will check and update my specifications. On Thu, Mar 21, 2024 at
unread,
Using of PlusCal in smart agriculture to write specification for potential of hydrogen(ph) in soil
thanks for your good response. Ok, I will check and update my specifications. On Thu, Mar 21, 2024 at
Mar 28
A. Jesse Jiryu Davis
Mar 28
Re: [tlaplus] Removing a label in a PlusCal algorithm changes the verification outcome
Hi Georgios, labels are very important in PlusCal. Code between a pair of labels runs atomically, and
unread,
Re: [tlaplus] Removing a label in a PlusCal algorithm changes the verification outcome
Hi Georgios, labels are very important in PlusCal. Code between a pair of labels runs atomically, and
Mar 28
Markus Kuppe
,
jayaprabhakar k
3
Mar 19
Schedule posted and registration open for TLA+ Conference on April 15th in Seattle, WA
Never mind, I see the collocated events on the next page. Sorry for spamming. On Tue, 19 Mar 2024 at
unread,
Schedule posted and registration open for TLA+ Conference on April 15th in Seattle, WA
Never mind, I see the collocated events on the next page. Sorry for spamming. On Tue, 19 Mar 2024 at
Mar 19
jayaprabhakar k
, …
Stephan Merz
7
Mar 16
Strong fairness
On Wed, 13 Mar 2024 at 11:01, Stephan Merz <stepha...@gmail.com> wrote: Thanks for the nice
unread,
Strong fairness
On Wed, 13 Mar 2024 at 11:01, Stephan Merz <stepha...@gmail.com> wrote: Thanks for the nice
Mar 16
Andrew Frances
,
Jones Martins
4
Mar 15
New to TLA+ Trying to install 1.7.3 from Github
The executable binary is toolbox inside the toolbox/ directory. I just ran it on my computer and
unread,
New to TLA+ Trying to install 1.7.3 from Github
The executable binary is toolbox inside the toolbox/ directory. I just ran it on my computer and
Mar 15
Michal Jaszczyk
Mar 14
what is wrong with this pluscal spec?
Below is a distilled version of something I ran into while writing my spec. PlusCal complains that a
unread,
what is wrong with this pluscal spec?
Below is a distilled version of something I ran into while writing my spec. PlusCal complains that a
Mar 14