 Note that the formula \([A,e]G\) is vacuously true if the precondition \(\pre(e)\) of event e is false. Accordingly, the action model semantics retains the assumption of truthfulness that we had for public announcements. That is, for an event to actually occur, its precondition must be true. As a consequence, the occurrence of an event e implies that its precondition \(\pre(e)\) was true, and hence the occurrence of an event conveys its precondition formula as a message. If an event can occur at a given world, then we say that the event is executable at that world. 