2

我正在用合金语言描述一些模型。为了描述一个有限状态机,我提供了这几行代码:

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)

4

2 回答 2

1

如果要排除所有有溢出的模型,可以设置 4.2 版本提供的“禁止溢出”。

于 2014-01-14T14:29:35.533 回答
0

事实上,我强制每个 FSA_state 的转换次数应该是负数。在您的签名 FSA_state 中,使用关键字“some”强制转换次数至少为 1。

在您设法生成的实例中,Alloy 利用了 Integer 签名的有限范围来满足两个相互矛盾的约束。

实际上,例如,如果整数的范围从 -2 到 3,那么如果每个状态的转换数为 4,则 #(f.transition) 将为 -2。

TL;DR:删除 i 事实(关键字 some 已经强制每个 FSA_state 至少有一个转换)

于 2014-01-11T15:50:50.603 回答