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