Trash Can

The goal of this challenge is to design a simple file trash can, such that a deleted file can still be restored if the trash is not emptied.

Consider the following partial model of this design:

// delete a file
pred delete[f : File] { 
  f not in Trash
  Trash' = Trash + f File' = File
}
// restore a file
pred restore[f : File] { ... } 
// empty the trash
pred empty { ... }
// do nothing
pred do_nothing {
  Trash' = Trash
  File' = File 
}

fact behavior { 
  // initial state
  no Trash
  // transitions
  always (
    (some f: File | delete[f] or restore[f]) or empty or do_nothing
  )
}

assert restoreAfterDelete {
  // Every restored file was once deleted
  always (all f : File | restore[f] implies once delete[f])
}
assert deleteAll {
  // If the trash contains all files and is emptied
  // then no files will ever exist afterwards
  always ((File in Trash and empty) implies always no File)
}