• Ticc
• BugClosed
• Simulation: Incomplete State

Simulation: Incomplete State

• Submitted by: Bo Adler and Vishwa Raman
• Date: 11-Dec-2005
• Assigned to: Vishwa

• Fixed. Simulation testing in progress.

The simulate function takes an argument which specifies the set of possible start states. Internally, mdd_pick_one_minterm is called to pick a specific starting state, but it doesn't seem to pick an assignment for local variables. It also seems to give incomplete assignments to range variables.

In the attached printer example, I specify a state set of not busy for the initial states, and the simulate function selects

(
 (user = 2)(
   (busy = 0)(
     (size = 8)
      +
     (size = 9)) ) )

as the start state. There are two problems with this start state:

1. the 'size' variable has two values assigned to it.
2. The variables 'User1.s' and 'User2.s' do not have any specific assignments.

Luca suggested on Friday that for range variables, we might need to conjoin the restrictions on the range.

Discussion

Luca says the following.

1. The first problem is due to the following: we get a cube in the bdd, not in the mdd. The choice between 8 or 9 corresponds to leaving the LSB unspecified. This might well be: perhaps both of those values are appropriate, and the LSB is simply not part of the bdd branch. So, there is no "bug" in what we implemented. Rather, the mistake is that we compute a cube in the bdd, rather than in the mdd. This is not a particularly easy problem to fix. I propose the following:

   1. Before we get a cube, we conjoin the given bdd/mdd with the bdd/mdd which specifies that each variable is in the correct range. The bdd could be the encoding of: x < 5 & y < 10 & z < 4, for instance.

   2. Once this is done, we modify the function that picks a cube, so that it picks a complete cube, one that assigns a value to every bit.

2. This is not a bug. A cube per se does not give values to all the variables. In any case, if we implement the above outlined fix to the first problem, this second problem will also go away.

Vishwa says the following.

Please remove this comment after you have had a chance to verify what I say. As of yesterday simulation is not the way it used to be but it does the randomization over rules instead. With this change things work better. The issue of multiple values of size still exists and it seems to come into play only when the rule delta_env is picked.

If you look at the implementation of mdd_pick_one_minterm, it does something along what Luca suggests. I haven't studied the code in detail, but it gets the onval bdd's corresponding to each MDD variable and conjoins them. It then conjoins the given MDD with this conjunction before calling bdd_bdd_pick_one_minterm_random.

• This is good. Then, all you need to do is to ensure that each bit gets a value - even bits that are skipped in the BDD. There should be a way to do this. -Luca

The problem earlier was that we were overapproximating the next state by considering all possible rules. Hence, it may well be that User1.s/User2.s may have been assigned 1 by one rule and 0 by another, turning it into a don't care. I haven't verified this yet, but since we were overapproximating, this seems very plausible.

• No, this is not the way don't cares are generated. Don't cares are generated when a variable does not appear in the branch of a BDD leading from the root to a leaf. -Luca

I do agree that maybe we can change mdd_pick_one_minterm to pick a complete minterm, that is one that is a complete assignment over all the variables.

• Yes, this is what I think we need to do. -Luca

Thanks.