论文标题
FSM中确定性有限状态机的视觉设计和调试
Visual Designing and Debugging of Deterministic Finite-State Machines in FSM
论文作者
论文摘要
本文介绍了一种可视化工具，用于在FSM中设计和调试确定性有限状态机器，这是自动机理论教室的域特定语言。像其他自动机构可视化工具一样，用户可以编辑机器并观察其执行，给定一些输入。与其他自动机构可视化工具不同，用户不会因渲染机器作为图形而负担或分心。此外，重点放在机器的设计上，本文为确定性有限状态机器提供了一种新颖的设计配方。为了支持设计过程，可视化工具允许每个状态与不变谓词相关联。在机器执行过程中，可视化工具指示每个过渡后提出的不变性是否持有或不保持。通过这种方式，学生可以在试图证明部分正确性或提交评分之前验证和调试机器。此外，使用可视化工具编辑的任何机器都可以作为可执行代码渲染。提供了可视化工具的接口以及其使用的扩展示例。
This article presents a visualization tool for designing and debugging deterministic finite-state machines in FSM -- a domain specific language for the automata theory classroom. Like other automata visualization tools, users can edit machines and observe their execution, given some input. Unlike other automata visualization tools, the user is not burdened nor distracted with rendering a machine as a graph. Furthermore, emphasis is placed on the design of machines and this article presents a novel design recipe for deterministic finite-state machines. In support of the design process, the visualization tool allows for each state to be associated with an invariant predicate. During machine execution, the visualization tool indicates if the proposed invariant holds or does not hold after each transition. In this manner, students can validate and debug their machines before attempting to prove partial correctness or submitting for grading. In addition, any machine edited with the visualization tool can be rendered as executable code. The interface of the visualization tool along with extended examples of its use are presented.
