FSV5, FSUZ_Lightfoot_07

系统（飞机）

类型：

• 集合 [PERSON]
• 变量（基本、自由）

状态：

• 声明系统的变量（取子集）
• 约束

初始化：

• 到下一状态
• 空集

操作：

• 每一种操作对应系统的状态改变 $\Delta$（系统变量改变）
• 声明输入 ? 变量
• 变量约束、次态变量操作

查询：

• 每一种查询对应系统的状态改变 $\Xi$（系统变量不变）
• 声明输入 ? 输出 ! 变量
• 对应输入变量，赋值给输出变量
• 不同情况用 $\vee$ 连接，同一情况用 $\wedge$ 连接