Movatterモバイル変換
[0]
ホーム
URL:
画像なし
夜間モード
Groups
Groups
Conversations
All groups and messages
Send feedback to Google
Help
Training
Sign in
Groups
Groups
tlaplus
Conversations
About
tlaplus
Contact owners and managers
1–30 of 1603
Posts by non-members are moderated.
We encourage you to join the group.
Mark all as read
Report group
0 selected
Weining Cao
, …
Igor Konnov
3
Nov 4
Discussion: Apalache found counter-example for invariant that was claimed proved via TLC→TLAPS
Hi Weining Cao, Seconding what Stephan wrote. The most important question is whether the
unread,
Discussion: Apalache found counter-example for invariant that was claimed proved via TLC→TLAPS
Hi Weining Cao, Seconding what Stephan wrote. The most important question is whether the
Nov 4
Ugur Yavuz
, …
Ugur Y. Yavuz
3
Nov 1
Initializing local variables in PlusCal
Yes, that's what I saw in the manual as well, but I was a bit surprised there wasn't any
unread,
Initializing local variables in PlusCal
Yes, that's what I saw in the manual as well, but I was a bit surprised there wasn't any
Nov 1
Chris Ortiz
, …
Markus Kuppe
4
Oct 30
Will there be a lesson learned on AWS 2025 East-1 Outage due to DynamoDB with regards to TLA+?
Amazon's 2022 paper, “Amazon DynamoDB: A Scalable, Predictably Performant, and Fully Managed
unread,
Will there be a lesson learned on AWS 2025 East-1 Outage due to DynamoDB with regards to TLA+?
Amazon's 2022 paper, “Amazon DynamoDB: A Scalable, Predictably Performant, and Fully Managed
Oct 30
Dylan Zueck
, …
Markus Kuppe
3
Oct 29
Checking that a specific path is always possible to take
Interrupt cannot occur at any time in your example specification because you restricted Interrupt to
unread,
Checking that a specific path is always possible to take
Interrupt cannot occur at any time in your example specification because you restricted Interrupt to
Oct 29
Rostislav Nikitin
Oct 26
Re: [tlaplus] Digest for tlaplus@googlegroups.com - 2 updates in 1 topic
Hello Stephan. Thank for your answer. Yep, you are absolutely right. Yesterday I found this article:
unread,
Re: [tlaplus] Digest for tlaplus@googlegroups.com - 2 updates in 1 topic
Hello Stephan. Thank for your answer. Yep, you are absolutely right. Yesterday I found this article:
Oct 26
Rostislav Nikitin
,
Stephan Merz
2
Oct 26
Temporal property unexpectedly fails
A TLA+ specification Init /\ [][Next]_vars allows for behaviors that end in infinite stuttering after
unread,
Temporal property unexpectedly fails
A TLA+ specification Init /\ [][Next]_vars allows for behaviors that end in infinite stuttering after
Oct 26
Shane Miller
,
Andrew Helwer
3
Oct 24
Checking temporal properties (2 quick questions)
Thank you for your reply On Thu, Oct 23, 2025, 4:07 PM Andrew Helwer <andrew...@gmail.com>
unread,
Checking temporal properties (2 quick questions)
Thank you for your reply On Thu, Oct 23, 2025, 4:07 PM Andrew Helwer <andrew...@gmail.com>
Oct 24
Markus Kuppe
,
Hillel Wayne
2
Oct 15
Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension
I need to rewrite learntla to use vscode, but might be a bit before I can get to that. If this
unread,
Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension
I need to rewrite learntla to use vscode, but might be a bit before I can get to that. If this
Oct 15
Ugur Yavuz
,
Stephan Merz
2
Oct 10
The Naturals module
I don't know why that module was changed in the distribution [1] with respect to the presentation
unread,
The Naturals module
I don't know why that module was changed in the distribution [1] with respect to the presentation
Oct 10
Shane Miller
,
Stephan Merz
3
Oct 3
Nailing down how/where fariness is inherited by macros, procedures
The best way to answer these questions is to understand the TLA+ specification that corresponds to a
unread,
Nailing down how/where fariness is inherited by macros, procedures
The best way to answer these questions is to understand the TLA+ specification that corresponds to a
Oct 3
Marko Schuetz-Schmuck
, …
Andrew Helwer
3
Oct 3
using the tla-toolbox on wayland
I mostly use neovim to write TLA+, with the tree-sitter-tlaplus grammar for highlighting. Syntax
unread,
using the tla-toolbox on wayland
I mostly use neovim to write TLA+, with the tree-sitter-tlaplus grammar for highlighting. Syntax
Oct 3
Jskri
, …
Stephan Merz
11
Oct 2
Feedback on TLA+ tutorial and proofs
Thank you for your thorough review. I agree with most of your comments. The links have been fixed in
unread,
Feedback on TLA+ tutorial and proofs
Thank you for your thorough review. I agree with most of your comments. The links have been fixed in
Oct 2
Ian Dardik
, …
Stephan Merz
5
Oct 1
Fully Compositional Inductive Invariant Inference in TLA+: Grant Presentation
Thank you to everyone who joined the presentation! The recording is available here. On Tuesday,
unread,
Fully Compositional Inductive Invariant Inference in TLA+: Grant Presentation
Thank you to everyone who joined the presentation! The recording is available here. On Tuesday,
Oct 1
Shane Miller
,
Markus Kuppe
2
Sep 26
How to configure TLA to emit event traces on command line only (no IDE)
> On Sep 25, 2025, at 7:58 PM, Shane Miller <gshane...@gmail.com> wrote: > > Hello
unread,
How to configure TLA to emit event traces on command line only (no IDE)
> On Sep 25, 2025, at 7:58 PM, Shane Miller <gshane...@gmail.com> wrote: > > Hello
Sep 26
Markus Alexander Kuppe
,
Andrew Helwer
3
Sep 26
TLA+ Validation Test Suite Now Available - Enabling ISO 26262 Certification for TLC
> On Sep 26, 2025, at 3:54 AM, Andrew Helwer <andrew...@gmail.com> wrote: > > Wow,
unread,
TLA+ Validation Test Suite Now Available - Enabling ISO 26262 Certification for TLC
> On Sep 26, 2025, at 3:54 AM, Andrew Helwer <andrew...@gmail.com> wrote: > > Wow,
Sep 26
Chris Pacejo
,
Shane Miller
2
Sep 26
Confused about depth-first search
I am similarly confused for the same reasons. -dfid num run the model check in depth-first iterative
unread,
Confused about depth-first search
I am similarly confused for the same reasons. -dfid num run the model check in depth-first iterative
Sep 26
Mehdi Sabraoui
,
Ovidiu Marcu
3
Sep 11
TLA+ Video Course License
Unfortunately that email no longer works. It bounced back to me. I found the lecture series to be
unread,
TLA+ Video Course License
Unfortunately that email no longer works. It bounced back to me. I found the lecture series to be
Sep 11
Matthew Thompson
, …
Andrew Helwer
9
Sep 7
Is Dempster Shaffer/Probabilistic Reasoning possible in TLA plus
Thanks Andrew, I am testing out using scaled values. On Tue, 2 Sept 2025, 23:59 Andrew Helwer, <
unread,
Is Dempster Shaffer/Probabilistic Reasoning possible in TLA plus
Thanks Andrew, I am testing out using scaled values. On Tue, 2 Sept 2025, 23:59 Andrew Helwer, <
Sep 7
Andrew Helwer
9
Aug 21
Monthly Development Update newsletter
August 2025 update: GenAI challenge winners announced, a startup paying people to write TLA⁺ spec
unread,
Monthly Development Update newsletter
August 2025 update: GenAI challenge winners announced, a startup paying people to write TLA⁺ spec
Aug 21
abhilash jindal
,
Stephan Merz
2
Aug 16
Proving liveness with TLAPM
Hello, there are very few examples of liveness proofs so far. Essentially you want to do an induction
unread,
Proving liveness with TLAPM
Hello, there are very few examples of liveness proofs so far. Essentially you want to do an induction
Aug 16
Markus Alexander Kuppe
2
Aug 13
GenAI-accelerated TLA+ challenge by the TLA+ Foundation and NVIDIA
🏆 Announcement: Winners of the 2025 TLAi+ Challenge The TLA+ Foundation, in collaboration with NVIDIA
unread,
GenAI-accelerated TLA+ challenge by the TLA+ Foundation and NVIDIA
🏆 Announcement: Winners of the 2025 TLAi+ Challenge The TLA+ Foundation, in collaboration with NVIDIA
Aug 13
Andrew Helwer
, …
Ugur Yavuz
4
Aug 13
The level of the expression or operator substituted for 'Def' must be at most 0
I found myself needing to do something very similar: I'm working on something where I need to
unread,
The level of the expression or operator substituted for 'Def' must be at most 0
I found myself needing to do something very similar: I'm working on something where I need to
Aug 13
Basant Singh
,
Andrew Helwer
2
Aug 2
Getting Started with TLA⁺ for Modeling an EV Charging Ecosystem
Hi Basant, TLA+ certainly can accomplish all of your goals, although it should be noted that it
unread,
Getting Started with TLA⁺ for Modeling an EV Charging Ecosystem
Hi Basant, TLA+ certainly can accomplish all of your goals, although it should be noted that it
Aug 2
thomas...@gmail.com
, …
Michael Leuschel
8
Aug 1
TLC Nat and Integers...still using 32 bit?
Hi, for your information, the ProB tool can also handle some TLA+ specifications. It works on the
unread,
TLC Nat and Integers...still using 32 bit?
Hi, for your information, the ProB tool can also handle some TLA+ specifications. It works on the
Aug 1
Anatoliy Bilenko
, …
William Schultz
7
Jul 30
Model based testing
We also wrote a bit about our recent experiences applying model-based test case generation to
unread,
Model based testing
We also wrote a bit about our recent experiences applying model-based test case generation to
Jul 30
tamarind code
, …
Markus Kuppe
7
Jul 18
How to specify Semmetry sets in config file in visual studio code
And thanks Markus, That was very useful. It confirms the same answer. Thank you for pointing that out
unread,
How to specify Semmetry sets in config file in visual studio code
And thanks Markus, That was very useful. It confirms the same answer. Thank you for pointing that out
Jul 18
Jaco van de Pol
2
Jul 16
CONFEST 2025 (CONCUR, FMICS, QEST+FORMATS): Call for Participation
============================================================== CONFEST 2025: 2nd Call for
unread,
CONFEST 2025 (CONCUR, FMICS, QEST+FORMATS): Call for Participation
============================================================== CONFEST 2025: 2nd Call for
Jul 16
Hillel Wayne
,
Finn Hackett
2
Jul 16
Are there any guides on writing our own PlusCal translators?
I've been thinking a lot about custom tooling workflows in the context of TLA+ recently. As a
unread,
Are there any guides on writing our own PlusCal translators?
I've been thinking a lot about custom tooling workflows in the context of TLA+ recently. As a
Jul 16
Finn Hackett
, …
Samuel Miller
4
Jul 13
Apropos selling formal methods (Galois article link)
Thanks for sharing. I enjoyed the article and think it makes a lot of great points. On Sun, Jul 13,
unread,
Apropos selling formal methods (Galois article link)
Thanks for sharing. I enjoyed the article and think it makes a lot of great points. On Sun, Jul 13,
Jul 13
Andrew Helwer
, …
Irwansyah Irwansyah
12
Jul 10
On a type of TLA+ contract
Hi Andrew, Your answer reflects your vision on the future of TLA+. I don't know what your vision
unread,
On a type of TLA+ contract
Hi Andrew, Your answer reflects your vision on the future of TLA+. I don't know what your vision
Jul 10
[8]
ページ先頭
©2009-2025
Movatter.jp