[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Specifying Garbage Collection


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! 

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f45bc661-6f64-43e0-872a-5cbd29670d5d%40googlegroups.com.