 The following example combines liveness and safety properties of a single computation: “Whenever a state of alert is reached, the alarm is activated and remains activated until a safe state is eventually reached”. This property is expressible in LTL as