防御性编程：对输入、状态和返回值进行检查，提前处理异常情况，提高程序的健壮性和可靠性。

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