Maude-help mailing list

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

By default BOOL is included in every module since it provides things 
like the equality test _==_

It also defines true and false and several Boolean operators. If you 
want to define your own with the same names you can disable automatic 
inclusion of BOOL with the command:

set include BOOL off .

Steven

On 2/4/19 1:18 PM, Liu, Si wrote:
> I think it messed up with the built-in theory.
>
> Try:
>
> fmod BOOLEAN is
>     sort Boolean .
>     ops t f : -> Boolean [ctor] .
>     op not_ : Boolean -> Boolean [prec 53] .
>
>     eq not f = t .
>     eq not t = f .
> endfm
>
> On 2/4/19 3:12 PM, 
> rainer.mann.rm AT gmx.de
>  wrote:
> > I am leaning Maude from the book "Designing Reliable Distributed Systems" by
> > Peter Csaba Ölveczky, 
> > https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flink.springer.com%2Fbook%2F10.1007%2F978-1-4471-6687-0&data=01%7C01%7Ceker%40csl.sri.com%7Ce97760d09a30405a925d08d68ae65f5e%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=7sV3BC%2BXsxTGMX2aM2Upc57rr5qWiuAftXUj8w05qSM%3D&reserved=0
> >
> > I made a simple specification which is a simplification of an example provided
> > on page 15 of the book.
> >
> > fmod BOOLEAN is
> >     sort Boolean .
> >     ops true false : -> Boolean [ctor] .
> >     op not_ : Boolean -> Boolean [prec 53] .
> >
> >     eq not false = true .
> >     eq not true = false .
> > endfm
> >
> > Loading this example into maude, I received an error message:
> >
> > Warning: "boolean.maude", line 6 (fmod BOOLEAN): multiple distinct parses for
> > statement
> > eq not false = true .
> >
> > What's going on here?
> >
> > Thanks
> > Rainer