Maude-help mailing list

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

Hi Marius,

Matching is not available on float numbers. They are not defined 
algebraically. 

You'll have to rely on conditions or predicates to check the sign or 
structure of your float numbers. 

Best,

Francisco Durán


> On 6 Nov 2018, at 12:32, Marius Storeide 
> <marius AT kikora.no>
>  wrote:
> 
> Using the match command, I try to match out negative floating on the 
> command line:
> 
> Maude> match -A:Float <=? -4.3 .
> match in CONVERSION : -A:Float <=? -4.2999999999999998 .
> Decision time: 0ms cpu (0ms real)
> 
> Solution 1
> -A:Float --> -4.2999999999999998
> 
> This does not work, as the '-' is considered part of the label. I encounter 
> the same problem when attempting the same in a module. This is intended as 
> a minimum example of such a case, it is not what I actually intend to do 
> with the floating-point number. Put another way: I can not solve my problem 
> with "abs(...)".
> 
> fmod TEST is
>     pr CONVERSION .
> 
>     eq [Absolute-number] :
>         -A:Float =
>         A:Float .
> endfm
> 
> Maude> in experiment.maude
> ==========================================
> fmod TEST
> Warning: "experiment.maude", line 4 (fmod TEST): variable A:Float is used 
> before it is bound in equation:
> eq -A:Float = A:Float [label Absolute-number] .
> 
> If I add a space between the '-' and 'A' (or any other label I give it), 
> the match fails, which means I'm no closer to my goal: 
> 
> Maude> match - A:Float <=? -4.3 .
> match in CONVERSION : - A:Float <=? -4.2999999999999998 .
> Decision time: 0ms cpu (0ms real)
> No match.
> 
> Is there any way to make this work, i.e. match out negative Floats? 
> 
> sincerely,
> Marius Storeide Kjelsvik

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