首页 文章

基数约束不可满足

提问于
浏览 次
1

即使在简单的例子中，我也无法使Alloy的基数运算符（ # ）按预期工作 .

例如，以下Alloy文件......

sig Y {}

sig X {r : Y -> Y} {
//#r = 2
}

run {} for exactly 1 X, 3 Y

...给我一个恰好包含2个 r -edges的解决方案（见下图） . 但是，如果我取消注释 #r = 2 线，合金找不到解决方案！我究竟做错了什么？

enter image description here

Edit. 我发现这个问题只会影响AlloyStar（而不是香草合金） . 当使用AlloyStar（0.2版）时，我得到了

执行“为1 X，3 Y运行运行$ 1”Solver = minisatprover（jni）Bitwidth = 1 MaxSeq = 0 Symmetry = 20 69 vars . 12个主要的变种 . 167条款 . 923ms . 实例发现 . 谓词是一致的 . 21ms .

但当我取消注释 #r = 2 时，我明白了

执行“为1 X，3 Y运行运行$ 1”Solver = minisatprover（jni）Bitwidth = 1 MaxSeq = 0 Symmetry = 20 0 vars . 0个主要变量 . 1条款 . 为15ms . 找不到实例 . 谓词可能不一致 . 1毫秒 .

所以我想这个问题已成为AlloyStar开发人员的错误报告！

alloy

2 回答

  • 2

    感谢错误报告 . 这里有几件事情 . 从本质上讲，所说的一切都是正确的，但完整的答案会更加细致入微 .

    首先，我假设你将“Forbid Overflows”选项设置为true，否则无论指定的整数范围（bitwidth）如何，都会得到一个实例 .

    接下来，我们不要使用“附加事实”，因为附加事实可以具有不同的语义，具体取决于是否启用了“启用隐式此选项”选项 . 那么让我们假设以下Alloy模型：

    sig Y {}
sig X {r: Y -> Y} 

fact { #r = 2 }

run {} for exactly 1 X, 3 Y

    现在，在Alloy4.2中，当没有指定整数绑定时，引擎用来表示整数表达式的默认位宽（例如，基数表达式，整数常量等）是5;由于常数2可用5位表示，因此不会发生溢出并找到实例 .

    另一方面，在Alloy *中，默认位宽为1，其宽度不足以表示常量2，因此发生溢出并且未找到实例 . 为什么选择bitwidth 1作为默认值？我不是100％肯定，但可能是因为添加了对位向量的支持，以及使用位向量的一些综合基准，所以在编写时它很方便 .

    回复于
  • 2

    看来你必须配置位宽：

    执行“为1 X，3 Y运行运行$ 1”Solver = minisatprover（jni）Bitwidth = 1 MaxSeq = 0 Symmetry = 20 0 vars . 0个主要变量 . 1条款 . 为15ms . 找不到实例 . 谓词可能不一致 . 1毫秒 .

    数字2不能用位宽1表示 . 我认为该示例适用于标准Alloy，因为默认位宽更高 .

    回复于

相关问题