为什么Alloy中不会出现简单的整数反例？答案

【问题标题】：Why doesn't simple integer counterexample occur in Alloy?为什么Alloy中不会出现简单的整数反例？
【发布时间】：2018-09-21 05:49:18
【问题描述】：

我正在尝试对数值变量和布尔变量之间的关系进行建模，其中如果数值变量在一定范围内，则布尔变量将改变值。我是 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 的可能值）？谢谢！

【问题讨论】：

标签： scope alloy formal-verification formal-methods

【解决方案1】：

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

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

check discreteCondition for 10 but 5 Int.

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

【讨论】：