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 の基礎を学ぶことをお勧めします。