代码之家 › 专栏 › 技术社区 › Max von Hippel MD. Sahib Bin Mahboob

为什么在Alloy中不出现简单的整数反例?

formal-methods formal-verification alloy scope

0

Max von Hippel MD. Sahib Bin Mahboob · 技术社区 · 7 年前

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 Object 应该只有一个 integer 还有一个 discrete 整数 . 但即使有1000个案子

如果我移除 整数 变量和相关的事实,然后它几乎立即找到了反例。我也尝试过使用其他解算器,并在选项中增加各种深度和内存值,但这没有帮助,所以很明显我的代码是错误的。

如何限制我的范围使Alloy找到反例(通过迭代 整数

1 回复 | 直到 7 年前

1

Loïc Gammaitoni 7 年前

要解决此问题,请将使用的位宽度至少增加到5:

check discreteCondition for 10 but 5 Int.

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