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,
ioannis