[sv-ac] cover in procedural context

All:

I like Ed's idea about defining enabling conditions
to work as preconditions of followed_by for a cover property.

I'm not sure that there is clear language in the LRM
today that says that the enabling condition behaves like
the precondition of |-> for a cover property.

In Annex E, we said that for assert property, the enabling
condition behaves like the precondition of |->.

I agree with Ed that we already have "followed_by" in
the language.  I don't see the connection to the LTL operators.

I think that if people are writing implication properties,
they intend them to be checked as correctness properties
and they expect the tool also to collect coverage on how
thoroughly the correctness properties have been exercised.

I think that it will be confusing for users to tell them 
that when they write

  cover property (a |-> b)

they are getting the same thing as

  cover property (a ##0 b)

I agree with Dmitry that we still need to address the problem
of disable iff for covers.

Best regards,

John H.