0

我正在尝试对数值变量和布尔变量之间的关系进行建模，其中如果数值变量在某个范围内，则布尔变量将改变值。我是 Alloy 的新手，无法理解如何充分限制我的范围以产生明显的反例。我的代码如下：

open util/boolean 

one sig Object {
    discrete : one Bool,
    integer : one Int
}

fact { all o : Object | o.integer > 0 and o.integer < 10 }
fact { all o : Object | o.integer > 5 iff o.discrete = False }

assert discreteCondition { all o : Object | o.discrete = True }

check discreteCondition for 1000

由于o.integer是整数值并且范围从 0 到 10，因此它只能是 10 种不同选择之一。我指定每个Object应该只有一个integer和一个discrete。所以在我看来，这里实际上只有 10 个案例需要检查：每个integer. 然而，即使有 1000 个案例，我也得到了

没有找到反例。

如果我删除integer变量和相关事实，那么它几乎会立即找到反例。我也尝试过使用其他求解器并在选项中增加各种深度和内存值，但这并没有帮助，所以很明显我的代码有问题。

如何限制我的范围以使 Alloy 找到反例（通过迭代 的可能值integer）？谢谢！

4

1 回答 1

1

默认情况下，用于表示整数的位宽为 4，因此在实例生成期间仅考虑 [-8,7] 范围内的整数，因此，由于整数溢出，您的第一个事实是 void（因为 10 超出此范围）。

要解决此问题，请将使用的位宽增加到至少 5：

check discreteCondition for 10 but 5 Int.

请注意，1000 的范围并不意味着您在分析中考虑了 1000 个案例。范围是生成的实例中存在的最大原子数，在给定签名之后键入。在您的情况下，您只有一个具有多重性的签名。因此，分析范围为 1 或 10000 的模型不会改变任何内容。生成的实例中仍然只有一个 Object atom。您可能希望查看此 Q/A 以了解有关范围的更多信息

于 2018-09-21T07:33:25.583 回答