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:

// 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 the temporal operators always, after and primes ':

• finish the model of, by defining predicates restore and empty
• specify and verify the following properties:
  • the set of files never increases
  • the set of files only changes when empty is performed
  • 􏰊if files are never deleted the trash can never be emptied
  • restoring a file immediately after deleting undos the operation
• assume the existence of a special kind of files that are protected
  • adapt the model so that this kind of files is supported
  • adapt the operations accordingly
  • specify and verify that protected files never disappear