DRAFT, 23-NOV-2003

This file describes the combined LRM changes for the following proposals:

   clock_flow.txt
   generalized_implication.txt	  
   negated_boolean.txt
   property_conjunction.txt
   property_disjunction.txt
   property_if_else.txt
   property_instances.txt
   property_negation.txt

The straw poll showed substantial support for all of these proposals.

These proposals all involve properties, so many of their changes
affect the same places in the LRM.  The combined effect of these
changes is simpler to digest than all of the individual changes and
conditional instructions for which changes apply under various
balloting outcomes.  In many cases, it is easy to see which parts
of the changes are associated with the individual proposals.


PROPOSED COMBINED CHANGES TO THE BNF:
-------------------------------------

1. p. 168, Box 17-12.  Change

      property_expr ::=                              
         ... 
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 

   to 

      property_expr ::=                              
         ...
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr

2. p. 168, Box 17-12.  Change

      multi_clock_property_expr ::= 
         ... 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence

   to

      multi_clock_property_expr ::=                     
         ...
         | multi_clock_sequence |=> multi_clock_property_expr

3. p. 176, Box 17-14.  Change

      property_expr ::=                              
           sequence_expr
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 
         | (property_expr)

   to 

      property_expr ::=                              
           sequence_expr
         | (property_expr)
         | not property_expr
         | property_expr or property_expr
         | property_expr and property_expr
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr
         | if (expression) property_expr [ else property_expr ]
         | property_instance

4. p. 176, Box 17-14.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | multi_clock_sequence |-> multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | if (expression) multi_clock_property_expr 
           [ else multi_clock_property_expr ]
         | clocking_event property_expr
         | property_instance

5. p. 177, Box 17-15.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | multi_clock_sequence |-> multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | if (expression) multi_clock_property_expr 
           [ else multi_clock_property_expr ]
         | clocking_event property_expr
         | property_instance

6. p. 279.  Change

      assert_property_statement ::= 
           assert property ( property_spec ) action_block 
         | assert property ( property_instance ) action_block

   to

      assert_property_statement ::= 
           assert property ( property_spec ) action_block 

7. p. 279.  Change

      cover_property_statement ::= 
           cover property ( property_spec ) action_block 
         | cover property ( property_instance ) action_block

   to

      cover_property_statement ::= 
           cover property ( property_spec ) action_block 

8. p. 280.  Change

      property_spec ::= 
           [ clocking_event ] [ disable iff ] ( expression ) [ not ] property_expr 
         | [ disable iff ( expression ) ] [ not ] multi_clock_property_expr

   to 

      property_spec ::= 
           [ clocking_event ] [ disable iff ( expression ) ] property_expr 
         | [ disable iff ( expression ) ] multi_clock_property_expr

9. p. 280.  Change

      property_expr ::=                              
           sequence_expr
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 
         | (property_expr)

   to 

      property_expr ::=                              
           sequence_expr
         | (property_expr)
         | not property_expr
         | property_expr or property_expr
         | property_expr and property_expr
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr
         | if (expression) property_expr [ else property_expr ]
         | property_instance

10. p. 280.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | multi_clock_sequence |-> multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | if (expression) multi_clock_property_expr 
           [ else multi_clock_property_expr ]
         | clocking_event property_expr
         | property_instance



PROPOSED COMBINED CHANGES TO LRM TEXT:
--------------------------------------


1. p. 168, first line of 17.7.11.  Change

      monitor sequences based on satisfying some criteria

   to 

      monitor properties based on satisfying some criteria


2. p. 168, first paragraph after box 17-12.  Change

      This clause is used to precondition monitoring of a sequence
      expression and is allowed at the property level. The result of
      the implication is either true or false. The left-hand side
      operand sequence_expr is called anteced-ent, while the
      right-hand side operand sequence_expr is called consequent.

   to 

      This clause is used to precondition monitoring of a property
      expression and is allowed at the property level. The result of
      the implication is either true or false. The left-hand side
      operand sequence_expr is called the antecedent, while the
      right-hand side operand property_expr is called the consequent.


