maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] model checking problem

From: Zhijiang Dong <zdong01 AT gmail.com>
To: maude-help AT maude.cs.uiuc.edu
Subject: [Maude-help] model checking problem
Date: Fri, 1 Apr 2005 11:10:35 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type:content-transfer-encoding; b=JLd4jJsPRWUJZx/t0WN8SOpwkT7P6EzZYTWMitx8P2c6aZ2TdzdafgBrBQ66lkU4TXelFxRD5NRLKb9knnBYz3jae93ZqupiS+VNBIe4vV47zrCzTpaX/Iv1laAzUp0LM8ee03fvzjx/+vackICvhh2K7Azn7wT447I8mM/V0LE=
List-archive: <http://maude.cs.uiuc.edu/pipermail/maude-help>
List-id: Maude help list <maude-help.maude.cs.uiuc.edu>

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.

Thanks.

Zhijiang

[Maude-help] model checking problem, Zhijiang Dong, 04/01/2005
- Re: [Maude-help] model checking problem, Steven Eker, 04/01/2005