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 in Electrum:

var sig File {}
var sig Trash in File {}

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

Solve the exercises below, relying only on first-order logic, set operators, and the temporal operators always, after, once and primes ':

1. finish the model by defining the predicates restore and empty
2. using the simulator, show that the same file can be perpetually deleted
3. specify and verify the following properties:
   1. the set of files never increases
   2. the set of files only changes when empty is performed
   3. if files are never deleted the trash can never be emptied
   4. restoring a file immediately after deleting it undos the operation
4. assume the existence of a special kind of files that are protected
   1. adapt the model so that this kind of files is supported
   2. adapt the operations accordingly
   3. use the simulator to show that if all files are protected, no deletions may occur
   4. specify and verify that, if there are protected files, some file will always exist