合金没有找到适合我的规格的解决方案（实例）

Question

我一直在关注合金文档并同时编写规范，但我得到了与文档所说不同的结果：

回想一下，如果没有任何时间运算符，添加的约束仅适用于第一个状态。执行此命令会生成一个带有单个文件的实例，该文件会立即被删除。通过按→，我们会进入与清空垃圾相对应的以下转换。

这是我的规格：

var sig File {}
var sig Trash in File {}

// empty the trash
pred empty {
    some Trash
    no Trash
    File' = File - Trash
}

// delete a file from the disk (& put in the trash)
pred delete [ f : File ] {
    not (f in Trash)
    Trash' = Trash + f
    File' = File
}

// restore a file from the trash
pred restore [ f : File ] {
    f in Trash
    Trash' = Trash - f
    File' = File
}

// user is doing sth else
pred do_sth_else {
    File' = File
    Trash' = Trash
}

fact system {
    always (empty or ( some f : File | delete[f] or restore[f] ) or do_sth_else )
}


run no_files {
    some File
    eventually no File
} for 5

执行后，我得到这个：

Executing "Run no_files for 5"
   Sig this/File scope <= 5
   Sig this/Trash in [[File$0], [File$1], [File$2], [File$3], [File$4]]
   Sig this/File in [[File$0], [File$1], [File$2], [File$3], [File$4]]
   Solver=sat4j Steps=1..10 Bitwidth=4 MaxSeq=5 SkolemDepth=1 Symmetry=20 Mode=batch
   1..10 steps. 11274 vars. 660 primary vars. 18586 clauses. 77ms.
   No instance found. Predicate may be inconsistent. 2ms.

所以，基本上，Alloy 无法找到一个实例，在 5 个步骤之后，文件系统包含 0 个文件，对吗？

我在Alloy软件中执行了代码

Answer 1

实际上测试了十步，如果你想要最多五步，你必须写

run {} for 5 but 5 steps

。

无论如何，问题是这个谓词：

pred empty {
    some Trash
    no Trash
    File' = File - Trash
}

some Trash && no Trash

是错误的，所以永远不能使用它。相反，你想要这个：

pred empty {
    some Trash
    no Trash'
    File' = File - Trash
}