时间迁移系统.ppt

时间迁移系统
自动售茶机
s0
1
1
1
2
1
取茶
s1
s3
s5
2
s2
2
s4
找钱/取钱
2
退钱
s6
s7
出茶
取钱
{x}
x<10
x>=10
量的变化
do时间迁移系统
自动售茶机
s0
1
1
1
2
1
取茶
s1
s3
s5
2
s2
2
s4
找钱/取钱
2
退钱
s6
s7
出茶
取钱
{x}
x<10
x>=10
量的变化
docin/sundae_meng
docin/sundae_meng
时间迁移系统
x==0||t==0
docin/sundae_meng
系统运行过程描述:例子
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
无约束
docin/sundae_meng
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
docin/sundae_meng
时间变化

b a a b b
z0z12 z12 z12 z20 z24
u=, u= u= u= u=
u=, u= u= u= u=
v= v= v= v= v=
v= v= v= v= v=
docin/sundae_meng
时间迁移系统
动作信息
系统状态
时钟变量
状态变化
初始状态
符号
抽象状态
变量集合
五元组
状态集合
时间迁移系统
docin/sundae_meng
时间迁移系统:例子
标号集合:
状态集合:
时钟变量集合:
迁移关系:
初始状态集:
{a,b}
{z0,z1,z2,z3,…}
{u,v}
{(z0,a,{v},true,z12),…}
{z0}
时钟变量相关公式
docin/sundae_meng
时间迁移系统:例子
S0
S1
a
S2
S3
d,y>2
x:=0
b
y:=0
c
x<1
docin/sundae_meng
时间Buchi自动机2
S0
S1
S2
S3
S2
a,y:=0
a,x:=0
x=1
b,y:=0,y<1
a,x:=0,x=1
docin/sundae_meng
时间Buchi自动机2
docin/sundae_meng
时间Buchi自动机2:运行/语言
混成迁移系统/混成自动机
docin/sundae_meng
混成迁移系统/混成自动机
水箱
x<=2
x>=5
x:=x+1
x'=1
x<=9
x'=-1
on
off
docin/sundae_meng
混成迁移系统/混成自动机
水箱
x'=1
x'=-1
on
off
on2off,{x:=x+1},x>=5
off2on,{},x<=2
x<=9
docin/sundae_meng
docin/sundae_meng
混成迁移系统/混成自动机
动作信息
系统状态
变量状态
状态变化
初始状态
符号
抽象状态
变量集合
五元组
混合状态集合
混成自动机
混成自动机
docin/sundae_meng
混成自动机
docin/sundae_meng
docin/sundae_meng
Petri网
x==0||t==0
docin/sundae_meng
系统运行过程描述:例子
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
docin/sundae_meng
系统资源模型
s0
s1
s2
s3
t0
t1
t2
t3
docin/sundae_meng
系统资源模型
t0
t1
t2
t3
s0
s1
s2
s3
docin/sundae_meng
系统资源模型
t0
t1
t2
t3
s0
s1
s2
s3
docin/sundae_meng
系统资源模型
t0
t1
t2
t3