通过例子学TLA+(六)--标准模块

标准模块

使用标准模块有两个原因。首先，当规范使用我们已经熟悉的基本操作符时，它们更容易阅读。其次，工具如TLC可以内置这些标准操作符。目前的内置模块主要有：数字相关的模块Naturals,Integers,Reals,以及Sequences，FiniteSets，Bags

数字模块

常用的整数和运算符集定义在Naturals、Integers和Reals三个模块中。

Naturals Module 定义了以下操作符

加+  减-  乘*  除/  取余%  小于<  大于>  小于等于<=  大于等于>=  区间..  自然数Nat  取幂^

Integers Module扩展了 Naturals Module，并定义了包含负数的整数Int和负号。

Reals Module 则是扩展了 Integers Module 并包含了实数。Reals Module 中定义了 Infifinity 用来表示无穷符号。

∀ r ∈ Real : −Infinity < r < Infinity               − (−Infinity) = Infinity

Sequences

Sequences Module在之前的例子中已经介绍过了，这里增加一些介绍

SubSeq(s, m, n)  包含了序列s中第m到第n个元素的子序列（m < n）如果m > n 则返回空序列，如果m < 1 或者 n > Len(s) 则结果是未定义的
SelectSeq(s, Test) 由序列s中的元素组成的子序列，并且这些元素都能够满足Test。例如：SelectData(s) == LET Greater(n) == N > 5IN  SelectSeq(s,Greater) 上述意思为选择序列s中大于5的元素当s为<<1,3,5,7,9>>时，SelectData(s) 为<<7,9>>

FiniteSets

FiniteSets是有限集合，新定义了两个操作

IsFiniteSet(S) 当且仅当集合S为有限集返回TRUE
Cardinality(S) 如果S是有限集合，返回S中的元素个数。空集合返回0。

Bags

一个bag也可以称作multiset，可以包含重复元素的Set。

IsABag(b) 如果b是bag，返回TRUE
BagToSet(b) 将bag b中的元素转换为set
SetToBag(s) 将set s转换为bag
BagIn(e,b) 元素e在bag b中，返回TRUE
EmptyBag   没有元素的bag，即空bag
CopiesIn(e,b) 返回元素e在bag b中的数量，如果e不在b中，返回0
b1 (+) b2  合并b1,b2
b1 (-) b2  从b1中删除存于b2中的元素

通过例子学TLA+(六)--标准模块相关推荐

通过例子学TLA+(十三)--多进程与await
多进程之前使用的例子都是单进程的,现在用多进程来描述多个逻辑同时发生,TLA+中的多进程可以理解为其他高级语言中的多线程.为了方便理解,使用Pluscal语言来描述,TLA+ Toolbox可以将p ...
通过例子学TLA+（一）-- HourClock
前言刚接触TLA+,将学习过程中的理解整理记录下来,用于加深理解和备忘.有对TLA+感兴趣的可以私信我,一起学习. TLA+简介 TLA+ 是一门形式规格说明语言(formal specificat ...
通过例子学TLA+(十)--集合
集合集合用大括号来表示,如{1,2},对于连续的数字集合有种特殊的表示方式,如 1-3 表示集合{1,2,3} 下表是集合的常见操作 Operator example 备注 \in 1 \in {1 ...
通过例子学TLA+(八)--表达式
表达式在之前的例子中,已经多次用到了表达式,常见的表达式中会用到大于,小于,等于,不等于等这样条件判断.还有一些其他的用法,比如逻辑连接,IF-ELSE 等逻辑连接逻辑连接在之前的例子中是用过 ...
通过例子学TLA+(五)--FIFO Sequences
FIFO 本例子是一个先进先出FIFO的Buffer.Sender向Buff发送数据,Buffer接收数据存储在Sequence中,然后,Buffer将Sequence中第一个数据取出发送给Recei ...
通过例子学TLA+(二) -- DieHard
第二个例子DieHard 这是一个倒水的例子,初始一个3升容量的桶,一个5升容量的桶,水不限,如何倒出一个容量刚好是4升的水.在一部老电影DieHard中主角就面临这个问题,这里就将module名命名 ...
通过例子学TLA+(十五)--时序属性
时序属性 Termination 最简单的时序属性是Termination,Termination是算法终止的要求,如果算法崩溃或者死锁或者进入一个无限循环,那么久违反了Termination规范. ...
通过例子学TLA+(十四)--宏，过程与标签
宏,过程与标签 TLA+在多进程之间复用代码,最简单的方法是使用宏和过程. 宏宏是通用的代码内联器,格式为 nacro Name(var1,...) begin\* stuff end macro; ...
通过例子学TLA+（四）-- Send Rev Print
Send & Rev 稍微复杂点的程序中都会涉及数据的发送与接收,本例子基于发送器Sender与接收器Receiver来实现数据的变更.假设Sender发送一个数据给Receiver,Rece ...