第3章迁 移 系 统







本章学习目标

(1) 掌握迁移系统的基本概念及其应用。

(2) 掌握迁移系统到迁移图的转换。
使用形式化方法，通常需要首先对被检测的(并发)系统进行形式化建模。由于并发系统比串行系统表现出更为复杂的并发行为，其形式化模型必须能很好地表达并发性。根据并发行为的方式，并发系统的计算模型可分为交错“交错”一词最初由E.W.Dijkstra于1971年提出。(interleaving，也称交替)模型和非交错(noninterleaving)/独立(independent)模型两大类。其中交错模型是通过各个原子迁移以不确定的顺序交错执行来表示并发行为的，其计算行为表现为状态迁移序列，不允许两个并行进程在相同的时间点上执行它们各自的语句，要求其中一个进程执行时，其余进程处于非激活状态，不允许干扰(interference)情形出现。

迁移系统(transition system)是R.M.Keller最初于1976年提出的一种基于交错并发执行方式的计算模型，也是描述计算机软硬件系统行为的基本抽象模型。迁移系统可以对处于不同情况下的并发系统建模，如可以是在进程完全自动运行的简单情况下，也可以是在进程间以某种方式通信的更现实的环境中。本章主要介绍迁移系统及相关概念，简要阐述迁移图的概念和其到迁移系统的转换，并通过实例说明迁移系统的具体应用。

3.1基 本 概 念

在迁移系统中，一个迁移表示系统的一个原子操作，系统可以处于有限或无限数量的状态中的某一个； 在每个状态上，系统可以执行一系列原子迁移中的一个，这一系列迁移就是该状态可行(使能)的迁移，其他迁移是不可行(非使能)的； 在每个状态中选择一个可行的状态，将系统迁移为一个新的状态，只要至少有一个可行状态，则该过程不断继续。

3.1.1形式定义

状态用于描述系统在某个时刻的行为信息，例如，一个交通灯的一个状态表示了灯当前的颜色。类似地，一个串行程序的一个状态表示了所有程序变量当前的值和程序计数器当前的值(该值指定了下一个将被执行的程序语句)。在一个时序电路中，一个状态表示了寄存器当前的值和输入位的值。

迁移表示系统如何从一个状态转换为另一个状态。在交通灯的例子中，迁移可以表示交通灯从一种颜色转换到另一种颜色。对串行程序来说，一个迁移对应一个语句的执行，也可以包含一些变量和程序计数器值的改变。在时序电路中，一个迁移是指寄存器值的改变和在一组新的输入下输出位的改变。

迁移系统包含迁移(状态的改变)的动作名称和状态的原子命题。动作名称将被用来描述进程间的通信机制，原子命题用来形式化在某状态下的一些特性，直观地表示了关于系统状态的一些简单的已知事实。例如，对于给定的整型变量x，“x等于0”或“x小于200”都是原子命题。

定义3.1一个迁移系统TS是一个六元组在许多文献中，迁移系统采用Kripke三元组(S,R,L)表示，有关Kripke内容介绍见第6章。(S，T，→，I，AP，L)，其中： 

S={s0,s1,s2,…,sn,…}表示状态集； 

T={τ0,τ1,τ2,…}表示迁移动作集； 

→S×T×S表示迁移关系，如(s,τ,s′)∈→，也可用sτs′或ρτ(s,s′)表示； 

IS表示初始状态集； 

AP={a,b,c,…}表示原子命题集； 

L: S→2AP称为标签函数。

如果S、T和AP都是有穷集，那么称TS是有穷迁移系统。

一个迁移系统的直观行为描述如下： 系统始于一些初始状态s0∈I，通过迁移关系→发生状态转变。也就是说，如果s是当前状态，那么源于s的迁移sτs′被不确定地选择并且执行，即执行迁移动作τ，并且系统从状态s迁移到状态s′。这个选择过程会在状态s′重复并且终止于一个没有出迁移的状态(需要注意的是，I可以为空，在这种情形下，迁移系统由于没有初始状态可以选择，不产生任何行为)。更重要的是，当一个状态有多个出迁移时，下一个迁移的选择完全是不确定的，也就是这个选择过程的结果是不可以推理得到的，并且也无法知道某个迁移被选择的可能性有多大。类似地，当初始状态集由多个状态组成时，起始状态的选择也是不确定的。

标签函数L将原子命题的一个集合L(s)∈2AP与状态s联系起来。2AP是AP的幂集。L(s)={a|a∈AP且状态s完全满足a}，假设φ是一个命题逻辑公式，如果L(s)使公式φ为真，那么可以推导s满足公式φ，则可以表示为

sφiffL(s)φ

定义3.2一个迁移系统TS=(S，T，→，I，AP，L)，对于s∈S和τ∈T： 

