文档介绍：自动售茶机s011121取茶s1s3s52s22s4找钱/取钱2退钱s6s7出茶取钱2互斥协议:卫式迁移模型初始状态:迁移集合:3互斥协议:示意图x==0||t==0t0x=1,t=0t1t2y==0||t==1t3x=0s0y=1,t=1s1s2s3y=0初始状态s0t0x=0y=0t=04z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55a:进程A的运行b:进程B的运行5z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55babaa:进程A的运行b:进程B的运行aababb6标号迁移系统7标号迁移系统动作信息系统状态状态变化初始状态符号抽象状态三元组状态集合标号迁移系统8标号迁移系统:例子标号集合:状态集合:迁移关系:初始状态集:{a,b}{z0,z1,z2,z3,…}{(z0,a,z35),(z0,b,z12),…}{z0}9Büchi自动机10z0z12z35z67z97z46z20z24z47抽象状态变化图:z78z55babaa:进程A的运行b:进程B的运行aababb