| 经典Petri网：库所（place）用圆表示，库所中包含（非负）整数个标记，称为令牌（token），用圆点表示；Petri 网的状态由令牌在库所的分布表示；变迁用竖线或方框表示，代表某种处理 | 容灾双中心有多种子状态，系统状态是所有子状态值的组合。对一个业务系统，包含以下3种子状态：系统运行状态（online、offline、maintenance）、容灾主备状态（北京主、上海主）、容灾模式（同步、跟随），则系统状态有：｛北京online，上海Online，北京主，同步｝ |
| ｛北京online，上海Online，北京主，跟随｝ |
| ｛北京online，上海Offline，北京主，跟随｝… |
| 容灾切换的每一个操作命令相当于一个变迁 |
| 经典 Petri 网：对于一个变迁，如果它的每个输入库所（input place）都拥有令牌，则该变迁为“可点火的”（enabled） | 执行操作是有前提的，如应在系统offline时执行启动命令，把系统启动到online；在系统是online时，不应当执行启动命令； |
| 有些操作需要在某个状态组合下才能执行，如“切换到北京主”的操作，要求必须在“上海主”、双中心“业务系统maintenance”、“同步消息队列为空”的条件下才能执行，否则会导致切换后数据不一致、系统无法正常运行 |
| 经典Petri 网：变迁“点火”（fire）后，其所有输入库所的令牌被消耗一个，同时向所有的输出库所（output place）中增加一个令牌 | 操作执行之后，系统状态将发生变换，如执行启动命令，系统会从offline（操作前的状态）启动到online（操作后的状态） |
| 经典Petri 网：如果两个变迁共享输入库所，当这两个变迁同时具备点火条件，且共享的输入库所只有一个令牌时，某个变迁点火将剥夺另一个变迁点火的机会 | 如在双中心同步运行时，系统进入单点运行和双中心跟随运行都是可以的；但系统一旦选择了进入单点运行，则不能再直接切换到双中心跟随状态 |
| 着色Petri网[10]：对库所和令牌赋予颜色属性，如果一个变迁有多个输出库所，点火后检查所生成令牌的颜色，只有与令牌颜色相同的输出库所里才产生令牌 | 有些操作执行后，可能设置多个状态之一，如启动命令如果执行成功，则系统会到online，执行失败则仍在offline |
| 时间Petri网[11]：一个变迁具备点火条件后，还需要满足一定的时间条件，如延时一定时间后，才能点火 | 容灾切换可分为“手动档”和“自动档”模式。“手动档”表示人工单步操作，每一步都可选择执行任何一个“可点火”的变迁；“自动档”表示每个变迁点火之后，由Petri网中间件自动选择后续的“可点火”变迁并执行点火。为提高变迁执行的可靠性，自动档下每个变迁都要延时一下再点火下一变迁 |
| Petri 网分层[11]：变迁可以是另一个Petri 网模型，即变迁精化；库所也可以是另一个Petri模型，即库所精化 | 某个切换操作可能包含多个命令，如同步切跟随，就需要分别执行北京和上海两个系统的容灾模式切换命令 |
| 可达性：从某个初始状态（令牌在库所中的某种分布）出发不断进行变迁点火，对模型运行可能到达的状态进行研究 | 从双中心同步运行状态（正常生产）开始进行切换，研究可能发生的所有场景中系统状态的变换情况。如§2.3所述，对于中国电信全国计费容灾双中心来说，可能的状态组合数量极大，完全不能通过人工分析得到 |
| 有界性（安全性）：从某个初始状态出发不断进行变迁点火，某个库所中令牌数量永远是有限的（如果这个上限为1，则为安全的），则称这个库所是有界的；如果所有库所均有界（安全），则称这个Petri网为有界的（安全的） | 业务系统的状态只能是“是”和“否”两种。对应到Petri网，库所中最多只能包含一个令牌。对于容灾切换控制来说，Petri网模型应该是安全的 |
| 弱活性：从某个初始状态出发，无论变迁序列如何，不会出现没有任何变迁可以点火的情况 | 容灾切换控制要求无死锁，也就是说，即使某一步操作失败，也要继续控制业务系统继续或回退到一个稳定的系统状态，死锁意味着无法恢复到双中心同步运行的初始状态 |
| 一级活：从某个初始状态出发，对于系统中任何一个变迁，均存在具备点火条件的机会 | 如果容灾切换的Petri网模型不满足一级活，则说明其中某个或某些操作的设计是没有意义的，因为它永远也不会得以执行 |
