learning tla+ strategy

[Alex Tim]

Hello.

Can you please specify the recommended strategy for tla+ learning.

Before writing practical specs i think its better to get full comprehension of all available features and techniques (including proofs, leveraging auxiliary vars etc)

By now I've studied the video course and tla+ auxiliary vars. I'm reading tla+2 guide now to learn proofs and tlaps. What should be next? Specifying systems or Practical TLA+?

Thanks in advance. Alex.

[Stephan Merz]

It really depends on what you are intending to use TLA+ for. I'm assuming that you are interested in using TLA+ for specifying and verifying some actual system. The video course and Practical TLA+ should be your first steps. Auxiliary variables is advanced stuff that you are unlikely to need in most practical cases. If you want to look at some more introductory material, you may want to consider reading the Hyperbook. But I'd recommend that in parallel you work on your own specs and go back to reading when you are lost.

My 2 cents,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/62c2f9db-77a1-4987-8091-a7ae4749e82a%40googlegroups.com.

[Alex Tim]

Thanks, Stephan!!!

четверг, 23 апреля 2020 г., 13:37:36 UTC+3 пользователь Stephan Merz написал:

It really depends on what you are intending to use TLA+ for. I'm assuming that you are interested in using TLA+ for specifying and verifying some actual system. The video course and Practical TLA+ should be your first steps. Auxiliary variables is advanced stuff that you are unlikely to need in most practical cases. If you want to look at some more introductory material, you may want to consider reading the Hyperbook. But I'd recommend that in parallel you work on your own specs and go back to reading when you are lost.

My 2 cents,

Stephan

On 23 Apr 2020, at 12:24, Alex Tim <alex....@gmail.com> wrote:

Hello.

Can you please specify the recommended strategy for tla+ learning.

Before writing practical specs i think its better to get full comprehension of all available features and techniques (including proofs, leveraging auxiliary vars etc)

By now I've studied the video course and tla+ auxiliary vars. I'm reading tla+2 guide now to learn proofs and tlaps. What should be next? Specifying systems or Practical TLA+?

Thanks in advance. Alex.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.