RE: mantis 4144

I agree with Dave that the LRM is not intended for training. It is enough if it fully specifies the rules. I don't think we want to go overboard with explanatory examples.

However, I do have my own nitpick with the proposed text. It takes the statement "There are 2**33 possible combinations of {s, d}" and replaces that number with "1+2**32". But the original statement is actually true. There are 2**33 combinations of {s, d}. There are only 1+2**32 combinations where the constraint c is true. That needs to be specified with the change in number.

-----Original Message-----
From: owner-sv-xc@eda.org [mailto:owner-sv-xc@eda.org] On Behalf Of Rich, Dave
Sent: Friday, July 13, 2012 5:24 PM
To: Kaiming Ho; sv-xc@eda.org
Subject: RE: mantis 4144

OK, I'll see what I can do before the next round of voting. The LRM is not supposed to be a user's guide, and we could get into a deep hole trying to explain how constraint probabilities work.
________________________________________
From: owner-sv-xc@eda.org [owner-sv-xc@eda.org] on behalf of Kaiming Ho [kaiming.ho@iis.fraunhofer.de]
Sent: Wednesday, July 11, 2012 12:24 AM
To: Rich, Dave; sv-xc@eda.org
Subject: mantis 4144

Hello Dave:

   I've looked at your proposed change to 18.5.10 in mantis 4144.
The example illustrates subtleties in the way the constraint solver
works which are still misunderstood by many people. Including a
table of valid solutions, and their probability of occurrence in the
LRM would be educational. One finds this approach in training slides
or papers outlining SV 'gotchas'.

   Please consider adding the following after the first paragraph.

| The following table illustrates the valid solutions of {s,d} which
| satisfy the constraint, and the probability of occurrence of each
| s d prob
| 1 0x00000000 1/(1+2^32)
| 0 0x00000000 1/(1+2^32)
| 0 0x00000001 1/(1+2^32)
| 0 0x00000002 1/(1+2^32)
| 0 ...
| 0 0xfffffffe 1/(1+2^32)
| 0 0xffffffff 1/(1+2^32)

   In place of the entire second paragraph, I'd like to suggest something
like:

| In this case, the order constraint instructs the solver to solve for s
| before solving for d. Adding this order constraint does not change
| the set of valid solutions, but alters their probability of
| occurrence.
| s d prob
| 1 0x00000000 1/2
| 0 0x00000000 1/2 * 1/2^32
| 0 0x00000001 1/2 * 1/2^32
| 0 0x00000002 1/2 * 1/2^32
| 0 ...
| 0 0xfffffffe 1/2 * 1/2^32
| 0 0xffffffff 1/2 * 1/2^32
|
| Note that the probability that d==0 without the order constraint
| is 2/(1+2^32), and is 1/2*(1+2^32) with the order constraint.

regards,
kaiming
Received on Sat Jul 14 17:04:10 2012