state-machine - 在 Alloy 中编写有限状态机规范

Question

我是合金新手。我正在尝试制定允许的模拟电话线规格。这是我的 FSM 图。

我编写了一个示例代码来说明状态转换。我的转换表是事实，但是输出乘数是合金语法中的一个问题。我无法运行此代码。

你会说我有什么问题吗。有什么建议吗？

module state
sig Input{}
abstract sig State {
transition:  Input-> State-> Output}
one sig  NULL extends State {}
one sig CALL_RECEIVED extends State {}
fact xTable {
NULL->one setup_ind :Input->CALL_RECEIVED->one alerting_req:Output in transition
CALL_RECEIVED->one disconnect_ind:Input->NULL->one clear: Output in transition
}
pred show {}
run show

Answer 1

问题是您在事实中使用了虚构的语法xTable。我建议您查看http://alloy.mit.edu/alloy/documentation.html并首先学习 Alloy 基础知识。