Maude-help mailing list

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

On Wednesday 02 June 2010 01:40:54 am Vladimir Klebanov wrote:
> On Tue, Jun 1, 2010 at 9:13 PM, Steven Eker 
> <eker AT csl.sri.com>
>  wrote:
> > Fresh names are not functional so are not available in the functional
> > fragment of Maude. They are available via rule rewriting by using mod
> > COUNTER which can be imported multiple times with renaming if multiple
> > counters are needed.
> 
> Thanks. I got some helpful hints on and off the list. Too bad that
> COUNTER does not work with search.

The decision not to support counters in search was intended to avoid trivial 
nontermination cases and also to avoid the issue of whether uniqueness should 
be guaranteed between branches (in which case one branch can affect others by 
using a value). In model checking counters are clearly a disaster but in 
breath-first search perhaps some reasonable semantics could be found.

Steven