RE: [sv-ac] ballot on 1466

Coming to the conclusion that there is a thread proliferation is not
trivial. I also disagree that 'users are already aware of this problem'
is sufficient. The understanding of many users about assertions is very
basic. A theoretical understanding that this can occur is one thing.
Applying it in practice is quite another. It is quite common for users
to write code with thread proliferation problems without realizing it.

Shalom

> By observing the tool performance and output.
> 
> User's are already aware of this sort of problem,
> since it is a common mistake to create thread
> proliferation due to redundancy, e.g. by writing
> 
>    assert property (a[*1:$] |-> b);
> 
> instead of
> 
>    assert property (a |-> b);
> 
> >
> > How would you expect that a user will notice the thread
> proliferation?
> >
> > > Regarding the argument about dropping a digit and
> > > accidentally writing [*] instead of [*2], I think
> > > that, from a user's perspective, it is much more
> > > likely that this will be caught quickly due to
> > > the thread proliferation
> > =20
> > Thanks,
> > Shalom

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