Alloy does not find a solution (instance) for my specification

Question

I've been following the Alloy docs and writing the spec at the same time, but I get a different result from what the docs say:

Recall that without any temporal operator, the added constrain applies only to the first state. Executing this command yields an instance with a single file that is immediately deleted. By pressing → we get to the following transition corresponding to the emptying of the trash.

Here's my spec:

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

After execution, I get this:

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.

So, basically, Alloy is unable to find an instance where, after 5 steps, the filesystem contains 0 files, right?

I executed the code in the Alloy software

Answer 1

It's actually testing for ten steps, if you want it up to five you have to write run {} for 5 but 5 steps.

Anyway, the problem is this predicate:

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

some Trash && no Trash is trivially false, so it can never be used. You instead want this:

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