(1) s的直接τ后继集合定义为Post(s，τ)={s′∈S|sτs′}，Post(s)=∪τ∈TPost(s,τ)，每个状态s′∈Post(s，τ)被称作s的一个直接τ后继。直接后继集合的概念由以下方式扩展为S的子集，对于CS，有Post(C，τ)=∪s∈CPost(s，τ)，Post(C)=∪s∈CPost(s)。

(2) s的τ前趋集合定义为Pre(s，τ)={s′∈S|s′τs}，Pre(s)=∪τ∈TPre(s,τ)。

Pre(C，τ) 和Pre(C)的概念以类似的方式定义： 

Pre(C，τ)=∪s∈CPre(s，τ)，Pre(C)=∪S∈CPre(s)

定义3.3对于迁移动作集T中的一个迁移动作τ 和状态集S中的一个状态s：

(1) 如果Post(s，τ)≠，则用enabled(τ)(简记En(τ))表示迁移τ在状态s是使能(能行)的，也就是说，s有一个直接τ后继。

(2) 如果Post(s，τ)=，则称迁移τ在状态s是非使能的(disenabled)，也就是说，s没有一个直接τ后继。

定义3.4对于一组迁移T1T和状态集S中的一个状态s： 

(1) 如果T1中有τ在s上是使能的，则称T1在s是使能的。

(2) 如果T1中所有τ在s上都是非使能的，则称T1在s是非使能的。

定义3.5(1) 如果对每个状态s∈S，都有Post(s，τ)={s}，则称τ为空迁移； 除了空迁移之外的迁移都叫作勤勉(diligent)迁移。

(2) 如果s上仅有的能行的迁移是空迁移τΙ，那么状态s是终止的。

一个迁移系统TS的终止状态是那些没有任何出迁移(即仅有空迁移)的状态，一旦由TS描述的系统到达了一个终止状态，整个系统将会停止。对于串行(顺序)程序而言，终止状态出现表示程序终止。

上面提到非确定性对于系统建模是非常重要的，但是迁移系统的“可见”行为是确定的，也常常是很有用的。一般有两种方法刻画一个迁移系统的可见行为： 一种依靠动作； 另一种依靠状态的标签。以动作为基础的方法从外部只看到执行的动作，以状态为基础的方法忽略了动作，并且要求约束当前状态的原子命题是可见的。从以动作为基础的方法的观点来看，迁移系统是确定的就要使每个状态都至多有一个标记动作τ 的出迁移，然而从状态标签的观点出发，确定性意味着对于任何状态标签A∈2AP和任何状态来说，至多有一个出迁移指向一个标签为A的状态。在这两种情况下，都要满足至多有一个初始状态。

定义3.6一个迁移系统TS=(S，T，→，I，AP，L)。

(1) 如果对于所有状态s和动作τ，|I|≤1和|Post(s，τ)|≤1，则称TS是动作确定的。

(2) 如果对于所有状态s和状态标签A∈2AP，|I|≤ 1和|Post(s)∩{s′∈S|L(s′)=A}|≤ 1，则称TS是AP确定的。

3.1.2迁移图

迁移图是L.Lamport于1983年提出的一种表示并发程序的图形化建模方法。与流程图类似，迁移图是一个带结点和有向边的有向图。不同的是，流程图用结点表示迁移，而迁移图是用有向边表示迁移的。



图31迁移图

设P1，P2，…，Pm(m≥1)是m个可并发执行的进程，每一进程Pi是带有标号(位置)结点的迁移图，勤勉迁移对应进程中出现的有标记的边。标号结点集Li={l0，l1，…，lt}，这里li是互不相交的，引入控制变量π1，π2，…，πm，其中πi表明进程Pi控制的当前位置。

设α是连接进程Pi中位置l到位置l′的一条边，
用指令c→［y-∶=e- ］标记(见图31)，这里y-=(y1，y2，…，yn)是各进程共享的程序变量，每个进程都可以引用或修改这些变量。则与α关联的迁移τ 定义为(πi=l)∧c∧(π′i=l′)∧(y-=e-)。如果在状态s下，Pi当前的位置是l，并且布尔表达式c为真，那么称迁移 τ 在状态s是使能的。如果对于一些属于进程Pi的边α来说，和α相关的迁移在状态s是使能的，则称进程Pi在状态s是使能的，否则称进程Pi在状态s是非使能的。



图32一个简单的饮料自动售货机的

迁移图

例3.1图32的迁移图是对一个简单的饮料自动售货机的建模，自动售货机可以卖啤酒或苏打水。状态用圆角矩形表示，迁移用带标记的边表示，状态的名称写在圆角矩形里面，初始状态用一个没有来源的进入箭头表示。

状态集S={pay，select，soda，beer}，初始状态集仅有一个状态，即I={pay}，对于饮料机的一些内部动作，用动作τ 表示。 动作集T={insert_coin，get_soda，get_beer，τ}，如pay insert_coin select和beer get_beer pay就是一些迁移的例子。

