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 回答