maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] model checking rules with rewrites in the condition

From: Roberto Vigo <rvig AT imm.dtu.dk>
To: "maude-help AT cs.uiuc.edu" <maude-help AT cs.uiuc.edu>
Subject: [Maude-help] model checking rules with rewrites in the condition
Date: Wed, 17 Oct 2012 13:53:02 +0200
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help/>
List-id: <maude-help.cs.uiuc.edu>
Organization: DTU

Dear Maude users,

in the Maude manual v2.6, sect. 9.2, it is written that model checking is supported only for rewrite theories in which the rules have purely equational conditions. As far as I understand, this means that I cannot model check a module where some rule conditions contain rewrites. Is that right? If so, do you know of any work for extending model checking support to conditional rules with rewrites in the condition?

Thanks for your time!

Best regards,
Roberto

[Maude-help] model checking rules with rewrites in the condition, Roberto Vigo, 10/17/2012