3. pp. 168-169, second paragraph after box 17-12.  Change

      The following points should be noted for |-> implication:   
      
      -- antecedent sequence_expr can result in multiple successful
         sequences.
      
      -- If there is no match of the antecedent sequence_expr,
         implication succeeds vacuously by returning true.

      -- For each successful match of antecedent sequence_expr,
         consequent sequence_expr is separately evalu-ated, beginning
         at the end point of the match. That is, the end point of
         matching sequence from antecedent sequence_expr overlaps with
         start point of the consequent sequence_expr.
      
      -- All matches of antecedent sequence_expr must satisfy
         consequent sequence_expr. The satisfaction of the consequent
         sequence_expr means that there is at least one match of the
         sequence_expr.
      
      -- Nesting of implication is not allowed.

   to

      The following points should be noted for |-> implication:   
      
      -- From a given start point, the antecedent sequence_expr can 
         have zero, one, or more than one successful match.
      
      -- If there is no match of the antecedent sequence_expr from a
         given start point, then evaluation of the implication from
         that start point succeeds vacuous and returns true.

      -- For each successful match of the antecedent sequence_expr,
         the consequent property_expr is separately evaluated.  The
         end point of the match of the antecedent sequence_expr is the
         start point of the evaluation of the consequent
         property_expr.
      
      -- From a given start point, evaluation of the implication
         succeeds and returns true iff for every match of the
         antecedent sequence_expr beginning at the start point, the
         evaluation of the consequent property_expr beginning at the
         endpoint of the match succeeds and returns true.


4. p. 169, paragraph starting at line 7.  Change

      Two forms of implication are provided: overlapped using operator |->,
      and non-overlapped using operator |=>. For overlapped implication, if
      there is a match for the antecedent sequence_expr, then the first
      element of the consequent sequence_expr is evaluated on the same clock
      tick. For non-overlapped implication, the first element of the
      consequent sequence_expr is evaluated on the next clock
      tick. Therefore:
      
         sequence_expr |=> [not] sequence_expr
      
      is equivalent to:
      
         sequence_expr ##1 `true |-> [not] sequence_expr
 
      If not is used on the consequent, the result of consequent
      sequence_expr is reversed.

      The use of implication when multi-clock sequences are involved
      is explained in Section 17.11.

   to 

      Two forms of implication are provided: overlapped using operator |->,
      and non-overlapped using operator |=>. For overlapped implication, if
      there is a match for the antecedent sequence_expr, then the end point
      of the match is the start point of the evaluation of the consequent 
      property_expr.  For non-overlapped implication, the start point of 
      the the evaluation of the consequent property_expr is the clock tick
      after the end point of the match.  Therefore:
      
         sequence_expr |=> property_expr
      
      is equivalent to:
      
         sequence_expr ##1 `true |-> property_expr
      
      The use of implication when multi-clock sequences and properties are 
      involved is explained in Section 17.11.


5. p. 170, paragraph after figure 17-14, line 3.  Change
 
      before continuing to match those sequences

   to

      before evaluating their consequent properties


6. p. 170, paragraph after figure 17-14, line 4.  Change

      by removing the precondition for the sequence

   to 

      by removing the precondition for the consequent 


7. p. 171, after example p16.  Add

      This property can be coded alternatively as a nested 
      implication:

         property p16_nested;
            (write_en & data_valid) |->
               (write_en && (retire_address[0:4]==addr)) [*2] |-> 
                  ##[3:8] write_en && !data_valid && (write_address[0:4]==addr);
         endproperty


