Clause: 17.11, 17.33.3, 29.4.3

Description

Currently, LRM mentions that if disable iff condition becomes true, the evaluation of property spec is true.

 

This makes it difficult for the users to identify the difference in match due to disable iff condition vs. match due to complete property evaluation. Therefore we propose to introduce another evaluation condition called “disabled”. This type of evaluation only occurrs when disable iff condition of the property becomes true.

Suggested Resolution

Clause 17.11, replace the following on page 267:

 

For an evaluation of the property_spec, there is an evaluation of the underlying

property_expr. If prior to the completion of that evaluation the reset expression becomes true, then the overall

evaluation of the property_spec is true.

 

By

 

For an evaluation of the property_spec, there is an evaluation of the underlying

property_expr. If prior to the completion of that evaluation the reset expression becomes true, then the overall evaluation

of the property results in disabled. A property has disabled evaluation if it was preempted due to disable iff condition. A disabled evaluation of a property does not result in success or failure.

 

 

Clause 29.4.3, change the following on page 482:

 

For any assertion, the number of attempts that have not

yet reached any conclusion (success or failure) can be derived from the formula:

in progress = attempts - (successes + vacuous success + disabled + failures)

The example below illustrates some of these queries:

 

Clause 28.3.2, Add the following:

 

cbAssertionSuccess

An assertion attempt reaches a success state.

cbAssertionVacuousSuccess

An assertion attempt reaches a vacuous success state.

cbAssertionDisabledEvaluation

An assertion attempt reaches a disabled state (e.g. as a result of disable iff condition becoming true).

 

Details:

a) In a failing transition, there shall always be at least one element in the expression array.

b) Placing a step callback results in the same callback function being invoked for both success and failure

steps.

c) The content of the cb_time field depends on the reason identified by the reason field, as follows:

— cbAssertionStart: cb_time is the time when the assertion attempt has been started.

— cbAssertionSuccess, cbAssertionVacuousSuccess, cbAssertionDisabledEvaluation and cbAssertionFailure: cb_time is the time when the assertion succeeded or failed.