[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com, cj@hermite.cs.uni-sb.de*Subject*: Model-Checking*From*: Christian Jacobi <cj@cs.uni-sb.de>*Date*: Wed, 7 Mar 2001 18:42:55 +0100*Sender*: pvs-help-owner@csl.sri.com

Hi, I've been playing with the PVS model-checker for some days, and now I've encountered a problem I cannot understand. I have defined a state type STATE, and a next-state relation N. I want to check the property AG AF p under the fairness constraint f. This is formalized as f(s: STATE) = (definition of f, not temporal) p(s: STATE) = (definition of p, not temporal) N(s1,s2: STATE) = (.....) lem: LEMMA FORALL s: AG(N, fairAF(N, p)(f))(s) I start the model-checker, which does not complete the proof (unfortunalty, the PVS modelchecker does not compute a counterexample). Now we change the fairness constraint to f':=AG AF f; this should not change anything (at least in my understeanding of fairness and temporal operators). f'(s: STATE) = AG(N, AF(N, f)) lem2: LEMMA FORALL s: AG(N, fairAF(N, p)(f'))(s) Surprisingly, lem2 can be proved by invoking the model-checker. Is this a bug in the model-checker, or is my understanding of fairness and temporal operators wrong? Thanks, Chris PS: if you need the actual files, just give me a note. -- ---------------------------------------------------------------- FB 14 - Informatik Christian Jacobi Im Stadtwald Computer Science Department D-66041 Saarbruecken Saarland University Germany Phone: (+49) 681 3024490 Fax: (+49) 681 3024290 ----------------------------------------------------------------

- Prev by Date:
**Re: what's the precise meaning of ...?** - Next by Date:
**Enumeration types** - Prev by thread:
**Re: Enumeration types** - Next by thread:
**what's the precise meaning of ...?** - Index(es):