8. p. 176, paragraphs after box 17-14.  Change

      The result of property evaluation is either true or false. There are
      two kinds of property: sequence, and implication. If the property is
      just a sequence, the result of a sequence for every evaluation attempt
      is true or false. This is accomplished by implicitly transforming
      sequence_expr to first_match(sequence_expr). That is, as soon as a
      match of sequence_expr is determined, the result is considered to be
      true, and no other matches are required for that evaluation
      attempt. However, if the property is an implication, then the
      semantics of implication determine whether the property is true or
      false.

      The disable iff clause allows asynchronous resets to be specified. For
      a particular attempt, if the expres-sion of the disable iff becomes
      true at any time during the evaluation of the attempt, then the
      attempt for the property is considered to be a success. Other attempts
      are not affected by the evaluation of the expression for an
      attempt. 
      
      The not clause states that the property_expr associated with the
      property must never evaluate to true. Effectively, it negates
      property_expr. For each attempt, property_expr results in either true
      or false, based on whether there is a match for the sequence. The not
      clause reverses the result of property_expr. It should be noted that
      there is no complementation or any form of negation for the sequence
      in property_expr.

   to

      The result of property evaluation is either true or false. There are
      seven kinds of property: sequence, negation, disjunction, conjunction,
      if-else, implication, and instantiation.

      1. A property that is a sequence evaluates to true if and only if
         there is a match of the sequence.  Since there is a match if and
         only if there is a first match, evaluation of such a property is
         the same as implicitly transforming its sequence_expr to
         first_match(sequence_expr).  As soon as a match of sequence_expr
         is determined, the evaluation of the property is considered to
         be true, and no other matches are required for that evaluation
         attempt.
   
      2. A property is a negation if it has the form 
   
            not property_expr
   
         For each evaluation attempt of the property, there is an
         evaluation attempt of property_expr.  The keyword not states
         that the evaluation of the property returns the opposite of the
         evaluation of the underlying property_expr.  Thus, if
         property_expr evaluates to true, then not property_expr
         evaluates to false, and if property_expr evaluates to false,
         then not property_expr evaluates to true.
   
      3. A property is a disjunction if it has the form 
   
             property_expr1 or property_expr2
   
         The property evaluates to true if and only if at least one of 
         property_expr1 and property_expr2 evaluates to true.
   
      4. A property is a conjunction if it has the form 
   
             property_expr1 and property_expr2
   
         The property evaluates to true if and only if both
         property_expr1 and property_expr2 evaluate to true.
   
      5. A property is an if-else if it has either the form
   
             if (expression) property_expr1
   
         or the form
   
             if (expression) property_expr1 else property_expr2 
   
         A property of the first form evaluates to true if and only if
         either expression evalues to false or property_expr1 evaluates
         to true.  A property of the second form evaluates to true if and
         only if either expression evaluates to true and property_expr1
         evaluates to true or expression evaluates to false and
         property_expr2 evaluates to true.
   
      6. A property is an implication if it has either the form
   
             sequence_expr |-> property_expr
   
         or the form
   
             sequence_expr |=> property_expr
   
         The meaning of implications has already been discussed in 17.7.11.
   
      7. An instance of a defined property can be used as a property_expr or
         property_spec.  In general, the instance is legal provided the body 
         property_spec of the defined property can be substituted in place of 
         the instance, with actual arguments substitited for formal arguments, 
         and result in a legal property_expr or property_spec, ignoring local 
         variable declarations.  Thus, for example, if an instance of a defined 
         property is used as a property_expr operand for any property-building 
         operator, then the defined property must not have a disable iff clause.
         Similarly, clock events in a defined property must conform to the 
         rules of multiple clock support when the property is instantiated in 
         a property_expr or property_spec that also involves other clock events.         

      A disable iff clause can be attached to a property_expr to yield
      a property_spec

         disable iff (expression) property_expr

      The expression of the disable iff is called the reset
      expression.  The disable iff clause allows asynchronous resets
      to be specified.  For an evaluation of the property_spec, there
      is an evaluation of the underlying property_expr.  If during
      that evaluation the reset expression becomes true, then the
      overall evaluation of the property_spec is true.  Otherwise, the
      evalution of the property_spec is the same as that of the
      property_expr.  The reset expression is tested independently for
      different evaluation attempts of the property_spec.  Nesting of
      disable iff clauses, explicitly or through property
      instantiations, is not allowed.


