Skip to Content.
Sympa Menu

maude-help - [Maude-help] Using Builtins in maude confluence checker

maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] Using Builtins in maude confluence checker


Chronological Thread 
  • From: Pranav Garg <garg11 AT illinois.edu>
  • To: maude-help AT cs.uiuc.edu
  • Subject: [Maude-help] Using Builtins in maude confluence checker
  • Date: Sat, 17 Mar 2012 13:57:24 -0500
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
  • List-id: <maude-help.cs.uiuc.edu>

Hi,

The maude confluence checker does not support built-in types like BOOL. The owise attribute for equations which works in Maude also seems to not work in the confluence checker. The module I want to define in Maude has 2 conditional equations depending on if the variables I == J or I != J.

eq find ( I & L,I ) = yes .
ceq find ( I & L,J ) = find ( L,J ) if I =/= J .

How can I write the second equation in the maude confluence checker without including the built-in module BOOL ? I have tried the following variants and none of them work:
ceq find ( I & L,J ) = find ( L,J ) if I =/= J . --- after including BOOL
ceq find ( I & L,J ) = find ( L,J ) if (I = J) = false . --- with or without BOOL
eq find ( I & L,J ) = find ( L,J ) [owise] .


Thanks
Pranav



  • [Maude-help] Using Builtins in maude confluence checker, Pranav Garg, 03/17/2012

Archive powered by MHonArc 2.6.16.

Top of Page