Maude-help mailing list

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

The model checker and the strategy language are two completely different 
algorithms for exploring the space of possible rewrites and cannot be used in 
combination.

The Maude team has discussed the possibility of model checking under various 
fixed strategies, such as various formulations of fairness or justice, 
however model checking under an arbitrary user defined strategy seems much 
harder to implement.

Steven

On Wednesday 14 May 2008 09:10, hicheur awatef wrote:
> 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