Trash

The goal of this challenge is to design a simple file trash, 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])
}

check restoreAfterDelete for 10 steps

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 after always no File)
}

check deleteAll

pred restoreEnabled[f : File] {
  // a file can be restored if it is in the trash
  f in Trash
}

assert restoreIsPossibleBeforeEmpty {
 // a deleted file can still be restored if the trash is not emptied
  always (all f:File | delete[f] implies (empty releases restoreEnabled[f]))
}

check restoreIsPossibleBeforeEmpty

1. Finish the model by defining the predicates restore and empty
2. Using the simulator and an empty run command, show that the following scenarios are possible:
   1. Starting with 3 files, delete all of them and empty the trash
   2. Starting with 1 file keep deleting and restoring it forever
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. Fix the specification of assertion restoreIsPossibleBeforeEmpty
5. Assume the existence of protected files
   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