Maude-help mailing list

[Bartosz Zielinski <bartosz.zielinski AT uni.lodz.pl>]

Another possibility is to name constants true and false differently, e.g., tt and ff. Otherwise, the interpreter will not know

if false and true in eq not false = true  are constants of sort Boolean or Bool. Finally, one can disambiguate the sorts, i.e., write

(false).Boolean and (true).Boolean instead of false and true.

Bartosz Zielinski

---

Od: Steven Eker <eker AT csl.sri.com>
Wysłane: poniedziałek, 4 lutego 2019 22:33
Do: maude-help AT lists.cs.illinois.edu
Temat: Re: [[Maude-help] ] multiple distinct parses for statement

 

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&amp;data=01%7C01%7Ceker%40csl.sri.com%7Ce97760d09a30405a925d08d68ae65f5e%7C40779d3379c44626b8bf140c4d5e9075%7C1&amp;sdata=7sV3BC%2BXsxTGMX2aM2Upc57rr5qWiuAftXUj8w05qSM%3D&amp;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