Refactor Entry / Exit event structs

[Baltoli]

These need to really have an associated function rather than just an arbitrary string description so that we can check them against a function object in the model-checking algorithm.