标号迁移系统.ppt

文档介绍：标号迁移系统
中国科学院软件研究所
张文辉
/~zwh/pv
自动售茶机
s0
1
1
1
2
1
取茶
s1
s3
s5
2
s2
2
s4
找钱/取钱
2
退钱
s6
s7
出茶
取钱
*
互斥协议：卫式迁移模型
初始状态：
迁移集合：
*
互斥协议：示意图
x==0||t==0
t0
x=1,t=0
t1
t2
y==0||t==1
t3
x=0
s0
y=1,t=1
s1
s2
s3
y=0
初始状态
s0
t0
x=0
y=0
t=0
*
z0
z12
z35
z67
z97
z46
z20
z24
z47
抽象状态变化图:
z78
z55
a: 进程A的运行 b: 进程B的运行
*
z0
z12
z35
z67
z97
z46
z20
z24
z47
抽象状态变化图:
z78
z55
b
a
b
a
a: 进程A的运行 b: 进程B的运行
a
a
b
a
b
b
*
标号迁移系统
*
标号迁移系统
动作信息
系统状态
状态变化
初始状态
符号
抽象状态
三元组
状态集合
标号迁移系统
*
标号迁移系统：例子
标号集合：
状态集合：
迁移关系：
初始状态集：
{ a, b }
{ z0, z1, z2, z3, … }
{ (z0,a,z35), (z0,b,z12), … }
{ z0 }
*
Büchi自动机