Video在线视频

那么还有没有其它的方法呢

我们定义了系统的性质

我们就要来研究

怎么分析它的性质对不对

那么通用的分析方法呢有这么几种

一个我们要想计算这个可达标识集

我们可以用构造树的方法来计算

另外刚才我讲过求解不变量式

还有一个就是化简的方法

这个网系统里面的元素太多

我给它化简了

再一个方法

就是提高这个网系统的层次

我说过petri网的特点就是这个太细了

局部确定每一个变迁都有确定的外延

所以它没有灵活性

因此呢就需要很多个变迁来表示

不像这个程序里面

有一个布尔表达式

a或者b就怎么着

那我们用petri网的表示呢就得说

a成真怎么着b成真怎么着

a和b都成真怎么着

所以这个元素就有很多了

那么我们为了减少这个元素的个数

又不改变程序的系统的性质

那么我们可以提高网系统的层次

这样呢分析它

提高层次的结果就是节点减少了

分析起来就简单了

先说这个可达树

就是用构造树的方法

来研究这个系统的性质

好 我们看这一个简单的系统

就这么一个网系统

Petri说过一句话

说元素个数不超过16

就是16以下的这么多个

我们才有可能用手用人工来分析

叫做hand simulation

用手来模拟

所以一旦网元素的个数太大了

我们就没法用手了

而我们这个课上

是必须用手来做分析的

这个是一个杜撰出来的例子

为了体现网系统可能的性质

所以它有一个初始标识呢

是用一个向量来表示

用一个这个s向量来表示

就是s1里面有一个token

s2里面没有

s3里面也没有

这就是标识的这个s向量表示

用向量来表示

好 我们看这个简单的petri网

那么这是一个杜撰的

没有物理背景的一个图

只是为了揭示

在我们构造这个可达树的时候

会遇到的这个什么情况

可达树呢从根构造起

这个根是什么呢

根就是它的初始标识

（1，0，0）这就是它的根

在这个根底下我们找一找看

这个系统里面在这个标识底下

都有那些变迁能够发生呢

所有能够发生的变迁

都分出一个分支来

比如说在这个状态底下

a可以发生b也可以发生对不对

a发生呢

你看啊我们这儿都没有写

这个容量是多少权是多少

那就是容量是无穷

权是1

容量为什么可以无穷的

我们讲了我们可以用技术的方法

s补的方法把它改造成无穷

所以我们不妨假定

它就是无穷的

那么a发生了以后

它的那个后继是什么呢

后继就是它（0，1，0）

你看这个s2里面得到一个token

s1里面的token失去了

在这个标识底下

什么也不能够发生了

那么在初始标识底下

另外一个能够发生的变迁那就是b

b发生以后

它的后继是什么呢

b因为是个闭环

它里面的token不消失

就像我说的工具或者是催化剂一样

它不会消失

所以这个s1里面的token仍然还在

这个不受影响

所以它里面还是零

s3里面得到了一个token

这就是（1，0，1）

在初始标识底下

有两个可以发生的有发生权的变迁

每一个能有发生权的变迁

都作为一个分支

加在这个根上面

然后每个分支的这个节点

都是它的后继标识

这就是这一层

然后我们看

我们现在有了两个叶节点对吧

一个呢是（1，0，1）

一个是（0，1，0）

先看看（1，0，1）

（1，0，1）这个标识

b2 s1里面还有一个token

因此呢这个a或b还是有发生权

分别加上两个分支

一个是a一个是b

就变成这一层

那么在这个（0，1，0）

这个节点下面呢

没有能够发生的变迁

你看这里有一个token

a和b都不能发生了

所以呢（0，1，0）这个节点呢

就是一个死节点了

它再也不可能改变这个状态了

下面我们可以继续

这个（0，1，1）

仍然是没有任何的变迁可以发生

因为这个a或b都需要s1里面的token

s1现在失去了token

a或b都不能够发生了

所以这个这个都是死的

这个叶节点

但是这一支呢

这个b可以发出任意多次

因为它是不消耗的

这个s1里面的token是不消耗的

所以b呢可以反复的发生反复发生

发生的没有终点

所以这个如果我们要构造

