当前位置:网站首页>Learn tla+ (XII) -- functions through examples
Learn tla+ (XII) -- functions through examples
2022-07-05 01:41:00 【Liu Xiaojing】
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]
边栏推荐
- es使用collapseBuilder去重和只返回某个字段
- PowerShell: use PowerShell behind the proxy server
- PHP wechat official account development
- Are you still writing the TS type code
- 整理混乱的头文件,我用include what you use
- Can financial products be redeemed in advance?
- Global and Chinese market of nutrient analyzer 2022-2028: Research Report on technology, participants, trends, market size and share
- Summary of regularization methods
- Introduction to redis (1)
- To sort out messy header files, I use include what you use
猜你喜欢
DOM basic syntax
What sparks can applet container technology collide with IOT
Wechat applet: new independent backstage Yuelao office one yuan dating blind box
Phpstrom setting function annotation description
[development of large e-commerce projects] performance pressure test - Performance Monitoring - heap memory and garbage collection -39
Win: use PowerShell to check the strength of wireless signal
Is there a sudden failure on the line? How to make emergency diagnosis, troubleshooting and recovery
ROS command line tool
After reading the average code written by Microsoft God, I realized that I was still too young
Armv8-a programming guide MMU (3)
随机推荐
Huawei machine test question: longest continuous subsequence
When the industrial Internet era is truly developed and improved, it will witness the birth of giants in every scene
The server time zone value ‘� й ��� ʱ 'is unrecognized or representatives more than one time zone【
A simple SSO unified login design
What is the length of SHA512 hash string- What is the length of a hashed string with SHA512?
batchnorm.py这个文件单GPU运行报错解决
Basic operation of database and table ----- phased test II
Global and Chinese market of veterinary thermometers 2022-2028: Research Report on technology, participants, trends, market size and share
Global and Chinese markets for stratospheric UAV payloads 2022-2028: Research Report on technology, participants, trends, market size and share
Global and Chinese market of network connected IC card smart water meters 2022-2028: Research Report on technology, participants, trends, market size and share
Roads and routes -- dfs+topsort+dijkstra+ mapping
Phpstrom setting function annotation description
Database postragesql client authentication
JS implementation determines whether the point is within the polygon range
Hedhat firewall
MATLB | multi micro grid and distributed energy trading
Basic operations of database and table ----- delete index
Global and Chinese markets of emergency rescue vessels (errv) 2022-2028: Research Report on technology, participants, trends, market size and share
Win:使用 PowerShell 检查无线信号的强弱
The perfect car for successful people: BMW X7! Superior performance, excellent comfort and safety