程序与系统模型-例子2d - 中国科学院软件研究所

时间迁移系统,中国科学院软件研究所张文辉/zwh/pv,自动售茶机,s0,1,1,1,2,1,取茶,s1,s3,s5,2,s2,2,s4,找钱/取钱,2,退钱,s6,s7,出茶,取钱,x,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,u1,b,u5,a,v,true,a,v,true,b,u,u2,x:=0,b,y:=0,c,x1,10,时间迁移系统：例子,11,时间迁移系统：运行,12,时间Buchi自动机1,S1,S0,b,S2,S3,S2,a,a, x:=0,a, x:=0,b, x2,13,时间Buchi自动机1,14,时间Buchi自动机1：运行/语言,15,时间Buchi自动机2,S0,S1,S2,S3,S2,a, y:=0,a, x:=0,x=1,b, y:=0, y1,a, x:=0, x=1,16,时间Buchi自动机2,17,时间Buchi自动机2：运行/语言,混成迁移系统/混成自动机,混成迁移系统/混成自动机,水箱,x=5x:=x+1,x=1x=5,off2on,x=2,x=9,21,混成迁移系统/混成自动机,动作信息系统状态变量状态状态变化初始状态,符号抽象状态变量集合五元组混合状态集合,混成自动机,混成自动机,混成自动机,24,Petri网,x=0|t=0,25,系统运行过程描述：例子,t0,x=1,t=0,t1,t2,y=0|t=1,t3,x=0,s0,y=1,t=1,s1,s2,s3,y=0,初始状态s0t0x=0y=0t=0,26,系统资源模型,s0s1s2s3,t0t1t2t3,27,系统资源模型,t0t1t2t3,s0s1s2s3,28,系统资源模型,t0t1t2t3,s0s1s2s3,29,系统资源模型,t0t1t2t3,s0s1s2s3,30,Petri网,位置迁移状态变化描述初始状态,抽象元素抽象元素边（两种）位置标号,Petri网,31,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,32,Petri网：例子,位置集合：迁移集合：边的集合：初始状态：, s0,s3,t0,t3, ts u0,u3,v0,v3 (s0,u0),(u0,s1),(s1,u1),(ts,u1),M: M(s0)=1,M(s1)=0,M(s2)=0,33,有问题的系统资源模型,s0u0s1u1s2u2,t0v0t1v1t2v2,34,通信系统,35,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,36,系统资源模型,ts ! 1ts ? 1,ts ! 1ts ? 1,ts,37,系统资源模型,ts ! 1ts ? 1,ts ! 1ts ? 1,ts,38,系统资源模型,1,ts ! 1ts ? 1,ts ! 1ts ? 1,ts,39,系统资源模型,ts ! 1ts ? 1,ts ! 1ts ? 1,ts,40,通信系统,状态通道状态变化初始状态,抽象状态二元组三元组给定状态,通信系统,41,系统资源模型,t0t1ts !1t2ts ? 1t3,s0s1ts ! 1s2ts ? 1s3,ts,42,通信单元：例子,状态集合：通道集合：迁移关系：初始状态：, s0,s3 ts: (s0,s1),(s1,ts?1,s2), s0,通信系统：通信单元的组合,43,通信系统：例子,q0,q1,q2,q3,q4,q5,!0,?1,?0,!1,?1,?0,!0,!1,44,通信系统：例子,q2,q0,q1,q3,q4,q5,?0,!0,?1,!1,?0,?1,!0,!1,45,通信系统：例2,rw()=1,2y+x=(y+x)%4,s0,t1,S!B,t0,B+1=b,B+,B+1 !=b,R!(A+rw(),s1,S?A,R?b,46,通信系统：例2,s0,s1,m1!1,m1!2,m2?1,m2?2,m2?0,s3,s2,m2?2,m2?3,m2?0,m1!2,m1!3,m2?3,m2?0,m2?1,m1!3,m1!0,m2?0,m2?1,m2?2,m2?3,m1!0,m1!1,m2?1,m2?2,m2?3,47,通信系统：例2,t0,t1,m2!0,m1?1,m1?2,m1?0,t3,t2,m1?2,m1?3,m1?0,m2!1,m1?3,m1?0,m1?1,m2!2,m1?0,m1?1,m1?2,m1?3,m2!3,m1?1,m1?2,m1?3,48,通信系统：例2,rw()=1,2,W,s0,t1,S!B,t0,B+1=b,B+,B+1 !=b,R!(A+rw(),s1,S?A,R?b,49,通信系统：例2,Window Protocol InvariantB W Ri B + W for 1 i r,50,通信系统：例2,Window Protocol InvariantB W Ri B + W for 1 i r,引理1：A S1 Ss B,引理2：设 R0=B, Rr+1=A+1 则 Ri Rj