Hello,
I'm trying to model a Garbage Collector. I have a set of objects
and a predicate
Collectible(Objects, Object) ⟶ True
If the predicate Collectible yields True, the object may be collected by the Garbage Collector.
The safety property of the Garbage Collector shall state, that no object may ever be deleted by the Garbage Collector if the object is not collectible i.e. Collectible yields False.
The liveness property of the Garbage Collector shall state, that every object that is forever collectible i.e. Collectible yields True that object has to eventually be deleted by the Garbage Collector.
Objects can be deleted by other actors whether Collectible yields True or False. So the "origin" of a delete is relevant.
I am not sure how to specify this correctly. Should I introduce helper variables that record the actor, the action taken, and the object? Also, the liveness property is challenging: As soon as an object is deleted, that object is not collectible any more, it has already been collected, so the "forever collectible" seems hard to express.
Thanks for your help!