需要注意的是，投了一个硬币后，自动售货机不能确定提供啤酒还是苏打水。

迁移系统中的原子命题以待考虑的属性而定，有一个简单的办法是让状态名作为原子命题，也就是对于任何状态s，L(s)={s}。然而，如果仅有的相关属性指的不是选择的饮料，如属性“在投了一个硬币后，自动售货机只递送一种饮料”，那么它就可以使用两个元素的命题集合AP={paid，drink}，伴随标签函数： 

L(pay)=，L(soda)=L(beer)={paid，drink}，L(select)={paid}

这里原子命题paid表示那些使用者已经付费，但还没有获得饮料。

前面的例子说明了有关原子命题和动作名称选择的任意性，即使一个迁移系统的形式化定义需要确定动作集T和命题集合AP，T和AP也可以在之后进行临时的处理。在许多情况下，动作名称是不相关的，例如，由于迁移代表一个内部流程活动，使用了一个特殊的标记τ 或者在动作名称不相关的情况下，甚至可以省略动作标记。在描述迁移系统时，原子命题集合AP的选择通常是不确定的，如可以假定APS和标签函数L(s)={s}∩AP。

使用迁移系统对软硬件系统建模时，需要注意非确定性的问题，这里采用的非确定性选择是通过交错对独立活动并行的建模和对产生冲突情况的建模。例如，如果两个进程都要获取一个共享资源，那么本质上交错指的是控制并行进程的动作指令的非确定选择。除了并行性，非确定性对于抽象目标、规约不足、未知或不可预测环境接口的建模也是很重要的。饮料自动售货机(见图32)是后面这种情况的例子，其中使用者需要做一个非确定的选择，也就是在select状态的两个τ迁移中选一个来获得两种饮料中的一种。“规约不足”指的是在早期设计阶段给系统提供的一个粗糙模型中，通过非确定性表示几种可能行为的选择。这个想法是由于在后面更细化的步骤中，设计者会实现非确定选择中的一个，而舍弃其他的选择。从这个意义上说，迁移系统中的非确定性可以代表实现上的自由性。

3.1.3计算

一个迁移系统的计算(也称执行或运行)来自系统非确定性的选择，表示迁移系统的一个可能的行为。

定义3.7一个迁移系统TS=(S，T，→，I，AP，L)。

(1) TS的一个有限计算片断σ是一个以状态为结尾的状态与动作交错的序列： 

σ=s0τ1s1τ2…τnsn，对所有0≤i<n，siτi+1si+1

其中n≥0，把n作为计算片断σ的长度。

(2) TS的一个无限计算片断ρ是一个无限的状态与动作的交错序列： 

ρ=s0τ1s1τ2s2τ3…，对所有i≥0，siτi+1si+1

需要注意的是，序列s (∈S)是一个长度n=0的有限计算片断。一个无限计算片断的每个奇数长度的前缀都是一个有限的计算片断。计算片断σ=s0τ1…τnsn和ρ=s0τ1s1τ2…分别被写成

σ=s0τ1…τnsn和ρ=s0τ1s1τ2…

当一个计算片断不能再延长了，就称它是最大化的。

定义3.8一个最大化的计算片断要么是一个以某终止状态结尾的有限计算片断，要么是一个无限计算片断。如果一个计算片断始于某初始状态(也就是s0∈I)，则称它是初始化的。

例3.2例3.1中描述的饮料自动售货机的计算片断的例子如下，为了简单起见，动作名称被简写，例如sget是get_soda的简写，coin表示insert_coin。

ρ1=paycoinselectτsodasgetpaycoinselectτsodasget…
ρ2=selectτsodasgetpaycoinselectτbeerbget…
σ=paycoinselectτsodasgetpaycoinselectτsoda

计算片断ρ1和σ是初始化的，而ρ2不是初始化的。σ不是最大化的，因为它没有以一个终止状态结尾，假设ρ1和ρ2都是无限的，则它们是最大化的。

定义3.9迁移系统的一个计算是一个初始化的最大化的计算片断。

在例3.2中，ρ1是一个计算，而ρ2和σ不是，因为ρ2是最大化的却不是初始化的，σ是初始化的却不是最大化的。

定义3.10一个迁移系统TS=(S，T，→，I，AP，L)，如果存在一个初始化的有限的计算片断： 

s0τ1 s1τ2 …τn sn=s

则称状态s∈S是可到达的，Reach(TS)表示TS中所有可达状态的集合。

3.2应 用 举 例