9. p. 177, after line 8.  Add the following examples illustrating the new
   property forms:

         property rule3;
            @(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
         endproperty

      Property rule3 says that if a holds and a also held last cycle,
      then either c must hold at some point 1 to three cycles after
      the current cycle, or, if d holds in the current cycle, then
      then e must hold one cycle later.

         property rule4;
            @(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
         endproperty

      Property rule4 says that if a holds and a also held last cycle,
      then c must hold at some point 1 to three cycles after the
      current cycle, and if d holds in the current cycle, then then e
      must hold one cycle later.

         property rule5;
            @(posedge clk) 
            a ##1 first_match(b || c) |-> 
               if (b) 
                  ##1 d |-> e
               else // c
                  f ;
         endproperty

      Property rule5 has a followed by the first match of either b or
      c as its antecedent.  The consequent uses if-else to split cases
      on which of b or c is matched first.

         property rule6(x,y);
            ##1 x |-> y;
         endproperty
         property rule5a;
            @(posedge clk) 
            a ##1 first_match(b || c) |-> 
               if (b) 
                  rule6(d,e)
               else // c
                  f ;
         endproperty

      Property rule5a is equivalent to rule5, but it uses an instance
      of rule6 as a property expression.

10. pp. 177-178, beginning after box 17-15.  Change

      Two cases are allowed:

      1) Concatenation of two sequences, where each sequence can have
         a different clock

      2) The antecedent of an implication on one clock, while the 
         consequent is on another clock

      The multi-clock concatenation operator ## synchronizes between
      the two clocks.
      
         @(posedge clk0) sig0 ## @(posedge clk1) sig1
      
      When signal sig0 matches at clock clk, ## moves the time to the
      nearest clock tick of clk1 after the match. At the first clock
      tick of clk1, it matches sig1. If the two clocks, clk0 and clk1,
      are identical, then the above sequence is equivalent to:
      
         @(posedge clk0) sig0 ##1 sig1
      
      For two sequences, such as
      
         @(posedge clk0) s0 ## @(posedge clk1) s1
      
      For every match of s0 at clock clk0, ## moves the time to the
      first clock tick of clk1. From that first tick of clk1, s1 is
      matched.
      
      Multi-clock implication is only allowed with the non-overlapping
      implication. The semantics are similar to the sequence
      concatenation with ##. Whenever there is a match of the
      antecedent sequence, time is advanced to the nearest clock tick
      of the clock of the consequent sequence. The consequent is then
      evaluated for satisfaction.

   to

      In a multiply-clocked sequence or property, the scope of a
      clocking event flows from left to right until replaced by a new
      clocking event.  The only operators after which a new clocking
      event can be defined are the multi-clock concatenation operator
      ## and the non-overlapped implication operator |=>.  

      If the clocking event is changed after the multi-clock
      concatenation operator ##, then it synchronizes between the two
      clocks.  For example, consider
      
         @(posedge clk0) sig0 ## @(posedge clk1) sig1
      
      When signal sig0 matches at clock clk0, ## moves the time to the
      nearest clock tick of clk1 strictly after the match. At the
      first clock tick of clk1, it matches sig1. If the two clocks,
      clk0 and clk1, are identical, then the above sequence is
      equivalent to:
      
         @(posedge clk0) sig0 ##1 sig1
      
      More generally, consider
      
         @(posedge clk0) s0 ## @(posedge clk1) s1

      where s0, s1 are sequences without clocking events.  A match 
      of this multiply-clocked sequence begins with a match of 
      s0 under clock clk0, after which ## moves the time to the first
      clock tick of clk1 strictly after the endpoint of the match.
      Then, starting from that first tick of clk1, there is a match
      of s1 under clk1.

      When using the multi-clock concatenation operator ##, both 
      operands are required to admit only non-empty matches.  This 
      ensures that the synchronization across ## is between a single
      pair of clock events.  For example,

         @(posedge clk0) sig0 ## @(posedge clk1) sig1[*0:1] ## @(posedge clk2) sig2

      is illegal because the possibilty of an empty match of
      sig1[*0:1] makes ambiguous whether the second ## transition is
      from clk0 to clk2 or from clk1 to clk2.

      With this restriction, any multiply-clocked sequence has 
      well-defined starting and ending clock events.


      As in the case of singly-clocked properties, the result of
      evaluating a multi-clock property is either true or false.  The
      meanings of negation, disjunction, conjunction, and property
      instantiation are the same for multi-clock properties as they
      are for singly-clocked properties, with the exception that the
      underlying property expressions can be multiply clocked.

      The multi-clock property features that require special 
      attention are:

      1) Non-overlapped implication with multiply-clocked antecedent and 
         consequent.

      2) Overlapped implication with multiply-clocked antecedent and  
         consequent.

      3) if-else with multiply-clocked then and else clause properties.

      The behaviors of these constructs depend on the notion of the
      leading clock event(s) for a multiply-clocked sequence or
      property.  A clock event is a leading for a multiply-clocked
      property if some subproperty begins with that clock event.  For
      example, the multiply-clocked property

         @(posedge clk0) sig0 ## @(posedge clk1) sig1

      has posedge clk0 as its unique leading clock event.  On the
      other hand, the multiply-clocked property
      
         (@(posedge clk0) sig0 |=> a) and (@(posedge clk1) sig1 |=> b)

      has both posedge clk0 and posedge clk1 as leading clock events.

      1) Multiply-clocked non-overlapped implication is not
         restricted.  The semantics is similar to that of
         singly-clocked non-overlapped implication.  Starting at the
         point at which the implication is being evaluated, for each
         match of the antecedent sequence, time is advanced from the
         end point of the match to the nearest strictly future tick of
         any leading clock of the consequent property, and evaluation
         of the consequent property starting at that point is required
         to return true.
      
      2) Multiply-clocked overlapped implication is allowed only if
         there is a unique leading clock event of the consequent
         property and it is equal to the ending clock event of the
         antecedent sequence.  If so, then the semantics is similar to
         that of singly-clocked overlapped implication.  Starting at
         the point at which the implication is being evaluated, for
         each match of the antecedent sequence, evaluation of the
         consequent property starting at the endpoint of the match is
         required to return true.

      3) Multiply-clocked if-else is allowed only if the then clause
         property and, if present, the else clause property has unique
         leading clock event equal to the clock event for the if
         condition.  If this restriction is met, then the semantics of
            
            if (b) p1

         is the same as the semantics of 
 
            b |-> p1
   
         and the semantics of 

            if (b) p1 else p2

         is the same as the semantics of 
    
            (b |-> p1) and (!b |-> p2)

         The restriction is not met, for example, in 
 
            @(posedge clk0) if (b) c else @(posedge clk1) d
   
         because the if condition b is clocked at posedge clk0, 
         while the else clause has leading clock event posedge clk1.
         The following variant is legal and makes syntactically 
         clear that the event posedge clk1 at which d is evaluated
         is strictly after the posedge clk0 at which b is evaluated:

            @(posedge clk0) if (b) c else (1 |=> @(posedge clk1) d)

