有限状态机与下推自动机的可视化执行与验证

在形式语言和自动机理论课程中，学生发现理解非确定性有限状态机和下推自动机困难。在许多情况下，这意味着他们难以理解此类机器的操作语义，从而难以确定单词为何被接受或拒绝。这并不全然令人惊讶，因为学生主要训练用于设计和实现确定性程序。对下推自动机的理解进一步复杂化，因为需要推理关于堆栈的行为。学生普遍面临的一个困难是，例如，理解同一单词上的两个不同计算可能到达同一状态但堆栈值不同。为帮助学生理解，我们提出了两种新的动态可视化工具用于 FSM — — 一种用于自动机理论教室的领域特定编程语言 — — 以支持此类机器的设计。这两种工具以逐步方式可视化可能由非确定性有限状态机或下推自动机执行的所有计算。此外，这些工具通过允许用户可视化验证状态表示的属性在机器转换进入该状态时是否成立，从而有助于机器验证过程。