本节通过对时序电路、数据依赖系统(一种简单的串行程序)和并发系统的建模来阐述迁移系统的应用。在这些例子中，状态代表可能的存储设置(即相关“变量”的值)，状态改变(即迁移)代表“变量”的改变。这里的变量需要从广义理解，对计算机程序来说，一个变量可以是一个控制变量(如一个程序计数器)，也可以是一个程序变量，而对电路来说，一个变量代表一个寄存器或一个输入位。

3.2.1时序电路

考虑一个用迁移系统对时序电路建模的简单例子。

例3.3在图33的时序电路的电路图中，输入变量是x，输出变量是y，寄存器是r，输出变量y的控制函数通过表达式λy=(xr)给出，其中代表异或(XOR)，寄存器值的改变是通过电路函数δr=x∨r实现的。



图33一个简单时序电路的迁移图



需要注意的是，一旦寄存器的值是［r=1］，r就会保持这个值不变，在寄存器初始值是［r=0］的情况下，电路的行为可以通过状态空间为S=Eval(x，r)的迁移系统TS进行建模，其中Eval(x，r)代表输入变量x和寄存器变量r的值的集合，TS的初始状态是I={<x=0，r=0>，<x=1，r=0>}。注意，这里有两个初始状态，是因为没有假定输入位x的初始值。

动作集合在这里不相关，可省略，迁移直接来自函数λy和δr。例如，如果下一个输入位等于0，则迁移为<x=0，r=1>→<x=0，r=1>； 如果下一个输入位等于1，则迁移为<x=0，r=1>→<x=1，r=1>。

下面考虑标签L，使用的原子命题集合AP={x，y，r}，那么状态<x=0，r=1>可以被标记为{r}，它没有标签y是因为电路函数 (xr)在该状态的值是0。对于状态<x=1，r=1>，由于λy的值是1，则标签L(<x=1，r=1>)={x，y，r}，于是可以得到： L(<x=0，r=0>)={y}，L(<x=1，r=0>)={x}，该迁移系统的标签在图33(b)中已经表示出来。

还可以使用命题AP′={x，y}，寄存器的值假定是不可见的，那么可以得到:

L′(<x=0，r=0>)={y}L′(<x=0，r=1>)=
L′(<x=1，r=0>)={x}L′(<x=1，r=1>)={x，y}

AP′的命题足以被形式化，如属性“输出位y经常被设成无限的”，但是和寄存器r相关的属性是不可表达的。

在这个例子中使用的方法可以推广到任意的时序电路，这个电路有n个输入位x1，x2，…，xn，m个输出位y1，y2，…，ym和k个寄存器r1，r2，…，rk。迁移系统的状态代表这n+k个输入位和寄存器x1，x2，…，xn，r1，r2，…，rk的值，输出位的值通过输入位和寄存器的值得到，也可以从状态中得到。假定输入位的值(通过电路环境)是非确定得到的，另外，设寄存器的初始值是［r1=c0,1，…，rk=c0,k ］，其中c0,i表示寄存器i的初始值，0<i≤k。对该时序电路建模的迁移系统TS=(S，T，→，I，AP，L)由以下组成部分，状态空间S=Eval(x1，x2，…，xn，r1，r2，…，rk)，这里的Eval(x1，x2，…，xn，r1，r2,…，rk)代表输入变量xi和寄存器ri的值的集合，并且等同于集合{0，1}n+k(一个s∈Eval(·)的值将值s(xi)∈{0，1}映射到输入位xi上，类似地，每个寄存器rj是s(rj)∈{0，1}的映射。为了简化这个问题，假设每个s∈S是一个n+k位的元组，当且仅当xi的值为1时，第i位才会被设置，因此第n+j位表示rj的值)。初始状态的形式是(…，c0,1，…，c0,k)，其中k个寄存器的值已经给出，前面的n位表示输入位的值，这些值是任意的，因此初始状态集是

I={(a1，a2，…，an，c0,1，c0,2，…，c0,k)|a1，a2，…，an∈{0，1}}

动作集合T是不相关的，用T={τ}表示，为了简洁起见，原子命题集合设为

AP={x1，x2，…，xn，y1，y2，…，ym，r1，r2，…，rk }

(实际上它可以定义为该AP的任意子集)因此任意寄存器、输入位和输出位都可以作为一个原子命题，标签函数设定为任意状态s∈Eval(x1，x2，…，xn，r1，r2，…，rk)，这正好是在状态s下xi，rj赋值为1的原子命题。如果对于状态s，输出位yi的值为1，那么原子命题yi也是L(s)的一部分。因此，有

L(a1，a2，…，an，c1，c2，…，ck)={xi|ai=1} ∪ {rj|cj=1}
∪ {yi|sλyi(a1，a2，…，an，c1，c2，…，ck)=1}

其中λyi： S→{0，1}是一个跳转函数，对应于由门电路得到的输出位yi。

迁移用来表示行为，用δrj表示电路图中寄存器rj的迁移函数，当且仅当c′j=δrj(a1，a2，…，an，c1，c2，…，ck)时，有

