maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] Maude Strategy and Model Checking

From: hicheur awatef <a_hicheur AT yahoo.fr>
To: maude-help AT maude.cs.uiuc.edu
Subject: [Maude-help] Maude Strategy and Model Checking
Date: Wed, 14 May 2008 16:10:08 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=4SQZ0jDvKs8mj9AKwUWVRZEn7dEqjUcO5I7W8ge4kh+6bnILe5oIhuMG/PM4KsLublGFQZbLZU63kcTIZ++BdCZ4pxBY2l8VUWsPR0ghvKauPaTGDoRQVKByMTZuWuFLqOXbXZd4w+EC1UNWoyG5r6FLqtzJuCl4Aq0c86s0Otg=;
List-archive: <http://maude.cs.uiuc.edu/pipermail/maude-help>
List-id: Maude help list <maude-help.maude.cs.uiuc.edu>

Hi,

I'd like to know how can we use the Maude Model Checker in combination with a strategy: For example in the case of the strategy defined in Maude manual (for controlling the execution of the rules in the VENDING-MACHINE module example) where one want to buy the same number of apples and cakes, and buy as many as possible, with the coins already inserted.

How can we call the model checker of Maude on such a strategy to verify some property on the resulting states? In fact, I want to use the model checker in such a way to verify a property on a bounded number of states generated by a system module.

Thank you for your help

__________________________________________________
Do You Yahoo!?
En finir avec le spam? Yahoo! Mail vous offre la meilleure protection possible contre les messages non sollicités
http://mail.yahoo.fr Yahoo! Mail

[Maude-help] Maude Strategy and Model Checking, hicheur awatef, 05/11/2008
- <Possible follow-up(s)>
- [Maude-help] Maude Strategy and Model Checking, hicheur awatef, 05/14/2008
  - Re: [Maude-help] Maude Strategy and Model Checking, Steven Eker, 05/14/2008