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, and solve the exercises below, relying only on the temporal operators always, after and primes ':

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

• finish the model of, by defining predicates restore and empty