THEOREM Spec => []Invariant<1>1. Init => Invariant
--
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 post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
Hi Petar,
Stephan is probably right about showing the model checker rather than
the proof system. However, it's impossible to give you good advice
without knowing more about your presentation--in particular, who it's
for, what its purpose is, and how much time you have. You might want
to look at one or more of the presentations I've given that have been
recorded and put on the Web. The one that I expect is most relevant
is at
http://www.heidelberg-laureate-forum.org/blog/video/lecture-monday-august-24-2015-leslie-lamport/
You might also suggest that your professor watch it.
Good luck,
Leslie