Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

The reason counter's special rewriting semantics are disabled in search and 
model checking is that otherwise any occurence of counter would result in an 
infinite state space.

You can always simulate counter by carrying an extra value around in your 
term 
and giving a rule that increments it - but this still runs into the infinite 
state space problem.

I wonder just how compatible random numbers are with search anyway; they can 
be seen as two alternatives for dealing with non-determinism; pick a path at 
random (don't care non-determinism) and follow all paths (don't know 
non-determinism).

Steven

On Wednesday 13 July 2005 13:39, Musab AlTurki wrote:
> 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