我正在用合金语言描述一些模型。为了描述一个有限状态机,我提供了这几行代码:
sig FSA_state {
transitions: some FSA_state,
initial: lone InitialState
}
sig InitialState {}
fact i {
all f: FSA_state | #(f.transitions) <= 0
}
pred show {
}
run show for 5 but 1 InitialState
现在我试图弄清楚为什么它在单个状态上进行的转换不止零。使用“评估器”工具,我发现某些世界在集合转换上具有负基数,这怎么可能(集合不能少于零元素)?我在 Evaluator 中使用的指令是#(FSA_state.transitions)