本节通过一个小时时钟示例,演示了如何定义一个简单的系统,给出它的TLA+形式的规约:
HC≜HCini∧□[HCnxt]hr 其中
-
hr为小时读数状态变量:
-
HC表示小时时钟系统规约;
-
HCini是系统初始状态,目前定义为
HCini≜hr∈{1,…,12};
-
□[HCnxt]hr,是
□(HCnxt∨(hr′=hr))的简写形式,
HCnxt≜hr′=IF hr=12 THEN hr+1 ELSE 1,这个公式表征系统的下一步状态需要满足的条件,即
hr递增或保持不变;
几个重要概念:
- 初始谓词(initial predicate):状态变量初始值定义,如上
HCini;
- 步骤(step):一对连续的状态;
- 下一状态关系(next-state relation):该关系指定任何步骤中状态变量如何变化;
- 动作(action):除既包括含
′的变量,也包括不含
′的变量外,其他和普通数学公式一样。“动作”表示“步骤”的值为真或假。满足“动作”
HCnxt的“步骤”,我们称为
HCnxt步骤。;
让我们从一个非常简单的系统开始——一个只显示小时的数字时钟,它是一个循环显示从1到12读数的设备(为了使系统变得简单,我们忽略显示和实际时间之间的关系)。如果让变量
hr代表小时读数,时钟的典型行为是下面这样的状态序列:
(2.1)
[hr=11]→[hr=12]→[hr=1]→[hr=2]→⋯
其中
[hr=11]是变量
hr值为11的状态。一对连续的状态,如
[hr=11]→[hr=12],称为“步骤”(
step)。
为了定义时钟,我们需要描述它所有可能的行为。我们先写一个“初始谓词”(
initialpredicate),它指定了
hr可能的初始值。和一个“下一状态关系”(
next−staterelation),该关系指定在任何步骤中
hr的值如何变化。
我们不希望精确地指定时钟最初的读数,任何小时数都可以。因此,我们希望初始谓词声明
hr可以是从1到12的任何读数。我们称初始谓词为
HCini,下面是非正式地定义:
HCini≜hr∈{1,…,12}在之后我们会学到如何正式定义它,不带“
…”这样表示“等等”的非正式描述。
“下一状态关系”
HCnxt是表示某一步骤新旧状态hr值之间关系的公式。我们让
hr代表
hr在旧状态下的值,
hr′代表
hr在新状态下的值(
hr′中的
′读作“piě”)。我们希望“下一状态关系”声明
hr′等于
hr+1,除非
hr等于12,在这种情况下
hr′应该等于1。使用意义明显的IF/THEN/ELSE结构,我们可以这样定义:
HCnxt≜hr′=IF hr=12 THEN hr+1 ELSE 1
HCnxt除了既包括含
′的变量,也包括不含
′的变量外,其他和普通数学公式一样。这样的公式我们称之为“动作”(
action)。“动作”表示“步骤”的值为真或假。满足“动作”
HCnxt的“步骤”,我们称为
HCnxt步骤。
每当
HCnxt步骤出现,我们有时会说
HCnxt被执行了。不过,严格地说这是错误的表述。“动作”是公式,公式不能被执行。
我们希望规约是一个单独的公式,而不是一个公式对(
HCini,
HCnxt)。这个单独的公式应该声明一个这样的“行为”:
(i)其初始状态满足
HCini
(ii)其每一步均满足
HCnxt
我们将(i)表示为公式
HCini,将其解读为行为的一个陈述,即初始状态满足
HCini;为了表示(ii),我们使用时态逻辑运算符口(发音为“方块”)。时态公式
□F断言公式
F总是为真。特别的,
□HCnxt断言
HCnxt对于行为中的每一步都为真。则公式
HCini∧□HCnxt对一个“行为”为真 当且仅当 其初始状态满足
HCini,且每一步都满足
HCnxt 。这个公式描述了所有如(2.1)这样的行为,这似乎就是我们要找的那种规约。
如果我们只单独考虑时钟,而从不试图将它与其他系统联系起来,那么这将是一个很好的规约。但是,假设这个时钟是一个更大系统的一部分——例如,显示当前时间和温度的气象站显示屏:其状态由两个变量描述:表示小时读数的
hr,表示温度读数的
tmp,考虑一下气象站的这种行为:
[hrtmp==1123.5]→[hrtmp==1223.5]→[hrtmp==1223.4]→[hrtmp==1223.3]→[hrtmp==123.3]→⋯
在第二和第三步中,
tmp有变化而
hr保持不变,这在
□HCnxt中是不允许的,因其声明每一步
hr都会递增,所以公式
HCini∧□HCnxt不能用来描述气象站的时钟读数显示。
描述任何时钟读数的公式必须允许出现
hr保持不变的步骤,即
hr′=hr步骤,这被称为时钟的“重叠步骤”。时钟的规约应该允许
HCnxt步骤和重叠步骤。因此,一个步骤是“容许”的当且仅当这一步是
HCnxt步骤或重叠步骤,也就是满足公式
HCnxt∨(hr′=hr))。这表明,我们可以采用
HCini∧□(HCnxt∨(hr′=hr))作为我们的规约。在TLA中,我们用
[HCnxt]hr代替
HCnxt∨(hr′=hr),这样之前的公式可以简写成
HCini∧□[HCnxt]hr
公式
HCini∧□[HCnxt]hr确实容许重叠步骤,事实上,它容许如下的行为:
[hr=10]→[hr=11]→[hr=11]→[hr=11]→⋯其最后是无限个重叠步骤。这个行为描述了一个时钟,它的最后读数为11,然后永远保持这个值——换句话说,一个时钟在11停止。以同样的方式,我们可以用一种无限的行为来表示任何系统的终止执行,这种行为以一串重叠步骤序列结束。我们将不再需要只限定分析有限的行为(有限状态序列)了,可以只考虑无限行为。
要求时钟永不停止是很自然的约束,所以我们的规约应该声明有无限多个非重叠步骤。第8章描述了如何表达这一要求。现在,我们满足于可以停止的时钟,时钟规约定义如下:
HC≜HCini∧□[HCnxt]hr