集合

集合用大括号来表示，如{1,2}，对于连续的数字集合有种特殊的表示方式，如 1…3 表示集合{1,2,3}

下表是集合的常见操作

Operator	example	备注
\in	1 \in {1,2} 为true 1\in {{1},2}为false	在集合为true，不在为false
\notin	1 \notin {} 为true {1} \notin {{1}}为false	与\in相反
\subseteq	{1,2} \subseteq {1,2,3}	是子集为true
\union	{1,2} \union {2,3} = {1,2,3}	并集，重复元素只保留一个
\intersect	{1,2} \intersect {2,3} = {2}	交集
S1 \ S2	{1,2} \ {2,3} = {1}	差集，在S1中，不在S2中
SUBSET S	SUBSET {1,2} = {{}，{1}，{2}，{1,2}}	S的所有子集，包括空和自身
UNION S	UNION {{1},{1,2},{5}} = {1,2,5}	等价于{1} \union {1,2} \union {5}

有个标准MODULE FiniteSets ，有两个operators,

operator	example	备注
IsFiniteSet(S)	IsFiniteSet({1，3}) = TRUE	S为有限集合返回True
Cardinality(S)	Cardinality({1,3}) = 2	但S为有限集时，返回元素个数

过滤器

可以对集合进行过滤，格式为{x \in S : P(x)}，其中S为集合，x为集合中元素，P为过滤条件，返回满足过滤条件的元素的集合，其中P必须返回一个布尔值，否则将会报错。

例如：

{x \in 1..8 : x % 2 = 1} = {1,3,5,7}

如果S是元组集合，可以用<<…>> \in S 来访问元素

例如：

{<<x,y>> \in {1,2} \X {1,2} : x>=y} = {<<1, 1>>, <<2, 1>>, <<2, 2>>}

过滤器可以嵌套使用，例如

{x \in {y \in S : P(y)} : Q(x)}  等价于 {x \in S: P(x) /\ Q(x)}

映射

映射的格式与过滤器相反：{P(x): x \in S} ，如果P是布尔表达式则结果集就是布尔值的集合。

例如：

{ x * x : x \in 1..4 } = {1,4,9,16}
{ x % 2 = 1: x \in 1..8 } = {TRUE,FALSE}T == <<1,2,3>>
{ T[x] : x \in DOMAIN T } = {1,2,3} \* 将元组转化为集合

CHOOSE

格式为：CHOOSE x \in S : P(x) 意思是从有限集S中选择一个满足P条件的元素

例如

 CHOOSE x \in 1..8 : x % 2 = 1  满足条件的1,3,5,7都可能是返回值。

需要说明的是采用CHOOSE则认为S中至少有一个满足P的元素，否则TLC将会引发错误。

实例

给定一个集合S，编写一个返回所有长度为 2 的子集的运算符，如 Op(1…3) = {{1, 2}, {1, 3}, {2, 3}}

\* 将该问题分解 1、获取S的所有子集， 2、计算每个子集的长度 3、过滤出子集长度为2的集合
Op(S) == { subset \in SUBSET S : Cardinality(subset) = 2 }

通过例子学TLA+(十)--集合相关推荐

通过例子学TLA+(十二)-- 函数与实例
函数和实例函数 TLA+中除了数字,字符串,布尔值,模型值 4种基本类型外,还有两种复杂类型,分别为集合和函数.函数构成了所有实用复杂类型的基础. 函数的形式看起来跟之前介绍过的操作符是一样的.函 ...
通过例子学TLA+(十五)--时序属性
时序属性 Termination 最简单的时序属性是Termination,Termination是算法终止的要求,如果算法崩溃或者死锁或者进入一个无限循环,那么久违反了Termination规范. ...
通过例子学TLA+(十四)--宏，过程与标签
宏,过程与标签 TLA+在多进程之间复用代码,最简单的方法是使用宏和过程. 宏宏是通用的代码内联器,格式为 nacro Name(var1,...) begin\* stuff end macro; ...
通过例子学TLA+(十三)--多进程与await
多进程之前使用的例子都是单进程的,现在用多进程来描述多个逻辑同时发生,TLA+中的多进程可以理解为其他高级语言中的多线程.为了方便理解,使用Pluscal语言来描述,TLA+ Toolbox可以将p ...
通过例子学TLA+(五)--FIFO Sequences
FIFO 本例子是一个先进先出FIFO的Buffer.Sender向Buff发送数据,Buffer接收数据存储在Sequence中,然后,Buffer将Sequence中第一个数据取出发送给Recei ...
通过例子学TLA+(九)--元组和结构体
元组元组和其他语言中的数组类似,用<<>>表示,不同之处在于TLA+中元组下标是从1开始. x == <<4, 5, 6>>; x[1] + x[2] ...
通过例子学TLA+（一）-- HourClock
前言刚接触TLA+,将学习过程中的理解整理记录下来,用于加深理解和备忘.有对TLA+感兴趣的可以私信我,一起学习. TLA+简介 TLA+ 是一门形式规格说明语言(formal specificat ...
通过例子学TLA+(八)--表达式
表达式在之前的例子中,已经多次用到了表达式,常见的表达式中会用到大于,小于,等于,不等于等这样条件判断.还有一些其他的用法,比如逻辑连接,IF-ELSE 等逻辑连接逻辑连接在之前的例子中是用过 ...
通过例子学TLA+(二) -- DieHard
第二个例子DieHard 这是一个倒水的例子,初始一个3升容量的桶,一个5升容量的桶,水不限,如何倒出一个容量刚好是4升的水.在一部老电影DieHard中主角就面临这个问题,这里就将module名命名 ...

通过例子学TLA+(十)--集合

集合

过滤器

映射

CHOOSE

实例

通过例子学TLA+(十)--集合相关推荐

最新文章

热门文章