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

Lists in strategies - without brackets?


I am working with PVS 2.4

I have a strategy defined with the following parameters:

(defstep split-rho-all (&optional (values nil)(split-up 1)(inst-into -)
(force? f) (remove-impl? t)(no-sub? f)(split-all -)(hide? t))

The first parameter, values, is a list of values, e.g. 
("i!1" "j!1" "z") etc. The other parameters are seldom used.

However, users often omit the brackets over the values e.g.

 (split-rho-all "i!1" "j!1") instead of
 (split-rho-all ("i!1" "j!1")) 

which results in a segmentation fault:

Error: Received signal number 11 (Segmentation violation)

Is there any way to make PVS see that "j!1" is part of the values list?

The other parameters are always preceded by the formal name (i.e.
:split-up) when used, and I am willing that they always must be.
Even willing to exclude them from the strategy if necessary.

I.e. is there any way to allow (split-rho-all "i!1" "j!1")
to be interpreted with values as ("i!1" "j!1")?
Or, even better, to allow the user to type 
(split-rho-all "i!1" "j!1" :hide? f) and still bind values as ("i!1"

Some inbuilt strategies allow lists to be given with or without brackets 
(e.g. hide). How can I do this?