使用 ProB 对 Prolog 转移系统进行动画、验证与可视化

论文介绍 ProB 中用于动画化 Prolog 转移系统的既有能力及近期扩展，包括统计检查模拟、更可靠的轨迹重放、用户输入驱动的转移和改进的状态可视化。作者以 Connect Four 等博弈策略案例展示其用途，并讨论其在 Event-B 顺序证明器和交互式教学模型中的价值。