此页面上的图14.5中的标准TLC模块定义了使用TLC时方便使用的运算符。TLC运行的模块通常会EXTENDS TLC模块,该模块会被其Java实现所覆盖。
模块TLC以如下语句开始:
LOCAL INSTANCE Naturals
如第171页中所述,这类似于EXTENDS语句,不同的是,任何其他EXTENDS或INSTANCE模块TLC的模块都无法获取Naturals模块中包含的定义。同样的,下一条语句在本地实例化Sequences模块。
接下来,模块TLC定义了三个运算符Print,Assert和JavaTime。它们仅在运行TLC调试模块时有用,可以帮助您查找跟踪问题。
定义运算符Print,使Print(out,val)等于val。但是,当TLC评估此表达式时,它将打印out和val的值。您可以将打印表达式添加到specification中以帮助定位错误。例如,如果您的specification包含
∧Print("a",TRUE)∧P∧Print("b",TRUE)
并且TLC在报告错误之前打印"a"而不打印"b",然后在TLC评估P时发生错误。如果您知道错误在哪里但不知道为什么会发生,则可以添加Print表达式,以向您提供有关TLC计算值的更多信息。
要了解什么时候打印什么,您必须知道TLC如何计算表达式,这在14.2和14.3节中有解释。TLC通常会对表达式进行多次评估,因此在specification中插入Print表达式会产生大量输出。限制输出量的一种方法是将Print表达式放在IF/THEN表达式内,因此仅在感兴趣的情况下执行。
接下来,TLC模块定义运算符Assert,如果val等于TRUE,则
Assert(val,out)等于TRUE。如果val不等于TRUE,则评估
Assert(val,out)会使TLC打印out的值并停止。 (在这种情况下,
Assert(val,out)的值无关紧要)。
扫描二维码关注公众号,回复:
8804217 查看本文章
接下来,将运算符JavaTime定义为等于任意自然数。但是,TLC在评估时不遵循JavaTime的定义。取而代之的是,对JavaTime进行评估时才会得出进行评估的时间,以自1970年1月1日世界标准时间00:00以来经过的毫秒数为单位,再模
231。如果TLC生成状态的速度很慢,则将JavaTime运算符与Print表达式结合使用可以帮助你明白为什么会这么慢。如果TLC花费太多时间评估一个运算符,则可以换一个等价的更有效率的的运算符。(请参阅第234页的14.2.3节。)
接下来,TLC模块定义运算符:>和@@,表达式
d1:e1@@⋯@@dn:en是一个值域为
{d1,⋯,dn}, 且对
i=1,⋯,n,
f[di]=ei的函数。例如,序列
⟨"ab","cd"⟩,是一个值域为
{1,2}的函数,可以写成
1:>"ab"@@2:"cd" TLC使用这些运算符来呈现待打印的函数值或者报告一个错误,不过,习惯上一般以在specification中出现的方式打印值,因此通常将序列打印为序列,而不是使用:>和@@运算符。
接下来,如果S是有限集,则将Permutations(S)定义为S的所有排列的集合。可以使用Permutations运算符为上面第14.3.4节中描述的SYMMETRY语句指定一组排列。可以通过定义一个集合
{π1,⋯,πn}来使用更复杂的对称性,集合中每一个
πi都是一个显式函数,可以用:>,和@@运算符编写。例如,考虑一个存储系统的specification,其中每个地址都以某种方式与处理器相关联。该specification在两种排列下是对称的:一种排列是与同一处理器关联的地址,另一种排列是与一组地址有关联的处理器。假设我们告诉TLC使用两个处理器和四个地址,其中地址a11和12与处理器p1相关联,并且地址a21和a22与处理器p2相关联。通过为TLC提供以下以下排列组合作为对称集,可以使TLC充分利用对称性:
Permutations({a11,a1})∪p1:p2@@p2:p1@@a11:a21@@a21:a11@@a12:a22@@a22:a12
排列
p1:>p2@@⋯@@a22:>a12交换处理器及其关联的地址。只是互换a21和a22的排列不需要明确指定,因为它是通过交换处理器,交换a11和a12并再次交换处理器获得的。
TLC模块通过定义运算符SortSeq结束,它可以用于将运算符替换为更有效率的TLC运算符。如果s是有限序列,
≺是其上的完整排序关系(排序算子)SortSeq(s,
≺)是s经过
≺排序得到的新序列。举例来说,SortSeq(< 3, 1, 8, 1>,
≺)等于<8,3,3,1>. SortSeqde的JAVA实现让TLC更有效率地实现排序算法。举例如下:下面是我们用SortSeq定义一个FastSort操作符去替换235页定义的Sort操作符:
FastSort(S) ≜LET MakeSeq[SS∈ SUBSET S]≜IF SS={}THEN ⟨⟩ELSE LET ss≜ CHOOSE ss∈SS: TRUE IN Append (MakeSeq[SS\{ss}], ss )IN SortSeq(MakeSeq [S],<)