(a1，a2，…，an，c1，c2，…，ck)τ(a′1，a′2，…，a′n，c′1，c′2，…，c′k)

这里假设输入位值的改变是不确定的，因此没有在a′1，a′2，…，a′n上加约束。

读者可以使用这种方法自行检验图33(a)的电路，该电路确实可以使用图33(b)的迁移系统表示。

3.2.2数据依赖系统

一个数据依赖系统的可执行动作一般来自分支条件，例如： 

ifx % 2=1 then x∶=x+1 else x∶=2·xfi

当用一个迁移系统对该程序片断进行建模时，迁移的条件可以省略并且条件分支可以通过非确定性代替，但这将导致该迁移系统只能验证较少的属性。此外还可以使用条件迁移，并将(标有条件的)结果图应用到随后要被验证的迁移系统中，以下通过示例详细介绍这个方法。

例3.4考虑例3.1中描述的饮料自动售货机的一个扩展，该机器可以计算苏打水和啤酒瓶子的数量，当自动售货机为空时，将返回投入的硬币。为了简便起见，自动售货机由两个位置start和select表示，下面两个条件迁移是对投了一个硬币和重新加满售货机的建模： 

starttrue:coinselectstarttrue:refillstart

条件迁移的标记形式是g： τ，其中g是一个布尔表达式(叫作卫式)，τ 是一个g成立才可能发生的动作。由于上面两个条件迁移的条件总是成立的，那么动作coin在开始位置也总是可行的，为了简洁起见，假定重新填充后，两种饮料都会装满。下面两个条件迁移是对如果饮料售货机中还有苏打水(或啤酒)，那么就能获得苏打水(或啤酒)的建模： 

selectnsoda>0:sgetstartselectnbeer>0:bgetstart

变量nsoda和nbeer分别记录了机器中苏打水和啤酒的数量。下面这个迁移表示当机器里没有任何瓶子，返还投的硬币时，自动售货机会自动转到初始start位置： 

selectnsoda=0∧nbeer=0:ret_coinstart

设两个饮料储藏室的最大容量是max，投硬币(通过动作coin)不会使饮料的数量发生改变，同样返还硬币(通过动作ret_coin)也不会使饮料的数量发生改变，其他动作的效果如下： 

refill  nsoda∶=max； nbeer∶=max
sgetnsoda∶=nsoda-1
bgetnbeer∶=nbeer-1

由位置作为结点和条件迁移作为边组成的图不是一个迁移系统，因为边当中加了条件，不过迁移系统可以由这张图演变得到。例如，图34描绘的是max等于2的扩展迁移系统，迁移系统的状态与其所处图中的位置和自动售货机中苏打水和啤酒的数量(在图中分别用白点和黑点表示)都有关系。



图34对扩展的饮料自动售货机建模的迁移系统


前面这个例子可以通过程序图(program graph)在一个类型变量集合Var上形式化，在这个例子中的变量就如nsoda和nbeer。实际上，这意味着一个标准化的类型(如boolean、integer或char)和每个变量都有关系，变量x的类型叫作x的论域dom(x)。设Eval(Var)表示变量赋值后变量集合的值，Cond(Var)是Var上的布尔条件集合，也就是命题符号形如x-∈的命题逻辑公式，其中x-=(x1，x2，…，xn)是一个由一组在Var中不同变量组成的元组，是dom(x1) ×dom(x2) ×… ×dom(xn)的一个子集。例如，下面的命题是一个关于变量x，x′和变量y的布尔条件： 

(-3 < x-x′ ≤ 5) ∧ (x ≤ 2·x′) ∧ (y=green)

其中x和x′是整型变量，dom(y)可以是{red，green}。

不限制论域，dom(x)可以是一个任意的集合，元素个数也可能是无限的，然而在实际的计算机系统中，所有的论域都是有限的(例如，integer类型只包含整数n的一个有限的定义域，即-216< n < 216)。而一个程序的逻辑和算法结构常常是建立在无限论域的基础上的，在论域上设置限制对于实现是很有用的，例如需要多少位表示整型变量会在后面的设计阶段考虑，但是这里先忽略。

一个类型变量集合上的程序图是一个边上标有变量和动作条件的有向图，动作的影响通过映射Effect表示： T×Eval(Val)→Eval(Val)。

映射Effect说明了在执行一个动作后，这些变量的值η会发生什么样的改变。例如，如果τ 表示动作x∶=y+5，其中x和y都是整型变量，η的值是η(x)=17和η(y)=-2，那么,有

Effect(τ，η)(x)=η(y)+5=-2+5=3，Effect(τ，η)(y)=η(y)=-2

因此Effect(τ，η)将3赋给x，将-2赋给y。程序图中的结点叫作位置(location)，并且由于它们指定了哪些条件迁移是可行的而有了一种控制的功能。

