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

Re: [PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand*



Ben,

Try
(defstep expand-grind-reveal (expand-list reveal-name)
  (then
   (expand* expand-list)
   (grind)
   (reveal reveal-name)
  )
"Expands, grinds, and reveals"
"Expanding '~a', grinding, and revealing")



-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 11/17/15 3:44 PM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
on behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

>Hi all,
>
>
>I’m trying to better understand how to create more complex strategies in
>PVS. To that end, I have the following strategy:
>(defstep expand-grind-reveal (expand-list reveal-name)
>  (then
>   (apply 'expand* expand-list)
>   (expand)
>   (reveal reveal-name)
>  )
> 
>"Expands, grinds, and reveals"
> 
>"Expanding '~a', grinding, and revealing")
>
>
>
>However, when I run this, the
>expand* strategy is definitely not running. If I try the
>apply step by itself:
>(apply 'expand* (“function_a” “function_b” “function_b2”))
>
>I get the following result:
>Ill-formed rule/strategy: expand*
>
>
>
>Can anyone give me advice on what I might be doing wrong?
>
>Best Regards,
>Ben Hocking
>ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>
>
>
>
>
>