Maude-help mailing list

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

On Friday 01 April 2005 08:10, Zhijiang Dong wrote:
> Dear Maude users and developpers:
>
> I have a question about model checker. Is it possible to put a
> fairness constraint during model checking?
>
> I have two loops in my system. The property fails because the system
> always executs one loop, and ignore the other.

There is no built in notion of fairness or justice in the model checker but 
some things can be encoded in LTL. For example if your property is P and e1 
is true iff your first loop is starting to execute and e2 is true iff your 
second loop is starting to execute you could check the following formula:

([]<> e1 /\ []<> e2) -> P

Steven