tlaplus

Will do On Thu, Mar 4, 2021 at 4:37 PM Markus Kuppe <tlaplus-google-group@lemmster.de> wrote:

Leslie, I completely agree! I try to answer questions and engage when I can. I do have to say that

On 03.03.21 13:56, Hillel Wayne wrote: >> Q2: While running the TLC model checker, I got output

Edited the message and forgot to change the subject. However, to explain the problem related to the

On 1 Mar 2021, at 02:28, Andrew Helwer <andrew.helwer@gmail.com> wrote: Is VIEW documented

Hi Ref, I posted a related thread (https://groups.google.com/g/tlaplus/c/JZaBcIhA1UY) as I have been

Very clear. Thank you, Stephan. On Saturday, February 27, 2021 at 9:25:12 AM UTC+1 Stephan Merz wrote

Hi Isaac o/ Can you run TLC from the command-line with the `-debug` flag set? Maybe you will have a

Hello, you did the right thing when you used TLC to get confident that your invariant is indeed

Hi Stephan Thanks for the answer ! Felipe Em terça-feira, 23 de fevereiro de 2021 às 13:56:46 UTC+1,

The GitHub link is not valid anymore but it looks like you constructed a function of the form forks =

Ah yes that's right, because of stuttering steps. Of course! Thank you Stephan. On Sunday,

Hi, Is there a way of setting the page margins when producing a PDF document from a TLA+ spec? I know

Hi Tim, This is not a bug; it's an example of why a program can't have a bug if it doesn'

The paper has been publicly available for quite some time. Chris posted that announcement some 8

I may not be adding much to the discussion but I understood many TLA+ constructs a lot better when I

I have a question or two regarding spec refinement. Suppose I can show that some component ComptL is

thank you! On Monday, February 15, 2021 at 2:41:58 PM UTC-8 ron.pr...@gmail.com wrote: WF_vars(A) is

Thank you, Markus. On Sun, Feb 14, 2021 at 3:09 PM Markus Kuppe <tlaplus-google-group@lemmster.de

In this final version, I promoted the check to a THEOREM. It's perhaps more idiomatic. ----------

Yes, I seem to be using the two terms to mean the same thing. I'm sorry for the confusion; thanks

I've written a module that specifies depth-first search over a directed graph. I now want to

Great, that's exactly what I was looking for. Thanks a lot. On Fri, Feb 12, 2021, 1:19 PM Stephan

Thank you all for the help. I ended up using IF .. THEN .. ELSE TRUE, which seemed easiest. On

Thanks, Markus! On Thu, Feb 11, 2021 at 5:08 PM Markus Kuppe <tlaplus-google-group@lemmster.de>

Hi Markus, Since it appears that a significant number of people run TLC from the command line, it

Thank you for your response. I understand that it's wrong, the way that I added 'canAdd'.

Check pdf tools command settings .I think the message means that such a tool command is not provided

http://lamport.azurewebsites.net/tla/tla.html On 11 Feb 2021, at 12:15, Muhammad Irfan <

I'll just add this here as it may help somebody in the future track down this problem if they