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

Re: [tlaplus] Error in spec Reg / Loop structure


the GitHub page https://github.com/tlaplus/Examples contains various examples, more to come!

You will find traditional control structures, including loops, in PlusCal. TLA+ has no built-in notion of control: typically you use an explicit "program counter" variable if you need one. But often you don't: look at the specification of the Alternating Bit protocol, which has cyclic behavior but doesn't require an explicit loop structure. Also note that you don't have to write as many loops as in ordinary programs because you can use quantifiers, for example for identifying an element of an array satisfying some predicate.


On 25 Jul 2018, at 06:45, Renjith Sasidharan <renjit...@xxxxxxxxx> wrote:


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

Renjith S
PhD scholar
Amrita School of Engg.

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.