tlaplus

Have downloaded the Ulpian Release to an Ubuntu Machine from https://github.com/tlaplus/tlaplus/

Ok, So I can define. But just not with | Is that right ? On Saturday, April 27, 2024 at 4:19:34 AM

Hello, Maybe this could be a first start on the definition rules: https://gist.github.com/lkraider/

TLAPM is the proof manager, the central component of TLAPS. (The other components are the backend

How can I write the proof for the number of permutations of n distinct objects using TLA ? In the

Hi, I am still new to TLA+. I started by watching the Video Course and plan to read the book

Lighthearted challenge - explain why this is valid TLA+ syntax: ---- MODULE Test ---- op == !!!!!!!!!

Hello, 1. It is mentioned in section 8.9.4 of Specifying Systems that substitution does not

Another advice: in the initial condition, instead of /\ txRequest = [tx \in txs |-> RandomElement(

Proving temporal properties such as termination requires adding fairness conditions to the

If the files MCSpec.tla and MCSpec.cfg exist, the VSCode extension will automatically check them when

For this particular example one thing that can be tried is change spec to EmptyNetwork ==

Hi Jack， I read the MongoRaftReconfig (https://arxiv.org/pdf/2102.11960.pdf), and I like this idea. I

Thank you to those who participated in the community survey. Attached are the results. There's a

> I would expect that the presence of labels would not affect liveness properties. Am I missing

thanks for your good response. Ok, I will check and update my specifications. On Thu, Mar 21, 2024 at

Hi Georgios, labels are very important in PlusCal. Code between a pair of labels runs atomically, and

Never mind, I see the collocated events on the next page. Sorry for spamming. On Tue, 19 Mar 2024 at

On Wed, 13 Mar 2024 at 11:01, Stephan Merz <stepha...@gmail.com> wrote: Thanks for the nice

The executable binary is toolbox inside the toolbox/ directory. I just ran it on my computer and

Below is a distilled version of something I ran into while writing my spec. PlusCal complains that a

I'm glad my understanding is correct. :) The \A \in S : F example is a good one, and I think it

I don't think there's a built-in integration, you'll have to write a script to generate .

yes, thank you. just was surprised a little bit by the PlusCal translator Andrew понедельник, 11

Hi Jesse and Igor, From the description of the algorithm in the Attiya-Welch book, one can see that

An extensively revised draft of A Science of Concurrent Programs is available at the same place.

I'd like to get my custom trailer on my GoogleGroup to be monospaced. Can I add code to the

Oh goodness. I think this works if you provide the spec name that isn't the same as the one

Does that mean that it wouldn't be possible switch based on type? For example: doTheThing(x) ==

Recursive operator definitions were not part of TLA+ when Specifying Systems was written. Their