Model Checker（通用检查器）负责通用任务枚举所有可达状态生成并探索状态转移搜索错误状态输出状态图Python Generator（生成器）是后面实现Model Checker的一个关键技术yieldnext()yield利用 Generator，Model Checker 可以控制不同线程每次只执行一步，从而模拟不同的线程调度顺序。