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并先学习合金基础知识。