Sir, How to implement loop in TLA+ spec. Also send me some simple example programs . I m a beginner in TLA+. I covered all the video lectures and eBook . In those videos there is no example to write specs with loop. So please give some examples related to this Regards Renjith S PhD scholar Amrita School of Engg.