这个可达树的话

我们是构造不完的

它有多少个可以到达的标识呢

无穷多个

因为这个s3里面可以收到任意多个

你想要几个有几个那么多的token

因为只要b发生那么多次就行了

所以如果我们想要把所有可能

到达的标识都算出来

那我们就算不完了对不对

算不完我们得想办法

它这里是不是有规律

我们想办法用数学的方法

把它这个规律给体现出来

那么我们就可以用有限的一个数

来表现这个无限长的这个树结构了

这一支是无限长的

怎么办呢

就是这里说的剪枝

这个无限长的分支

我们要用数学的方法

给它处理成有限的

而这个有限的要能够反映出

这个无穷长的这个规律

这就是需要一个概念

叫做覆盖的概念

一个标识覆盖另外一个标识

M1被M2覆盖

M2覆盖M1什么意思啊

就是所有的s元素

也就是说所有的库所里面

s2的token都不比M_1少

M_2这个标识底下

任何一个s元素里面的token数

都不少于M_1那个状态下

这个s元素里面的token数

这就叫做覆盖

那么如果M_2覆盖M_1

而且其中有一个库所

它的token数确确实实比M_1的时候多

刚才我们讲的覆盖

是指要求大于等于

而现在我们要求它是一定要大于

所有那地方都大于等于

至少有一个地方是大于

那么这个时候呢

就是严格的覆盖了

我们就用大于符号

而不用大约等于符号来描述

所以叫做M_2呢覆盖了M_1

而且在这个地方比它大

有了这个概念以后

我们就可以来进行剪枝了

好 我们看

有了a有了b以后到这一层

再下一层

这个是变成什么了

（1，0，2）吧

（1，0，2）是不是覆盖了

这个（1，0，1）呀 对吧

你有一个我有一个

你有零个我也有零个

你有一个我有两个是不是

所以这个呢不仅覆盖它

而且在这个第三个元素呢是比它大的

所以你如果发现了这种情况

那么就把大的那个地方

这里就是第三个元素

把它改成ω

然后这个ω有什么特点呢

ω就是相当于一个无穷

ω+1还等于ω

ω-1也等于ω

ω+ω还是ω

那么我们就继续往下做

这是（1，0，ω）

然后b再发生

你再加进去一个ω+1还是ω

所以就变成（1，0，ω）了 对吧

那么这个分支也是（0，1，ω）

你这a再发生

这里只是在中间加了一个1

也就是s2里面得到了一个token

这样一来我们看

这个（1，0，ω）

（1，0，ω）是不是两个一样啊

这两个完全一样了

完全一样了以后

我们就没有必要再重复下去了

因为我从这个节点

到下面一个节点跟我一样

所以呢就到此为止

所以我们就可以

剪枝就剪到这儿了

就是我已经发现两个一样的了

这两个一样的不见得非要连着

也可能过了几个以后才两个一样

那么这个时候

我们就可以停滞在这

把这个无限长的枝子呢

剪成有限长的了

我们看它的结果是什么

这就是我们最后得到覆盖树

因为它已经不是可达树了

而是覆盖树了

我是用覆盖这个概念得到的这棵树

那么我把刚才那些小的东西呢

都移到边上去了

得到的就是这样一棵树

从这儿出发到了这儿

然后通过这个引进ω

然后这两个完全一样

那么就到此为止

这就是可达树算法

可达树算法呢你必须要证明

就是这个算法好不好 好

是不是所有的系统

你都能够用这种方法来剪枝呢

是不是每一个无穷长的序列

都能够出现覆盖和严格覆盖的情况

让你能够引进ω呢

那么这就是需要数学证明的

这个数学证明啊说起来不难

但是真正写下来还是挺复杂的

这里面用到这个数学归纳法等等

比方说我们这里是有三个数对吧

每一个标识都是三个数

那么你要想证明

任何一个无穷序列

无穷长的向量序列

一定存在一个子序列

其中后面一个比前面一个大

后面一个比前面一个大

那么要想证明这个

你就要用数学归纳法

你想证明三个

那你先证明一个

说如果我只有一个数

有个无穷长的数

它一定能够找到一个子序列

