Section 14.3

LRM-137

Change (changes in red and blue):

The Observed region is for the evaluation of the property expressions when they are triggered. It is essential that the signals feeding and producing all the clocks to the property expressions have stabilized, so that the next state of the property expressions can be calculated deterministically. A criterion for this determinism is that the property evaluations must only occur once in any clock triggering time slot. During the property evaluation, pass/fail code shall be scheduled to be executed in the Reactive region of the current time slot.

LRM-137

Change (changes in red and blue):

Code specified in the program block, and pass/fail code from property expressions, are scheduled to occur in the Reactive region.

LRM-137

Change (changes in red and blue):

An explicit zero #0 delay (#0) requires that the process be suspended and an event scheduled into the Inactive region of the current time slot so that the process can be resumed in the next inactive to active iteration.