[sv-champions] comments on 2069

Hi Dmitry:

From reviewing 2069 for Champions, I have the comments below.

J.H.

  . p. 2, Change "satisfied on each set trace" to "satisfied on each trace".
  . p. 2, Change "satisfied on at least one set trace" to "satisfied on at least 
    one trace".
  . p. 2.  The phrases 

       "trace that satisfies all the assumptions associated with the model" 

    and 
    
       "feasible trace" 

    have not been defined that I can see.  I guess that these are intended 
    to mean the same thing.  If so, I would change

       The following definitions describe assertion statement satisfaction on a
       set of traces:
       
       - assert property statement is satisfied on a set of traces if it is
         satisfied on each set trace that satisfies all the assumptions
         associated with the model.
       
       - assume property statement is satisfied on a set of traces if it is
         satisfied on each trace of the set.
       
       - cover property statement is satisfied on a set of traces if it is
         satisfied at least on one set trace satisfying all the assumptions
         associated with the model.
       
       An assertion statement holds globally if it is satisfied on the set of
       all feasible traces.

    to something like 

       Given a set of traces and a set of assumptions, the following definitions
       describe assertion statement satisfaction on the set of traces predicated
       on the set of assumptions:
       
       - A trace in the set of traces is _feasible_ if every assumption in the set 
         of assumptions is satisfied on the trace.

       - An assert property statement is satisfied on the set of traces predicated
         on the set of assumptions if it is satisfied on each feasible trace.
       
       - A cover property statement is satisfied on a set of traces predicated on
         the set of assumptions if it is satisfied on at least one feasible trace.
       
       An assertion statement holds globally on the set of traces predicated on
       the set of assumptions if it is satisfied on every feasible trace.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.