[Page last updated on "dicembre 04, 2020, 19:27:43".]
PHAVerLite's specification language
PHAVerLite inherits most of
specification language of PHAVer.
A few of the language commands and parameters of PHAVer are not supported;
also, a few parameters have been subject to renaming in an attempt
to somehow improve consistency.
Here is a brief summary of the main changes.
do, end, goto,
sync, wait are treated
as identifiers in PHAVerLite; hence, they can be used
as location names and/or syncronization label names
without causing a syntax error.
Parameter USE_CONVEX_HULL has been renamed to REACH_USE_CONVEX_HULL.
- Added parameter REACH_USE_CONSTRAINT_HULL.
Parameter CHEAP_CONTAIN_RETURN_OTHERS has been renamed to
- Added parameter REACH_CHEAP_CONTAINS_USE_BBOX.
Parameter ELAPSE_TIME has been renamed to REACH_USE_TIME_ELAPSE.
Parameter SEARCH_METHOD has been changed to only accept 3 values
(rather than the 8 values accepted by PHAVer):
- value 0: transaction based
(corresponding to value 0 in PHAVer);
- value 1: topological sort of all states
(corresponding to value 7 in PHAVer);
- value 2: topological sort of reachable states
(corresponding to value 6 in PHAVer);
this is the value used by default.
- Parameter REACH_ONLY_EXPLORE has been removed.
- Parameter REFINE_LOCATION_PLANE has been removed.
- All parameters related to simulation checking have been removed
(as simulation checking is no longer supported).