Work in progress (actually I just got back to this topic). The idea is
that we want to associate choice generator objects with each state that
has nondeterministic choices, i.e. delegate the enumeration of choice
values to dedicated objects. This would allow more than just the simple
integer interval that's currently kind of hard-wired into the Scheduler
(where it doesn't really belong). My favorite example for this are
random floating point values - quite obvious there is no complete
enumeration, but there are plenty of potential (application specific)
heuristics (e.g. a "threshold value" choice generator).
The Verify.randomDouble() is not functional yet, and the interface will
change.
-- Peter
On Jun 10, 2005, at 7:20 AM, Ladislav Prosek wrote:
> could anyone please explain what is the exact semantics of the
> Verify.randomDouble(String) method? The stub in Verify.java is not
> commented.
|