tlaplus

It should be noted that unicode symbol quality varies pretty widely by font. You also will want a

Thanks Will and Stephan for your answers. Is it OK then to say that [][Next]_vars will allow

When running tlapm [1], the command line tool for TLAPS, is there any functional difference between

> In general, if we work over only finite domains, can't all SMT problems, in theory, be

To correct the syntax of the above, actually you omit the placeholders in the substitution statements

Where can I find language standard documents and other things relating to PlusCal? I don't mean

To follow up on this, you may be able to use TLC to check the CTL formula AG(P1) => EF(P2) with

On 9/4/21 6:51 PM, Clifford Heath wrote: > Is there a more readable syntax for TLA+ somewhere?

Not exactly related, but there is the Apalache project: https://apalache.informal.systems/. This is a

Thanks for answering. This is exactly what I was looking for, don't worry about disagreeing with

After some back and forth between different encodings, I got to learn a little more TLA+ and would

Disabling deadlock checking is standard practice when verifying algorithms whose executions are

Interesting, thanks! This is more or less what I figured. It turns out this is a feature I was

Hello Markus, > You will have to create a benchmark to determine if performance differs >

Hi Hengfeng, Building on previous efforts, I recently developed one such model checking technique

Great tips, thanks. On Thu, Aug 5, 2021 at 2:19 PM Markus Kuppe <tlaplus-google-group@lemmster.de

Hi Young, Yes, I have done something similar, you can also ping me at https://twitter.com/pfeodrippe?

I'm sorry, but I have to come back at this. I know that the general sentiment is not to fix

On 7/26/21 4:31 AM, Andrew Helwer wrote: > However this then caused TLC to output a novel (to me)

Tried to check this proof as well. But I'm getting the following error when using tlapm from the

If you're mechanically translating policy lists to TLA+ to check them, it might not be the most

Section 16.2.4 gives a syntactic definition of a valid TLA formula, which is defined inductively from

The program of TLA+ Conf is now up at http://conf.tlapl.us/2021/ Markus

Oh, I see. Thank you, Markus On Thursday, July 15, 2021 at 6:05:04 PM UTC+3 Markus Alexander Kuppe

Consider A == x /\ x' = FALSE B == ~x /\ x' = TRUE Then ENABLED A <=> ~(ENABLED B). H

I feel like the programmer in me understood fairness a lot better when I learned how liveness is

Sweet. Works like a charm. And page numbers fixed too! Now if only we could click and goto the page

So turns out the US holiday weekend made the deadline tricky for some people, so we're extending

On Jun 30, 2021, 11:23 AM -0700, Markus Kuppe <tlaplus-google-group@lemmster.de>, wrote: On 6/

Ah that makes perfect sense! I ended expanded the definition according to Specifying Systems (\A n \