[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: TLA+ for beginners

On Friday, November 25, 2016 at 5:12:17 AM UTC-8, Abay Kozhabergenov wrote:

So, can you help how to begin the model checking and the formal proof for my case in TLA+, please?

 Good tutorial will be very useful.

Hi Abay,

You may want to look at [1] and [2]. There are also some posts in this Google group with relevant comments that
can be found by searching for "real time" at the top, for example [3].

[1] https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#real-simple
[2] Ch.9 in the TLA+ book, https://research.microsoft.com/en-us/um/people/lamport/tla/book.html
[3] https://groups.google.com/d/msg/tlaplus/uw7ZtLVQPLo/bw3_BKGeFAAJ

Best regards,