Alloy规范无实例返回：与官方文档结果不符的技术求助

按照Alloy官方文档规范编写的文件系统模型代码，运行run no_files命令后无法找到5步内文件数变为0的实例，执行日志显示"No instance found"。

原代码 #

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.

问题原因 #

核心错误出在empty谓词的定义上：

• 原代码中some Trash要求当前状态的回收站有文件，同时no Trash又要求当前状态的回收站为空，这两个约束完全矛盾，导致empty动作永远无法被触发。
• 而delete和restore动作都不会减少File集合的大小（File' = File），因此系统永远无法达到eventually no File的目标，自然找不到符合条件的实例。

修正方案 #

修改empty谓词，将no Trash改为no Trash'，表示下一状态回收站为空：

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

修正后，empty动作会在当前回收站有文件时触发，将回收站清空并移除对应文件，系统就能在两步内完成"删除文件→清空回收站"的流程，满足eventually no File的约束。

内容的提问来源于stack exchange，提问作者devio