Draft LRM Changes for Parameterized And/Or

From: Dana Fisman <dana.fisman@gmail.com>
Date: Mon Dec 27 2004 - 02:05:45 PST

Erich, All,

Below is a list of suggested changes to the LRM in order to
incorporate Parameterized And/Or Sequences/Properties as per the
decisions in the last meeting.

1. Changes in the BNF (Appendix A):

The following productions should be added:

Parameter_Definition ::= /PSL/_Identifier [ Index_Range ] in
Value_Set Parameters_Definition ::= Parameter_Definition {
Parameter_Definition } Parameterized_Sequence::= 'for'
Parameters_Definition':' And_Or_SERE_OP '{' Compound_SERE '}'
Parameterized_Property ::= 'for' Parameters_Definition':'
And_Or_Property_OP '(' FL_Poperty ')'

And_Or_SERE_Op :: = '&&' | '&' | '|'
And_Or_Property_OP ::= AND_OP | OR_OP

Compound_SERE ::= Parameterized_Sequence
FL_Property ::= Parameterized_Property

2. Changes in the body of the LRM:

I. Two sections should be added:
a. A section describing parameterized sequences should
    be added between section 6.1.1.2 to 6.1.1.2.1.
b. A section describing parameterized properties should
    be added between section 6.2.1.7 to 6.2.1.7.1
Detailed changes follows.

II. To incorporate the relaxation decisions regarding the simple
subset, changes should be done in:
a. In the simple subset definition (Section 4.4.4)
b. In the sections of the Logical And/Or operators (Sections 6.2.1.7.3
and 6.2.1.7.4)
Note:
For OR I made the decision to phrase the restrictions as follows:
at most one operand can be non-boolean. This will give the result
that for a parameterized OR no operand can be non-temporal since
the syntax makes them all of the same type. This also gives for
the non-parameterized multiple OR (e.g. in A | B | C)
the result that only one can be non-Boolean.
(For AND we decided to remove the restriction all together. )
Details follows.

-------------------------------------

Parameterized Sequence

Introduction: The parameterizing operators, shown in Box xxx,
apply a given base operator to a set of compound SEREs obtained by
instantiating a base compound SERE once for each possible value or
combination of values of the given parameter(s).

Box: Compound_SERE ::= Parameterized_Sequence
Parameterized_Sequence::= 'for' Parameters_Definition':'
  And_Or_SERE_OP '{' Compound_SERE '}'
Parameters_Definition ::= Parameter_Definition {
Parameter_Definition } Parameter_Definition ::= /PSL/_Identifier [
Index_Range ] in Value_Set
  And_Or_SERE_Op :: = '&&' | '&' | '|'

Text following the box: The PSL Identifiers are the names of the
parameters. A PSL Identifier with an Index Range is an array. The
base operator can be either SERE or ('|'), SERE length-matching
and ('&&'), or SERE non-length matching and ('&'). The Compound
SERE enclosed in braces is the base compound SERE.

For each PSL Identifier, the Value Set defines the set of values
that the corresponding parameter or array elements can take on.

The set of values can be specified in three different ways - The
keyword boolean specifies the set of values {True, False}. - A
Value Range specifies the set of all values within the given
range. - The comma (,) between Value Ranges indicates the union of
the obtained sets.

For a single parameter, 1. If the parameter is not an array, and
the set of values has size K, then the obtained set is of size K.
Each element in the set is obtained by instantiating the base
compound SERE with one of the possible values in the set of
values. 2. If the parameter is an array of size N, and the set of
values has size K then the obtained set is of size K^N. Each
element in the set is obtained by instantiating the base compound
SERE with one of the combination of values that can be taken on by
the array.

For multiple parameters, the set of values is that obtained by
applying the above rules repeatedly, once for each parameter.

Restrictions:

