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

Re: [PVS-Help] Finding Variables



Sorry, 
I forgot to say that I was assuming you have the Field package. 

Otherwise, if fnum is positive, use

(formula (car (select-seq (s-forms *goal*) fnum)))

instead of

(form (extra-get-formula fnum))

If fnum is negative, use 
(args1 (formula (car (select-seq (s-forms *goal*) fnum))))

Cesar


On Tue, 2005-04-19 at 14:46, Cesar A. Munoz wrote:
> Erika,
> 
> If I understood correctly, this strategy 
> 
> (defstrat if-store (&optional (fnum 1) (step1 (skip)) (step2 (skip)))
>   (let ((form (extra-get-formula fnum)))
>     (if (forall-expr? form)
> 	(let ((vars (remove-if-not
> 		     #'(lambda (v)
> 			 (and (type-name? (type v))
> 			      (equal (id (type v)) '|Store|)))
> 		     (bindings form)))
> 	      (varstr (format nil "Variables of type Store: ~a" vars)))
> 	  (if vars
> 	      (then (skip-msg varstr t)
> 		    step1)
> 	    step2))
>       (skip)))
> "Applies STEP1 if formula in FNUM is a quantifier over Store. Otherwise
>  applies STEP2"
> "Applying if-store to ~A"
> )
> 
> implements the functionality you need. 
> 
> Assuming:
> 
> test : THEORY
> BEGIN
> 
>   Store : TYPE
> 
>   s1,s2 : VAR Store
>   x1,x2 : VAR real
> 
>   store : LEMMA
>     forall(s1,x1,s2,x2):1=0
> 
> END test
> 
> then
> 
> store :  
> 
>   |-------
> {1}   FORALL (s1, x1, s2, x2): 1 = 0
> 
> Rule? (if-store 1 (skip-msg "YES" t) (skip-msg "NO" t))
> Variables of type Store: (s1 s2)
> No change on: (skip)
> store :  
> 
>   |-------
> [1]   FORALL (s1, x1, s2, x2): 1 = 0
> 
> YES
> No change on: (skip)
> 
> You probably have to modify the test "(equal (id (type v)) '|Store|)" as
> PVS supports sub-typing and, depending on your definition of Store, you
> may have to dig a little bit more on the structure of the expression.
> 
> In addition to the PVS reference manual, some papers in these
> proceedings may be useful if you are writing strategies:
> 
> http://techreports.larc.nasa.gov/ltrs/dublincore/2003/cp/NASA-2003-cp212448.html
> 
> 
> Hope that it helps,
> Cesar
> On Mon, 2005-04-18 at 18:19, Erika Rice wrote:
> > Hello,
> > 
> > I am writing a strategy and have found myself in the
> > following situation.  I have a store type and the guarantee
> > that variables of type store will always be quantified at
> > this point, and I want to do something like this
> > 
> >     (if <formula mentions variable with of type store>
> >         step1
> >         step2)
> > 
> > The challenge is the bit in angle brackets.  Is there a way
> > of determining whether or not a formula makes any mention
> > of a variable of a certain type?  
> > 
> > If that is too vague of a question, please give me
> > information about any of the following: comparing variable
> > types, peeling apart the structure of a formula, finding the
> > types of all quantified variables, or anything else that
> > seems vaguely related.
> > 
> > Thank you,
> > 
> >     Erika Rice
> >     University of Washington
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855