Learn tla+ (XII) -- functions through examples

Functions and examples

function

TLA+ In addition to Numbers , character string , Boolean value , Model value 4 There are two basic types , There are also two complex types , Set and function . Functions form the basis of all practical complex types .

The form of the function looks the same as the operators introduced before . There are two ways to define functions ：

Function == [s \in S |-> foo]  \*  here foo It can be any equation . Notice I'm using theta |->, No :
Function[s \in S] == foo 

Infinite sets can be used in function definitions , Such as

Doubles == [n \in Nat |-> 2*n ] 
Doubles[12] = 24 \*  The call mode is [], instead of ()

\*  multi-parameter 
Sum == [x, y \in 1..10 |-> x + y] \* Limit the x,y The value of the 1..10 in 
Sum[2,3] = 5
Sum[2,30]    \* error,30 be not in 1..10 in 

Addx(x) == [y \in Nat |-> x+y+1]
Addx(2)[3] = 6  \* This call x=2,y=3

Set of functions

The syntax of the function set is ：SetOfFunctions == [A -> B], Notice I'm using theta -> , instead of |->. -> The result of needs to be used |-> To describe . for example ：

S1 == {1, 2}
S2 == {3, 4}
[s \in S1 |-> S2] = [1 |-> {3, 4}, 2 |-> {3, 4}] = <<{3,4},{3,4}>> \*  This is a tuple 
[S -> S] = {[1 |-> 3, 2 |-> 3], [1 |-> 3, 2 |-> 4], [1 |-> 4, 2 |-> 3], [1 |-> 4, 2 |-> 4]} = {<<3, 3>>, <<3, 4>>, <<4, 3>>, <<4, 4>>} \*  This is a collection ,[1 |-> 3, 2 |-> 3] Medium 1 Represents the first element ,2 For the second element , If you will 1,2 Replace with 2,3, It cannot be expressed as <<3,3>> 了 , It can only be expressed as [2|->3,3|->3]

example

1、 Given a string , Returns the number of each character . Such as ： Given <<“a”,“b”,“a”>> return [a |-> 2, b |-> 1]

\* 1  Convert tuples into sets , At this time, the set contains elements of non repeating tuples  2  Traversing set elements , Count the number of each element in the tuple 
Range(S) == {S[t]:t \in 1..Len(S)} 
Counter(str) == [c \in Range(str) |-> Cardinality({n \in 1..Len(str) : str[n] = c})]

Counter(<<"a","b","a">>) = [a |-> 2, b|-> 1]

2、 Given a set S And number N, return N individual S Cartesian product of , Such as Op(S, 3) == S \X S \X S

Op(S,N) == [1..N -> S]