Hi Liviu, On Wed, Sep 16, 2009 at 2:23 AM, Ciortea Liviu <liviu.ciortea at epfl.ch> wrote: > I noticed that the internal forks are not considered in the seeding scheme.
I'm not sure what you mean by this. When a state forks, the set of seeds that state is following is split, regardless of whether the fork is internal or not. > This means, among other things, that there is not a one-to-one mapping > between a seed and a single state in the execution tree. This is always true, when execution starts there all the seeds are associated with a single state. As that state forks it the set of seeds it is associated with shrinks. > I am implementing a similar replay mechanism, based on seeding. However, in > my case I need to make sure I include the internal forks as well. Is there > any side-effect of removing the condition for the fork to be internal when > seeding? Also, since in internal forks the solver is called, would this be > deterministic? I don't understand this. Are you perhaps talking about the replayPath functionality, not the seeding functionality? - Daniel
