This function defines an invariant condition that will hold true before and after all transitions.
The message added to exception
A boolean expression applied to the context