The restrictions of the base operator apply to the resulting
Compound SERE as specified in the sections of the respective base
operator (Section 6.1.1.2.1 SERE or ('|'), Section 6.1.1.2.2 SERE
non-length-matching and ('&') and Section 6.1.1.2.3 SERE
length-matching and (&&).

For each parameter definition the following restrictions apply

- If the parameter name has an associated Index Range, the Index
Range shall be specified as a finite Range, each bound of the
Range shall be statically computable, and the left bound of the
Range shall be less than or equal to the right bound of the Range.

- If a Value is used to specify a Value Range, the Value shall be
statically computable.

- If a Range is used to specify a Value Range, the Range shall be
a finite Range, each bound of the Range shall be statically
computable, and the left bound of the Range shall be less than or
equal to the right bound of the Range.

- The parameter name shall be used in one or more expressions in
the Property, or as an actual parameter in the instantiation of a
parameterized SERE, so that each of the instances of the SERE
corresponds to a unique value of the parameter name.

Note— The parameter is considered to be statically computable, and
therefore the parameter names can be used in a static expression,
such as that required by a repetition count.

Informal semantics:

For Compound SERE A:

- for i in boolean: | {A(i)} is equivalent to the applying '|' to
the set containing the two Compound SEREs A(false) and A(true),
i.e. is equivalent to the Compound SERE {A(false)} | {A(true)}

- for i in {j:k}: && A(i) is equivalent to applying '&&' to the
set containing the k-j+1 Compound SEREs: A(j), A(j+1), ..., A(k),
i.e. is equivalent to the Compound SERE {A(j)} && {A(j+1)} && ...
&& {A(k)}

- for i in {j,l,k}: && A(i) is equivalent to applying '&&' to the
set containing the 3 Compound SEREs: A(j), A(l) and A(k), i.e. is
equivalent to the Compound SERE {A(j)} && {A(l)} && {A(k)}

- for i[0:1] in boolean: & A(i) is equivalent to applying '&' to
the set containing the 4 Compound SEREs: A({false,false}),
A({false,true}), A({true,false}) and A({true,true}), i.e. is
equivalent to the Compound SERE {A({false,false})} &
{A({false,true})}& {A({true,false})} & {A({true,true})}

- for i[0:2] in [c,d]: | A(i) is equivalent to applying '|' to
the set containing the 8 Compound SEREs: A({c,c,c}), A({c,c,d}),
A({c,d,c}), A({c,d,d}), A({d,c,c}), A({d,c,d}), A({d,d,c})and
A({d,d,d}), i.e. is equivalent to {A({c,c,c})} | {A({c,c,d})} | {
A({c,d,c})} | { A({c,d,d})} | {A({d,c,c})} | { A({d,c,d}) } |
{A({d,d,c})} | { A({d,d,d}) }

- for i in {j:k}, j in {m:n}: & A(i,j) is equivalent to applying
'&' to the set containing the (k-j+1)x(n-m+1) Compound SEREs:
A(j,m), A(j+1,m), ..., A(k,m),
A(j,m+1),A(j+1,m+1),....,A(k,m+1),....,A(j,n),A(j+1,n),....,A(k,n)
i.e. is equivalent to the Compound SERE {A(j,m)}& {A(j+1,m)} & ...
&{ A(k,m)}& { A(j,m+1)}& {A(j+1,m+1)}&
....&{A(k,m+1)}....{A(j,n)}& {A(j+1,n)}&....&{A(k,n)}

-------------------------------------

Parameterized Property

Introduction: The parameterizing operators, shown in Box xxx,
apply a given base operator to a set of FL Properties obtained by
instantiating a base FL Property once for each possible value or
combination of values of the given parameter(s).

Box: FL_Property ::= Parameterized_Property Parameterized_Property
::= 'for' Parameters_Definition':' And_Or_Property_OP '('
FL_Poperty ')' Parameters_Definition ::= Parameter_Definition {
Parameter_Definition } Parameter_Definition ::= /PSL/_Identifier [
Index_Range ] in Value_Set And_Or_Property_OP ::= AND_OP | OR_OP

Text following the box: The PSL Identifiers are the names of the
parameters. A PSL Identifier with an Index Range is an array. The
base operator can be either a logical and or a logical or. The FL
Property enclosed in parenthesis is the base FL Property.

For each PSL Identifier, the Value Set defines the set of values
that the corresponding parameter or array elements can take on.

The set of values can be specified in three different ways - The
keyword boolean specifies the set of values {True, False}. - A
Value Range specifies the set of all values within the given
range. - The comma (,) between Value Ranges indicates the union of
the obtained sets.

For a single parameter, 1. If the parameter is not an array, and
the set of values has size K, then the obtained set is of size K.
Each element in the set is obtained by instantiating the base
compound SERE with one of the possible values in the set of
values. 2. If the parameter is an array of size N, and the set of
values has size K then the obtained set is of size K^N. Each
element in the set is obtained by instantiating the base compound
SERE with one of the combination of values that can be taken on by
the array.

For multiple parameters, the set of values is that obtained by
applying the above rules repeatedly, once for each parameter.

Restrictions:

The restrictions of the base operator apply to the resulting FL
Property as specified in the sections of the respective base
operator (Section 6.2.1.7.3 Logical and and Section 6.2.1.7.4
Logical or). In particular, since for logical OR at most one
non-Boolean operand is allowed, applying the parameterizing
operator on or, requires the base FL_Property to be Boolean.

For each parameter definition the following restrictions apply

- If the parameter name has an associated Index Range, the Index
Range shall be specified as a finite Range, each bound of the
Range shall be statically computable, and the left bound of the
Range shall be less than or equal to the right bound of the Range.

- If a Value is used to specify a Value Range, the Value shall be
statically computable.

- If a Range is used to specify a Value Range, the Range shall be
a finite Range, each bound of the Range shall be statically
computable, and the left bound of the Range shall be less than or
equal to the right bound of the Range.

- The parameter name shall be used in one or more expressions in
the Property, or as an actual parameter in the instantiation of a
parameterized SERE, so that each of the instances of the SERE
corresponds to a unique value of the parameter name.

Note— The parameter is considered to be statically computable, and
therefore the parameter names can be used in a static expression,
such as that required by a repetition count.

Informal semantics:

For FL_Propoerty F:

- for i in boolean: || {F(i)} is equivalent to the applying '||'
to the set containing the two FL Properties F(false) and F(true),
i.e. is equivalent to the FL Property {F(false)} || {F(true)}

- for i in {j:k}: && F(i) is equivalent to applying '&&' to the
set containing the k-j+1 FL Properties: F(j), F(j+1), ..., F(k),
i.e. is equivalent to the FL Property {F(j)} && {F(j+1)} && ... &&
{F(k)}

- for i in {j,l,k}: && F(i) is equivalent to applying '&&' to the
set containing the 3 FL Properties: F(j), F(l) and F(k), i.e. is
equivalent to the FL Property {F(j)} && {F(l)} && {F(k)}

- for i[0:1] in boolean: && F(i) is equivalent to applying '&&' to
the set containing the 4 FL Properties: F({false,false}),
F({false,true}), F({true,false}) and F({true,true}), i.e. is
equivalent to the FL Property {F({false,false})} &&
{F({false,true})}&& {F({true,false})} && {F({true,true})}

- for i[0:2] in [c,d]: || F(i) is equivalent to applying '||' to
the set containing the 8 FL Properties: F({c,c,c}), F({c,c,d}),
F({c,d,c}), F({c,d,d}), F({d,c,c}), F({d,c,d}), F({d,d,c})and
F({d,d,d}), i.e. is equivalent to {F({c,c,c})} || {F({c,c,d})} ||
{ F({c,d,c})} || { F({c,d,d})} || {F({d,c,c})} || { F({d,c,d}) }
|| {F({d,d,c})} || { F({d,d,d}) }

- for i in {j:k}, j in {m:n}: && F(i,j) is equivalent to applying
'&' to the set containing the (k-j+1)x(n-m+1) FL Properties:
F(j,m), F(j+1,m), ..., F(k,m),
F(j,m+1),F(j+1,m+1),....,F(k,m+1),....,F(j,n),F(j+1,n),....,F(k,n)
i.e. is equivalent to the FL Property {F(j,m)}&& {F(j+1,m)} && ...
&{ F(k,m)}&& { F(j,m+1)}&& {F(j+1,m+1)}&&
....&{F(k,m+1)}....{F(j,n)}&& {F(j+1,n)}&....&{F(k,n)}

---------------------------------------
In Section 6.2.1.7.3 Logical and -
Change the restriction to:
   None
---------------------------------------
In Section 6.2.1.7.4 Logical or -
Change the restriction to:
Within the simple subset (see section 4.4.4), at most one operand
of a logical or property may be non-Boolean.
------------------------------------------
In Section 4.4.4 -
1. Remove the restriction on logical and
2. Change the restriction on logical or to:
     at most one operand of a logical or property may be non-Boolean.

Regards,
Dana.
Received on Mon Dec 27 02:05:54 2004

This archive was generated by hypermail 2.1.8 : Mon Dec 27 2004 - 02:05:55 PST