ProB新增动画与验证功能，可交互演示逻辑系统状态演化
Animation, Verification and Visualisation of Prolog Transition Systems with ProB
- 基于Prolog的动画模式支持状态转移系统可视化
- 新增统计模拟、用户输入响应及可靠回放功能
- 适合教学演示与Event-B形式化证明辅助
ProB是一个基于Prolog的模型检测器、动画工具和约束求解器，用于高阶形式化规格。本文介绍ProB中基于Prolog的动画模式现有功能及其最新扩展：包括用于统计检验的仿真、更可靠的轨迹回放、支持用户输入的转移以及改进的状态可视化。通过案例研究，特别是对连珠棋（Connect Four）游戏策略的评估，验证了这些新功能的有效性。该工具对Event-B规范的定理证明、教学演示中的互动可视化等应用同样具有价值。
原文摘要 · Abstract (English)
ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB's new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。