定义3.11类型变量集合Var上的一个程序图是一个六元组PG=(Loc，T，Effect，，Loc0，g0)，其中： 

Loc是位置集； 

T是动作集； 

Effect： T×Eval(Val)→Eval(Val)是效应函数； 

Loc×Cond(Var)×T×Loc是条件迁移关系； 

Loc0Loc是初始位置集； 

g0∈Cond(Var)是初始条件。

标记lg:τl′是(l，g，τ，l′)∈的简洁写法，条件g也叫作条件迁移lg:τl′的卫式，如果卫式是一个重言式(如g=true或g=(x<1)∨(x≥1))，那么可以简写成lτl′。

在位置l∈Loc上的行为依赖当前变量的值η，在值η上满足条件g(即ηg)的所有迁移lg:τ l′之间会存在一个非确定的选择。根据Effect(τ，·)，动作τ的执行可以改变变量的值，接着系统迁移到位置l′，如果没有可用的迁移，系统就会停止。

例3.5例3.4中的图是一个程序图，变量集是Var={nsoda，nbeer}，其中变量的定义域是{0，1，…，max}，位置集是Loc={start，select}，Loc0={start}，并且T={bget，sget，coin，ret_coin，refill}，动作的效应可以表述为

Effect(coin，η)=η
Effect(ret_coin，η)=η
Effect(sget，η)=η［nsoda∶=nsoda-1］
Effect(bget，η)=η［nbeer∶=nbeer-1］
Effect(refill，η)=［nsoda∶=max，nbeer∶=max］

这里，η［nsoda∶=nsoda - 1］是对η′(nsoda)=η(nsoda) - 1，η′(x)=η(x)中η′求值的简写，初始条件g0=(nsoda=max∧nbeer=max)说明开始时两种饮料都已装满。

每个程序图都可以转变为一个迁移系统，迁移系统的状态可以由一个控制部分(即程序图中的一个位置l)和变量的值组成，因此状态可以用<l，η>表示，初始状态是满足初始条件g0的初始位置。为了描述一个程序图描述的系统的属性，命题的AP集合由位置集l∈Loc(能够说明系统当前所在的控制位置)和变量的布尔表达式组成。例如： 

(x≤5) ∧ (y是偶数) ∧ (l∈{1，2})

该命题是用整型变量x、y和自然数位置描述的。状态标签形如<l，v>，是由l和在Var上满足η的所有条件组成的。迁移关系表示为，无论什么时候在程序图中有一个条件迁移lg:τl′，并且卫式g使η值不变，那么都有一个迁移从状态<l，η>到状态<l′，Effect(τ，η)>，以上形式化表述为

定义3.12程序图PG=(Loc，T，Effect，，Loc0，g0)中变量的Var集上的迁移系统是一个六元组TS=(S，T，→，I，AP，L)，其中： 


S=Loc×Eval(Var)； 

→S×T×S定义为lg:τl′∧ηg<l,η>τ<l′,Effect(τ,η)>； 

I={<l，η>|l∈Loc0，ηg0}； 

AP=Loc∪Cond(Var)； 

L(<l，η>)={l}∪{g∈Cond(Var)|ηg}。


TS(PG)的定义给出了一个很大的命题集合AP，一般地，在描述系统属性时，只需要AP中的一小部分。

3.2.3并发和交错

前面介绍了迁移系统的定义，并且阐述了如何通过迁移系统对时序电路和数据依赖系统进行有效的建模。实际上，大多数的软硬件系统不是串行的，而是并行的。当有多个迁移系统TS1，TS2，…，TSn且它们的进程行为是并行的，可以用以下方式表示： 

TS=TS1‖TS2‖…‖TSn

这里的‖是连接的符号，本节通过例子的方式介绍‖的几个变式。注意，上面的组合会在TSi中进行重用，即TSi是由几个迁移系统组成的迁移系统： 

TSi=TSi,1‖TSi,2 ‖…‖TSi,n

通过分级的方式使用并行组合，复杂的系统可以用一种结构化的方式描述。

采用交错执行方式作为并发系统建模的基本想法最初由E.W.Dijkstra于1965年提出。并发系统由多个单独部分组成，整个系统的状态是由多个单独部分的状态构成的。系统的动作同样也会由多个单独部分的动作交织构成。因此交错可以用来表示并发，也就是在同时运行的进程之间的非确定性选择。这个观点是建立在只有一个处理器是可用的基础上的，进程的动作在其中都是相互关联的。“单处理器的观点”只是一个建模概念，也可以用在运行在不同处理器上的进程。因此不需要假设不同进程间的执行顺序，例如，如果有两个完全互不依靠的无终止的进程P和Q，那么下面的顺序都是可能的： 

