Group E - First Draft LRM Changes

The following changes to the Simple Subset definition address both Issue 13 (Group E) and the changes proposed as part of the parameterized and/or operator proposal. The changes are as follows:

 - restrict the operand f of next_e to be Boolean
     (because next_e[1:2](f) = next (f | next f), and one operand of | must be boolean)
 - restrict the operand f of next_event_e to be Boolean
     (because next_event_e(b)[1:2](f) = next_event(b) (f | next_event_e f), and one operand of | must be boolean)
 - remove the restriction on logical and
     (according to Dana's parameterized and/or proposal)
 - change the restriction on logical or to allow at most one operand to be non-Boolean
     (according to Dana's parameterized and/or proposal)

Specific changes:

In section 4.4.4, Simple Subset, change the list of restrictions and the final paragraph from the following:

- delete the following entry from the list:
    — The left-hand side operand of a logical and operator is a Boolean.

- change the following entry in the list:
    — The left-hand side operand of a logical or operator is a Boolean.
  to read as follows:
    — At most one operand of a logical or operator is non-Boolean.

- add the following entries to the list:
    — The operand of next_e* is Boolean.
    — The FL Property operand of next_event_e* is Boolean.

- change the last paragraph from:
    All other operators not mentioned above are supported in the simple subset
    without restriction. In particular, all of the next_event operators and all forms
    of suffix implication are supported in the simple subset.
  to read as follows:
    All other operators not mentioned above are supported in the simple subset
    without restriction. In particular, the operators always, next*, next_a*, next_event,
    next_event_a*, and all forms of suffix implication are supported without restriction
    in the simple subset.

The end result should read as follows:

    — The operand of a negation operator is a Boolean.
    — The operand of a never operator is a Boolean or a Sequence.
    — The operand of an eventually! operator is a Boolean or a Sequence.
    — At most one operand of a logical or operator is non-Boolean.
    — The left-hand side operand of a logical implication (->) operator is a Boolean.
    — Both operands of a logical iff (<->) operator are Boolean.
    — The right-hand side operand of a non-overlapping until* operator is a Boolean.
    — Both operands of an overlapping until* operator are Boolean.
    — Both operands of a before* operator are Boolean.
    — The operand of next_e* is Boolean.
    — The FL Property operand of next_event_e* is Boolean.

    All other operators not mentioned above are supported in the simple subset
    without restriction. In particular, the operators always, next*, next_a*, next_event,
    next_event_a*, and all forms of suffix implication are supported without restriction
    in the simple subset.
Received on Sat Jan 8 17:59:18 2005