Maude-help mailing list

[Rainer Mann <rainer.mann.rm AT gmx.de>]

Great! Thanks, Francisco!

Best,
Rainer

On 12.02.19 12:15, Paco Durán wrote:
> 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