Re: [PVS-Help] Finding Variables

["Cesar A. Munoz" <munoz@nianet.org>]

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