Video在线视频

这同步距离的第二个应用呢

就是规范软件

我们讨论的就是教堂婚礼

教堂婚礼我们已经讲过了

那个petri网怎么描述教堂婚礼

将来我们要设计一个软件

指挥教堂婚礼的话

那么我们应该怎么给它做规划呢

我们的目的就是

把这个细节的东西去掉

先抓主要矛盾

主要的事件是什么

一共有三个

一个是神父和新郎交互

一个是神父和新娘交互

然后是新郎和新娘交互

这是三个主要的事件 必不可少的

他们之间的这个其他的安排都是属于细节

我们看怎么来描述他们之间的依赖关系

神父和这个新娘的交流

跟这个新郎新娘之间的交流

他们的同步距离应该是1

神父跟新郎交流了以后

然后就是他们两个互相交流

因此神父和他们的关系

这个就是同步距离为1

神父跟新郎交流

神父跟新娘交流这两个事件

它是同步距离是几呢

因为这一对婚礼

这个神父可以先跟新娘交流

下一对婚礼神父可以先跟新郎交流

所以有可能神父

连续两次都跟新郎交流

也有可能连续两次先跟新娘交流

所以呢这个同步距离呢就是2

而且我们知道距离公理里面

有个三角不等式

这个a b的同步距离呀

一定是小于a c加b c的

所以这个同步距离呢应该是小于等于2

三角不等式小于等于2

所以我们现在呢有两种选择

一种选择呢 就是同步距离

𝜎(𝑎,𝑏)的同步距离等于1

或者同步距离等于2

我们画出图来就是这样

a b这是新郎新娘分别跟神父的交流

他们之间的同步距离

我们现在假定选择等于2

也就是说允许神父

连续两次就是跟

这一对的新郎后交互

跟下一对的新郎先交互

这就是我们前面看到的那个例子

就是是冲突的

就是新郎新娘的交互啊 不固定顺序

由神父来自己选择

这就是同步距离为2

那么如果你要是同步距离为1呢

那就等于是规定

神父必须先跟新娘交流

再跟新郎交流

下一队仍然是

先给新娘交流 再跟新郎交流

所以这样呢 就是这个两种可能的选择

这个教堂婚礼呢

这个主要事件之间的依赖关系

我们用同步距离就可以这样描述

当然了 我们这样规范出来的

是以petri网为基础的

那么我们得到的是一个petri网

那么如果要是你要想得到一个程序的话

教堂当然可能不需要程序

但是你要是其它的软件

你需要写成程序的话

用程序语言来改写

我前面介绍过的C_net呢就是一种选择

它既有petri网的这个结构

又有程序语言的这个各种成份

而且它是并发的

那么我如果用C_net来表示

它就是可执行的程序了

软件规范呢我就简单的说到这

因为软件规范本身就是一个大问题

如果我们拿出一个

真正的软件问题来讨论它的规范的话

那就会花很多时间

不是我们petri网的内容了

下次你要有这个机会呢不妨试一试

看看能不能用同步距离

来规范你的那个软件里面

主要的子任务啊

或者子程序啊之间的关系

最主要的这个同步距离的作用

是对系统进行控制

我们知道同步距离

是网系统里面算出来的

就是你这里面就是这两组事件

是怎么互相依赖的

它们的规律性是什么

那么做系统控制呢是我们反过来用

把这个同步距离作为一种手段

反过来用

我不是算算你怎么互相依赖的

而是我规定你怎么依赖的

显然如果我们增大这个容量的话

那么它的自由度就大了

如果缩小呢

它的自由度就小了

咱们看顺序 同步距离为1

描述的是顺序关系

因为它只能是ababa这是第一行

或者是babab因为交替吗

a一下b一下a一下b一下

我们所有的自由度只有第一次

你是先a呢还是先b呢

就这个花括号所代表的

这是唯一的我们有自由选择的地方

你如果要求 𝜎(𝑎,𝑏)

就同步距离是1的话

那么只有两种可能性两种序列

或者a开头或者b开头

后面就只能是交替发生了

为了简单起见我已经把这个

E1 E2改写成小a小b了

这样看起来清楚一些

自由度大一点

我们把 𝜎同步距离改成2

第一个选择呢就是那个

最左边的那个花括号a也行b也行

第一个如果是a了第二个选谁呢

因为它是同步距离是2

所以呢仍然你有选择权

你可以选a也可以选b

所以又有第二个括号

然后如果你选了a

这个a已经连续发生两次了

你就没有选择权了

所以最上面呢就是ab

那个a以后因为a已经连续发生两次

只能是b b了以后

又有发生选择权了

或者a或者b

所以我们看整个这个图

发生有小的这个花括号的地方

就是我们有选择权的地方

你看只是同步距离增加了1

可以自由的选择的地方

就是我们的系统的控制就少了

系统可以自由选择的地方就多了

这样呢我们就可以加大

或者缩小对系统的控制

那么在控制论里面

我不知道这个是不是会有用

因为我对控制论不熟悉

也没有去研究过

那我就不多说了