Algorithmic Notation Sample Clauses

Algorithmic Notation. ‌ In this thesis we present algorithms as state machines, specified in terms of atomic actions, state functions, and operators. The notation we use to define each of them should to be less ambiguous than the normally used pseudo-code, but more easily readable than the TLA+ [Lamport, 2002a] specifications in which we have specified our main algorithms. An action can only be executed if all of its pre-conditions are satisfied, in which case we say that the action is enabled. An enabled action executes atomically and changes the state machine accordingly. State functions evaluate some condition over the state of the state machine and are useful to express properties; a state function that evaluates to a boolean value is called a state predicate. Operators are functions that operate on a set of parameters. Agents are divided in sets according to their roles. Hence, checking if an agent plays a given role is the same as checking its inclusion in the respective set. Agents keep their state in variables indexed by their names. In the following specification, for example, the action FlipIfZero is enabled for an agent a of type flipper that has its variable var[a] equal to 0. If the action is executed, var[a] is flipped to 1. Most keywords that we use have obvious meanings. For example, the If (a, b, c) operator defined above evaluates to b if a is true and to c otherwise. Another exam- ple is the pair LET and IN, which specifies the scope of a definition. In the definition of SumSeq(seq) above, for example, Sum is defined as a recursive function that iter- ates over the elements of a sequence summing them, but only inside SumSeq. For