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

Question about strategies




Hello

I am a relatively new user of PVS.  I am trying to set
up a "metastrategy" that will apply a given strategy to
a bunch of subgoals, leaving me with only the subgoals
that the given strategy did not eliminate.  My best effort
is:

(defstep dosimp
	(simpcasestrat)
   (BRANCH (SMASH)
    ((TRY (TRY (simpcasestrat) (FAIL) (SKIP)) (SKIP) (SKIP))))
	"Dealing to easy cases"
	"Dealing to easy cases"
)

This sometimes does exactly what I want: I do not even see the subgoals
that are proved by the strategy (simpcasestrat), and for the
subgoals that are not handled by simpcasestrat, I just see
the unadulterated subgoal produced by the smash.

The above is not satisfactory because, depending on the
given strategy, it might fail to terminate (or just take
way too long - I'd rather inspect the subgoal manually in
this case to see if I can improve the strategy).  What I'd
really like is to say something like "try simpcasestrat and
if you don't quickly prove the subgoal, leave it to me".  

Is there some way to do this, or can someone suggest a better
overall method?

I'm also interested in pointers to papers that present detailed
examples of strategies, etc.  

Thanks a lot.

Cheers

Mark



______________________________________________________
Mark Moir                     Email: Mark.Moir@sun.com
Sun Microsystems Laboratories Phone: (781)442-3596
1 Network Drive UBUR02-311    Fax:   (781)442-1692
Burlington, MA 01803-0902
______________________________________________________