# Re: [PVS-Help] Finding Variables

```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

```