1Chapter 2 有限状态机及其扩展 o有限状态机 n 有限状态机是有限计算的基本模型，也是许多形式化规格、验证方法的基础模型。o Statecharts n Statecharts是通过定义递阶状态、状态的AND或OR分解等高级特性的有限状态机的一种扩展形式。2（一） 有限状态机（1） 基本概念 有限状态机（finite state machine）或有限自动机（finite automata）是有限计算的基本模型，是许多形式化规格、验证方法的基础模型。 超级商场的自动门控制器 自动门的前、后分别有两个缓冲区。自动门的前缓冲区用来检测是否有人接近。自动门的后缓冲区，使得控制器把门打开足够长的时间让人走进去，并且不让门在打开的时候碰到站在它附近的人。自动门控制器依据前缓冲区、后缓冲区的检测信息给出打开或闭合的动作指令。 自动门的动作控制应满足如下要求（规格）： 当前缓冲区和后缓冲区均无顾客出现，则自动门处于闭合状态； 当后缓冲区有顾客出现，则自动门维持其原有状态； 当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。前缓冲区后缓冲区（1） 基本概念状态集合Q = closed, ope
