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

[Renjith Sasidharan <renjit...@xxxxxxxxx>]

Sir,

Thanks for your valuable feedback . I will check it and I request you
to continue this support

Regards
Renjith S

On Wed, Jul 25, 2018 at 12:24 PM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
> Hello,
>
> 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.
>
> Regards,
> Stephan
>
>
> On 25 Jul 2018, at 06:45, Renjith Sasidharan <renjit...@xxxxxxxxx> wrote:
>
> 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.
>
> --
> 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.
>
>
> --
> 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.