11. p. 178, end of 17.11.  Add the following examples:

      7) property using clock flow and overlapped implication:

            property mult_p7;
               @(posedge clk) a ##1 b |-> c ## @(posedge clk1) d;
            endproperty

         Here, a, b, and c are clocked at posedge clk.

      8) property using clock flow and if-else:

            property mult_p8;
               @(posedge clk) a ##1 b |-> 
                  if (c) 
                     1 |=> @(posedge clk1) d 
                  else 
                     e ## @(posedge clk2) f ;
            endproperty

         Here, a, b, c, and e are clocked at posedge clk.



PROPOSED COMBINED CHANGES TO THE FORMAL SEMANTICS:
--------------------------------------------------

1. p. 344, G.2.1.  Change the abstract grammar for unclocked properties 
   from

      P ::= [disable iff ( b )] [not] R                // "sequence" form 
         | [disable iff ( b )] [not] ( R |-> [not] R ) // "implication" form
   
   to 
   
      P ::= R                    // "sequence" form
   	 | (P)                   // "parenthesis" form
   	 | not P                 // "negation" form
   	 | (P or P)              // "or" form
   	 | (P and P)             // "and" form
   	 | (R |-> P)             // "implication" form
   	 | disable iff (b) P     // "reset" form
   
2. p. 344, G.2.1.  Change the abstract grammar for clocked properties from

      Q ::= @(b) P                                   // "clock" form 
   	 | [disable iff ( b )] [not] S               // "sequence" form 
   	 | [disable iff ( b )] [not] (S |-> [not] S) // "implication" form

   to 

      Q ::= @(b) P               // "clock" form
   	 | S                     // "sequence" form
   	 | (Q)                   // "parenthesis" form
   	 | not Q                 // "negation" form
   	 | (Q or Q)              // "or" form
   	 | (Q and Q)             // "and" form
   	 | (S |-> Q)             // "implication" form
   	 | disable iff (b) Q     // "reset" form

3. p. 344, G.2.2.  Delete 

      * \phi is an unclocked property fragment provided 
        disable iff (b) \phi is an unclocked property. 
   
      * N is a negation specifier if N is either the empty token or not.

   Delete also 
  
      \phi denotes an unclocked property fragment; N, N_1 , N_2 denote 
      negation specifiers;

