Maude-help mailing list

[Musab AlTurki <alturki AT uiuc.edu>]

Title: random and counter question - Maude Alpha86a

Hi,

I'm using the 'random' and 'counter' ops defined in the RANDOM and COUNTER modules (of Maude Alpha86a), resp. I'm using them to generate a pseudo-random number in a standard way (similar to how 'rand' is defined in PMaude).

The problem I have is that once I use my pseudo-random number, I can no longer use Maude's search tool to explore the states of the system. I read in Maude's release notes that 'counter' is inert to searching (but not to rew and frew) so I should expect such behavior. So, my question: How can I use these ops to generate a pseudo-random number such that I can still use the search tool to explore states? Is this even possible? Or is it that another tool is used to explore the states?

Musab