Add Token Elimination abstraction

[NicEastvillage]

Token Elimination is an abstraction that removes tokens from a marking based on possible, visible, directional effects while preserving reachability properties.

• The dynamic variant uses the structure of the net and the current marking to find the relevant effects for the given reachability query and then removes irrelevant tokens in accordance.
• The static variant does not take the current marking into account and will due to caching often be much faster on repeated invocations involving the same reachability queries but is overall less effective.

The abstraction provided through token elimination is similar to that of structural reduction rule I+M as well as stubborn reductions. However, it can additionally be used on-the-fly in state space searches to simplify states and thus reduce the size of the state space.

Token elimination can as off this PR be used in the Certain Zero CTL engine and the standard reachability search. By default, Token Elimination is off, but it can be activated with the flags --token-elim-ctl <t> and --token-elim-reach <t> where <t> is either dynamic or static. It is not recommended to use --token-elim-reach when structural reductions (rule I+M) and stubborn reductions are enabled, due to their similar effect for reachability queries.

Token Elimination is based on the work in 'Token Elimination in Model Checking of Petri Nets' (TACAS'25) by Nicolaj Ø. Jensen, Kim G. Larsen, and Jiri Srba.