PHAVerLite

PHAVerLite's specification language

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.

• PHAVer's keywords 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 REACH_CHEAP_CONTAINS.
• 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).