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
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
}