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

*To*: pvs-help@csl.sri.com*Subject*: about prove commands!*From*: Kun Wei <k.wei@eim.surrey.ac.uk>*Date*: Wed, 17 Sep 2003 14:27:06 +0100*Organization*: University of Surrey*Reply-To*: Kun Wei <k.wei@eim.surrey.ac.uk>*Sender*: pvs-help-owner@csl.sri.com

Hello, I got a big problem when I proved the following lemma. Because I don't know too much prover commands, who could give me any suggestions. That's so appreciated! hide_para.1.2 : [-1] P2!1(t1!3) [-2] P1!1(t1!2) [-3] t1!1 = leak(t1!2, X!1) [-4] t2!1 = leak(t1!3, X!1) {-5} prod(A!1)(leak(t1!2, X!1), leak(t1!3, X!1), x!1) [-6] disjoint?(A!1, X!1) |------- [1] EXISTS (t1_1: ({t: trace[E] | EXISTS (t1: (P1!1), t2: (P2!1)): prod(A!1)(t1, t2, t)})): x!1 = leak(t1_1, X!1) ==================================================== ps: Here prod is a function in which t is observed as a result if t1 and t2 can be executed concurrently by two processes which synchronise on A. Indeed, t,t1 and t2 are traces denoted as lists. prod(A)(t1, t2, t) : RECURSIVE bool = CASES t OF null : null?(t1) AND null?(t2), cons(x, y) : IF A(x) THEN cons?(t1) AND cons?(t2) AND car(t1) = x AND car(t2) = x AND prod(A)(cdr(t1), cdr(t2), y) ELSE (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y)) ENDIF ENDCASES MEASURE length(t) leak(t,A) is a function that gets rid of t's events included in set A for example: t: a->b->c-> Stop A:{a,b} leak(t,A)= c->Stop ok, let's go back the above question. In 1.2, I can't use inst? because I can't find a instance. Please suggest me some commands to make the prove carry on. Many thanks! Kun Wei

- Prev by Date:
**Re: PVS installation with redhat Linux 9** - Next by Date:
**Re: about prove commands!** - Prev by thread:
**PVS/Cygwin** - Next by thread:
**Re: about prove commands!** - Index(es):