[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)
[condition type: SYNCHRONOUS-OPERATING-SYSTEM-SIGNAL]
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?