课程项目2——模型检验，本项目可独立或合作完成（合作者每组最多3人），要求按时提交。
有限状态迁移系统（Finite Labelled Transition System) 是形式化方法中常用的模型之一。一个有限状态迁移系统包含有限个状态（State）和一系列的迁移（Transition），每个迁移包括起始状态，后继状态和一个动作，当系统处于起始状态时，可以执行该动作并跳转到其后继状态。一个简单有限状态迁移系统的例子（Coffee Machine）定义如下所示：
idle paid
idle
coin idle paid
coffee paid idle
第一行给出所有状态的名称（名称只能包含大小写英文字母和数字，用空格隔开）。在这个例子中，咖啡机共有两个状态，分别是待机（idle）以及已付款（paid）。第二行给出系统的初始状态，在这个例子中为idle。之后每一行描述一个迁移（三个由空格分开的字符串，分别是动作名称，起始状态和后继状态）。其中起始状态和后继状态必须是第一行中出现过的。
一个有限状态迁移系统的运行过程如下：
最开始，系统处于其初始状态
如果系统的当前状态上存在一个迁移，那么就执行这个迁移并跳转到它的后继状态
如果存在多个迁移，系统会随机选择一个执行
将系统执行过程中的动作序列记录下来，我们称为它的一个迹（Trace）。例如，例子中系统的迹可以是如下的无限序列：
coin, coffee, coin, coffee, ...
显然，一个有限状态迁移系统所对应的迹不是唯一的，而是一个集合。
时序逻辑用于描述系统满足的时序性质，常用的时序逻辑包括线性时序逻辑、计算树逻辑等。例如线性时序逻辑（Linear Temporal Logic）可以描述一个系统在线性时间上的变化所要满足的条件。一个线性时序逻辑公式L的定义如下所示：
L：：= True | a | L1 and L2 | not L | X L （next）| L1 U L2 （until）
具体含义见[1]，[2]。
假设我们有一个线性时序逻辑公式（not coffee）U coin），那么我们可以看出上述的系统是满足这个公式的。因为它唯一的一条轨迹上从初始位置开始，一定不会出咖啡直到用户付款（这很显然！因为总共只有两个状态……）
如果给定一个有限状态迁移系统TS和一个线性时序逻辑公式L。当且仅当TS所有可能的轨迹均满足L时，我们说TS满足L。
基本要求：
设计并实现一个LTL/CTL的模型检查工具，使得对给定的状态迁移系统TS和LTL/CTL公式L，可以判断TS是否满足L，若满足，返回True，若不满足，返回False并给出TS中一条不满足L的路径作为反例。并对所给出的实现进行性能分析。
示例输入文件格式：
第一行为n个用空格分开的字符串，描述状态迁移系统的每个状态名称。第二行为一个字符串，描述状态迁移系统的初始状态。之后的若干行为状态迁移系统的边，每行由三个字符串组成，分别是：动作，起始状态，目标状态。中间用空格隔开之后空一行。然后每一行是一条要检查的时序逻辑公式。为简化问题，我们假设任何运算都由括号括起，从而不存在优先级的问题。到文件结束为止。
示例输出文件格式：
m行（m为公式的条数），每行为True，或者False加上一个状态序列作为反例，表明该模型满足公式或者不满足且给出反例。
选作：
1. 在LTL/CTL公式中可使用其他扩充运算符，如eventually、always、weak until等。
2. 设计并实现其他时序逻辑（如CTL*、TCTL、PCTL等）的模型检查算法。
本次上机实习报告要求：
- 独立或合作完成（合作者每组不超过3人），写出上机实习报告（不少于6000字），在报告中注明每人工作。
- 本次报告和程序12月22日晚12点之前由第一作者通过系统提交。
- 程序和实习报告都采用电子文档形式打包上传。
- 上交所有源文件及测试用例，应保证程序能编译和执行。
- 保证自己上交的文档中没有病毒。
- 不要在报告中大量使用源代码凑字数。
注意：
1. 感兴趣的同学可以考虑选作内容，不做这部分的内容不会导致本次报告成绩降低。
2. 数据结构的设计和算法的效率是需要重点考虑的问题，不需要把太多的时间花在图形界面上。做了图形界面并不是加分项。
3. 可自己定义输入输出文件格式，但需在报告中说明。
参考文献（院图馆藏）：
[1] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.
[2] Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled. Model Checking, The MIT Press, 1999. |