P Q P Q P Q Q Q P…
P P Q P P Q P P Q…
P Q P P Q P P P Q…

其中P和Q的动作可以是关联的。

例3.6一个非交叉(平行)路的两个交通灯的迁移系统，假定两个交通灯的跳转是彼此之间完全独立的。例如，交通灯由过路的行人控制，每个交通灯用一个两个状态的简单迁移系统来建模，一个状态表示红灯，另一个状态表示绿灯。两个灯的并行组合如图35所示，其中‖‖表示交错符号。原则上，交通灯之间的任何连接形式都是可行的。例如，在初始状态两个交通灯都是红色，那么在哪个灯变绿之中就需要做一个非确定性选择。注意，非确定性是可以描述出来的，只是这里没有对交通灯之间的调度问题进行建模。



图35交通灯的迁移系统


系统中交错的重要依据是当并发运行的独立动作α和β以任意顺序成功执行时，都会产生同一个结果，这种情况可以形式化表示为

Effect(α‖‖β，η)=Effect((α； β)+(β； α)，η)

其中分号(； )代表顺序执行； +代表非确定性选择； ‖‖代表独立活动的并发执行。可以用两个独立的赋值简单地理解上述内容： 

x∶=x+1=α‖‖y∶=y-2=β

当初始值x=0，y=7时，无论α和β的赋值是并发执行(即同时)还是以一个任意的顺序执行的，之后x的值是1，y的值是5。可以用如图36所示的迁移系统表示： 



图36具有独立动作的交错


注意，动作之间的无关性很重要。如果动作之间是相关的，那么动作的顺序就很重要。例如并行程序x∶=x+1‖‖x∶=2·x(初始值是x=0)，那么变量x的最终值就与x∶=x+1和x∶=2·x的执行顺序有关。

下面给出迁移系统交错的形式化定义。迁移系统TS1‖‖TS2代表一个由TS1和TS2描述的交错动作的并行系统。该描述假定没有通信和共享变量，TS1‖‖TS2的(全局)状态是由TSi的局部状态组成的状态对<s1，s2>，全局状态<s1，s2>的出迁移也是由s1和s2的出迁移组成的。因此，无论什么时候系统处于状态<s1，s2>时，都要在s1和s2的所有出迁移中做一个非确定性选择。

定义3.13设TSi=(Si，Ti，→i，Ii，APi，Li)是两个迁移系统(i=1，2)，则迁移系统TS1‖‖TS2定义为

TS1‖‖TS2=(S1×S2，T1∪ T2，→，I1×I2，AP1∪ AP2，L)

其中迁移关系→定义如下： 

s1τ1s′1<s1,s2>τ<s′1,s2>s2τ2s′2<s1,s2>τ<s1,s′2>

标签函数定义为L(<s1，s2>)=L(s1) ∪ L(s2)。

交错符‖‖可以用来对异步并发建模，异步并发就是子进程间是完全独立的，即没有任何信息的传递和共享变量。但是迁移系统的交错符对于大多数并发或通信的并行系统来说过于简化。下面通过涉及共享变量的例子说明这一点。

例3.7考虑下面并行程序的程序图，如图37所示。

x∶=2·xactionα‖‖x∶=x+1actionβ

其中，设定初始值x=3。(为了简化图形，位置可省略)迁移图TS(PG1)‖‖TS(PG2)包含的不一致状态<x=6，x=4>并不能反映α和β并行的行为，有



图37具有共享变量的交错


这个例子中的问题在于动作α和β使用共享变量x，但是迁移系统的交错符没有考虑潜在的冲突，就直接构造了这些单独状态空间上的笛卡儿积。因此局部状态x=6和x=4不能描述互斥事件。

定义3.14设PGi=(Loci，Ti，Effecti，i，Loc0,i，g0,i)，i=1，2，是在变量Vari上的两个程序图，则在Var1 ∪ Var2程序图PG1‖‖PG2定义为

PG1‖‖PG2=(Loc1×Loc2，T1+∪T2，Effect，，Loc0,1×Loc0,2，g0,1∧ g0,2)

其中定义如下： 

l1g:τ1l′1<l1,l2>g:τ<l′1,l2>l2g:τ2l′2<l1,l2>g:τ<l1,l′2>

如果τ∈Ti，Effect(τ，η)=Effecti(τ，η)。

程序图PG1和PG2有同样的变量Var1∩Var2，这些变量称为共享变量(也叫全局变量)，在Var1/Var2中的变量是PG1的局部变量，同样地，在Var2/Var1中的变量是PG2的局部变量。

例3.8程序图PG1和PG2对应的赋值分别是x∶=x+1和x∶=2·x，程序图PG1‖‖PG2和它转化后的迁移系统TS(PG1‖‖PG2)如图38所示，其中假定x的初始值等于3。注意，在迁移系统初始状态中的非确定性不表示并发，这正好是解决x∶=x+1和x∶=2·x都可以修改共享变量x的一种方式。



