This is Enea.

Home

Personal Info

Research

Papers

Teaching

About

PHAVerLitePHAVerLite

[Page last updated on "dicembre 04, 2020, 19:27:43".]

PHAVerLite's specification language

PHAVerLite inherits most of the 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.

  • 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).
© Enea Zaffanella
enea.zaffanella@unipr.it

| Home | Personal Info | Research | Papers | Teaching | About