Maude-help mailing list

[Paco Durán <duran AT lcc.uma.es>]

Hi Rainer, 

Even though the RANDOM module is in the prelude it is not the actual module 
when you start Maude. You can either select it or indicate so in the reduce 
command. 

Maude> red in RANDOM : random(0) .
reduce in RANDOM : random(0) .
rewrites: 1 in 0ms cpu (0ms real) (100000 rewrites/second)
result NzNat: 2357136044
Maude> red in RANDOM : random(1) .
reduce in RANDOM : random(1) .
rewrites: 1 in 0ms cpu (0ms real) (1000000 rewrites/second)
result NzNat: 2546248239
Maude> red in RANDOM : random(2) .
reduce in RANDOM : random(2) .
rewrites: 1 in 0ms cpu (0ms real) (1000000 rewrites/second)
result NzNat: 3071714933

Best,

Francisco


> On 12 Feb 2019, at 12:10, Rainer Mann 
> <rainer.mann.rm AT gmx.de>
>  wrote:
> 
> In prelude.maude the module RANDOM is defined
> 
> fmod RANDOM is
>   protecting NAT .
>   op random : Nat -> Nat
>       [special (id-hook RandomOpSymbol
>       op-hook succSymbol (s_ : Nat ~> NzNat))] .
> endfm
> 
> 
> However, when I try to use the operation random in maude, I get an error
> 
> $ maude.darwin64
>              \||||||||||||||||||/
>            --- Welcome to Maude ---
>              /||||||||||||||||||\
>        Maude 2.7.1 built: Jun 27 2016 16:43:23
>         Copyright 1997-2016 SRI International
>            Tue Feb 12 12:09:17 2019
> Maude> red random(0) .
> Warning: <standard input>, line 1: bad token random.
> Warning: <standard input>, line 1: no parse for term.
> Maude>
> 
> 
> Can anyone tell me what is wrong?
> 
> Thanks,
> Rainer

Attachment: smime.p7s
Description: S/MIME cryptographic signature