图38程序图的交错


局部变量和共享变量之间的区别对程序图PG1‖‖PG2的动作也有影响，获取共享变量的动作被认为是“临界的”，其他的动作被认为是非临界的。临界的动作和非临界的动作之间的区别可以在表示迁移系统TS(PG1‖‖PG2)的非确定性时清楚地看到。迁移系统一个状态的非确定性可以表示为： 

(1) 程序图PG1或PG2中的一个内部非确定性选择。

(2) PG1和PG2的非临界动作的交错。

(3) PG1和PG2的临界动作之间选择的解决方式(并发)。

特别地，PG1的非临界动作可以和PG2的临界性和非临界动作并行，因为它只影响PG1的局部动作，对于PG2的非临界动作同样适用。但是PG1和PG2的临界动作不能同时执行，因为共享变量的值依赖动作的执行顺序。所以需要通过一个合适的调度策略描述PG1和PG2的临界动作的并发情况。

例3.9用迁移系统描述一个多用户终端执行程序MUTEX(MULtiuser Terminal Executive)： 

MUTEX: flag： array［0..n-1］of 0..4 where flag∶=0； 
P［0］‖P［1］‖…‖P［n-1］

其中每一进程Pi为

l0:loop forever do

begin

l1: Non Critical

l2: flag［i］∶=1

l3: wait until  j:0≤j<n： (flag［j］<3)

l4: flag［i］∶=3

l5: if  j:0≤j<n： (flag［j］=1) then

begin

l6: flag［i］∶=2

l7: wait until  j: 0≤j<n (flag［j］=4)

end

l8: flag［i］∶=4

l9: wait untilj: 0≤j<i： (flag［j］ <2)

l10: Critical

l11: wait until j:i<j<n： (flag［j］<2∨flag［j］>3)

l12: flag［i］∶=0

end
(1) 原子命题集AP={l0，…，l12，flag［0］，…，flag［n-1］}，其中l0，…，l12∈{0，…，n-1}是控制变量，变量flag［0］，…，flag［n-1］表示对应的程序变量的当前值。

(2) 状态集S包含原子命题集AP在定义域上所有可能的赋值。

(3) 初始状态集I： (l0∈{0，…，n-1})∧(l1..12=)∧(flag［i］=0)，即在程序的初始状态，所在进程驻留在l0位置，且flag(0)，…，flag(n-1)均为0。

(4) 迁移关系： 算法所在测试(如其中之一在语句l1中)当作原子处理，即通过单一迁移完成每一次执行，相应地给出每一进程P［i］及每一位置lk的一个迁移τk［i］和对应的迁移关系ρk［i］。例如： 

状态l1的迁移关系为ρ1［i］: (i∈l1)∧(stay∨move(i，1，2))，根据上述公式，进程P［i］可以不确定地选择在l1处停留或者从l1移至l2。

状态l5的迁移关系为ρ5［i］: (i∈l5)∧［(F1≠)∧move(i，5，6)］∨［(F1=)∧move(i，5，8)］，当在l5时，如果一些进程P［j］具有flag［j］=1和F1≠，P［i］可以处理l6； 如果没有进程flag值等于1和F1=，也可以处理l8。

其余状态对应的迁移关系可类似给出。

(5) 迁移动作集T： 略。

(6) 标签函数L： 略。

3.3本 章 小 结

迁移系统是一种基于状态迁移的基本计算模型，通过系统(程序)的状态集合及对应状态间的迁移(也称操作)集合描述系统的计算行为，可以从不同角度对并发系统进行建模。迁移系统本质上是一种交错并发模型，即系统进程间的并发执行并不是真并发，而是通过各个原子迁移以不确定的顺序交错执行来表示的，其计算行为表现为状态与动作交错的序列。

基于迁移系统，人们提出多种并发模型，如进程代数CSP模型、CCS模型等； 通过对基本迁移系统进行扩展，如将公平性引入迁移系统，可得到公平迁移系统； 将时间(或时钟)引入迁移系统，可分别得到时间(时钟)迁移系统等。

习题3

1. 给出如图39和图310所示的时序电路的迁移系统。



 图39题1图（1）图310题1图（2）


2. 给出容量为3的栈的迁移系统(使用top、pop、push操作)。

3. 给定三个进程P1、P2和P3，共享一个整型变量x，进程Pi(i=1,2,3)的程序如下： 

for ki=1，…，10 do

LOAD(x)； 

INC(x)； 

STORE(x)； 

od
Pi执行10次x∶=x+1，x∶=x+1通过LOAD(x)、INC(x)和 STORE(x)这三个动作实现，如果这三个进程是并行的，且以x∶=0开始，那么整个过程是否有一个执行以x=2结束？