4. p. 345, G.2.3.1.  Change

      * ( R_1 |=> N R_2 ) \equiv (( R_1 ##1 1 ) |-> N R_2 ) . 

   to 
   
      * (R |=> P) \equiv ((R ##1 1) |-> P).

   Change

      * ( S_1 |=> N S_2 ) ((S_1 ## @(1) 1 ) |-> N S_2 ) .

   to 

      * (S |=> Q) \equiv ((S ## @(1) 1) |-> Q).


5. p. 346, G.3.1.  Change

      * @(c) (R) ---> (@(c) R).

   to

      * @(c) (P) ---> (@(c) P).

6. p. 347, G.3.1.  Change

      * @(c) disable iff (b) \phi ---> disable iff (b) @(c) \phi.

   to

      * @(c) disable iff (b) P ---> disable iff (b) @(c) P.

7. p. 347, G.3.1.  Delete

      * @(c) not b ---> @(c) !b.

8. p. 347, G.3.1.  Change

      * @(c) not R ---> not @(c) R, provided R is not a boolean expression

   to 

      * @(c) not P ---> not @(c) P
   
9. p. 347, G.3.1.  Change

      * @(c) N_1 ( R_1 |-> N_2 R_2 ) \equiv N_1 ( @(c) R_1 |-> @(c) N_2 R_2 ) .

   to

      * @(c) (R |-> P) ---> (@(c) R |-> @(c) P).

10. p. 347, G.3.1.  Add

      * @(c) (P1 or P2) ---> (@(c) P1 or @(c) P2).

      * @(c) (P1 and P2) ---> (@(c) P1 and @(c) P2).


11. p. 348, Neutral satisfaction of properties.  Add

      * w |= (P) iff  w |= P.

12. p. 348, Neutral satisfaction of properties.  Change

      * w |= disable iff (b) \phi iff either w |= \phi or there 
        exists 0 <= k < |w| such that w^k |= b and 
        w^{0,k-1}\top^\omega |= \phi.  Here, w^{0,-1} denotes the 
        empty word.
   to

      * w |= disable iff (b) P iff either w |= P or there exists 
        0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega |= P.  
        Here, w^{0,-1} denotes the empty word.

13. p. 348, Neutral satisfaction of properties.  Change

      * w |= not \phi iff not({\bar w} |= \phi).

   to

      * w |= not P iff not(\bar w |= P).


14. p. 348, Neutral satisfaction of properties.  Change

      * w |= (R_1 |-> N R_2) iff for every 0 <= j < |w| such that 
        {\bar w}^{0,j} |== R_1, w^{j..} |=  N R_2 . 

   to 

      * w |= (R |-> P) iff for all 0 <= j < |w| such that 
        {\bar w}^{0,j} |== R, w^{j..} |= P.

15. p. 348, Neutral satisfaction of properties.  Add

      * w |= (P1 or P2) iff w |= P1 or w |= P2.

      * w |= (P1 and P2) iff w |= P1 and w |= P2.

16. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= disable iff (b) \phi iff either w,L0 |= \phi or there exists 
      	0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega,L0 |= \phi.  
      	Here, w^{0,-1} denotes the empty word.

   to

      * w,L0 |= disable iff (b) P iff either w,L0 |= P or there exists 
      	0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega,L0 |= P.  
      	Here, w^{0,-1} denotes the empty word.

17. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= not \phi iff not(\bar w,L0 |= \phi).

   to
      
      * w,L0 |= not P iff not(\bar w,L0 |= P).

18. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= (R_1 |-> N R_2) iff for all 0 <= j < |w| and L1 such that 
      	{\bar w}^{0,j},L0,L1 |== R_1, w^{j..},L1 |= N R_2.
      
   to
      
      * w,L0 |= (R |-> P) iff for all 0 <= j < |w| and L1 such that 
      	{\bar w}^{0,j},L0,L1 |== R, w^{j..},L1 |= P.

19. p. 351, Neutral satisfaction of properties (with local variables).
   Add

      * w,L0 |= (P) iff  w,L0 |= P.
   
      * w,L0 |= (P1 or P2) iff w,L0 |= P1 or w,L0 |= P2.

      * w,L0 |= (P1 and P2) iff w,L0 |= P1 and w,L0 |= P2.

