时间迁移系统.ppt

文档介绍：时间迁移系统
中国科学院软件研究所
张文辉
./~zwh/pv
自动售茶机
s0
1
1
1
2
1
取茶
s1
s3
s5
2
s2
2
s4
找钱/取钱
2
退钱
s6
s7
出茶
取钱
{x}
x<10
x>=10
量的变化
3
时间迁移系统
x==0||t==0
4
系统运行过程描述:例子
t0
x=1,t=0
t1
t2
y==0||t==1
t3
x=0
s0
y=1,t=1
s1
s2
s3
y=0
无约束
<1
<5
无约束
无约束
<2
<8
无约束
5
z0
z12
z35
z67
z97
z46
z20
z24
z47
抽象状态变化图:
z78
z55
b,{u},true
b,{u},u<1
b,{},u<5
a,{v},true
a,{v},true
b,{u},u<1
6
时间变化

b a a b b
z0 z12 z12 z12 z20 z24
u=, u= u= u= u=
u=, u= u= u= u=
v= v= v= v= v=
v= v= v= v= v=
7
时间迁移系统
动作信息
系统状态
时钟变量
状态变化
初始状态
符号
抽象状态
变量集合
五元组
状态集合
时间迁移系统
8
时间迁移系统:例子
标号集合:
状态集合:
时钟变量集合:
迁移关系:
初始状态集:
{ a, b }
{ z0, z1, z2, z3, …}
{ u, v }
{ (z0,a,{v},true,z12), …}
{ z0 }
时钟变量相关公式
9
时间迁移系统:例子
S0
S1
a
S2
S3
d, y>2
x:=0
b
y:=0
c
x<1
10
时间迁移系统:例子