Formal verification of Trash on Alloy 6

trash.als

module Trash

var sig File {}

var sig Trash in File {}

fact init {
	no Trash
}

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

pred delete [f : File] {
	not (f in Trash) and
	Trash' = Trash + f and
	File' = File
}

pred restore [f:File] {
	f in Trash and
	Trash' = Trash - f
	File' = File
}

pred do_smth_else {
	File' = File
	Trash' = Trash
}

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

run example {}

run example {} for 5

run no_files {
	some File
	eventually no File
} for 5

assert restore_after_delete {
	always (all f : File | restore[f] implies once delete[f])
}

check restore_after_delete for 5 but 20 steps

assert delete_all {
	always ((Trash = File and empty) implies after always no File) 
}

check delete_all for 5 but 20 steps