是一个比一个大

既然一个比一个大

我就把第一次出现大的地方换成ω

换成ω以后底下就一样了对吧

那么然后假定

（n-1）个对那么你把它推广了n个

这个呢我的书里有

我为什么要说写下来不容易呢

因为在一本外国书上出现了它的证明

这是上个世纪80年代

那个证明就是不正确的

这就我们的结论

你有了覆盖树以后

就这个所有可以到达的标识

都被覆盖树上面的节点所覆盖

就是你虽然有无穷多个可达标识

但是我这棵有限的数

就把你全部覆盖了

从我们这个例子来讲

它的标识有什么规律呢

就是这么

（1，0，0）（1，0，1）

（1，0，2）（1，0，3）

或者是（0，1，0）（0，1，1）

（0，1，2）（0，1，3）

那么我们这个呢都用ω来表示

所以一共就有两种

这是一个另外

（0，1，ω）（1，0，ω）

一共就这么几种

所以全部被覆盖了

所以我们这个可达标识呢

虽然是个无穷集合

但是我们用一个有限的树呢

就把它给算是算出来了吧

因为如果你的权是1的话这个是准确的

如果你的权是2或者是3呢

那你这个覆盖就多了

因为权是3的话

那个2它是到不了的

但是你一盖把它盖住了是不是

所以不完全相等

除非你的权是1

这是没有办法的办法

这是我们总之

找到了一个有限的东西

来代表那个无限的东西

然后呢我们可以

把它的性质保留下来

这个可达树呢有一个缺点

你看我们这可达树呢有几个节点了

有3个节点

一个是（0，1，0）

另外一个是（1，0，ω）

（0，1，ω）这三个

这个节点和这个节点有什么特点呢

刚才我说了

这两个节点是一个死节点

再也没有变迁可以发生了

就是你到了这儿到这儿以后

再也没有变迁可以发生了

所以这个呢就是死节点

但是这个不一样

这个节点它是个活的

这个节点b永远可以发生下去

所以这两列看上去都是叶节点

但是这个叶节点跟叶节点不同

有的是死的有的是活的

那么我们怎么能够把它区分开呢

使得我们一眼就知道

这个叶节点是死了没有呢

那么就是用这个方法可达弧

我们把相同的两个叶节点

把它重叠起来

就是（1，0，ω）（1，0，ω）

我用一条弧把这两个叶节点重复

用一个节点来表示

然后用这个循环这么一个箭头

来表示从这个节点

还是可以经过变迁的发生

回到这个节点的

这是一个特例自己回到自己了

我们这个例子简单是回到自己

这个呢就叫做一个可达图

它已经不是一棵树了是一个图的结构

这个图比树有用

我们将来你看

这个同步距离的计算呢等等那些东西

都可以用到这个覆盖图而不是覆盖树

我们看看这个图

这个图是不是活的

不是活的为什么

这个a是个死变迁

它到了这里它就动不了了对不对

它没有可能性再发生

所以这是个死的

另外有界没有界呢

无界

因为它这有个ω出现了

是个无界的

公平不公平呢

当然是不公平的

这个b可以无穷多的发生对吧

这个a只发生一次就完蛋了

这个系统就不转了

所以呢这是一个

无界的 不活的

不公平的一个网系统

所以这个覆盖图覆盖树

我们可以这个用来回答

我们提出来的那些系统的性质

这是我们构造这个覆盖树的算法

这个算法书上是有的

这是我们分析一个网系统

性质的这个方法

就是构造它的一棵大树

或者可覆盖树覆盖图

可达图和覆盖图有什么区别呢

如果你这个图里面没有ω

它就叫可达

如果有ω就叫覆盖

因为那个ω是用来覆盖的

那么如果没有ω

那就说我权在这了

所以它就是可达的

注意我们这个分析的

都是刚才我说的

什么有界性啊 活性啊 公平性

但是我以前也说过

这个公平性也好活性也好

都不是特别的有针对性的定义的性质

那么我们自己在做应用的时候

应该根据你自己的应用系统的特点

应用领域的特点

定义出你自己的性质来

然后开发出你自己

有针对性的那个分析方法