PHAVer v0.2.4 Release Notes
---------------------------

PHAVer is still in an early development stage. While we're trying to
improve the code and provide updates as soon as possible, the
following issues are still unresolved:

- The partitioning of the state space generates new locations that can
  currently not be mapped back to the original locations. E.g., if an
  automaton has a location "idle", any reference to this location
  after a reachability analysis with partitioning/refinement switched
  on will be empty. This prohibits the intersection of unpartitioned
  states with the set of reachable states.

- The partitioning only works for the command "reachable", not for
  "reachable_stop".

- The command "reachable_stop" only accepts as input a set of symbolic
  states, i.e., "reg=reachable_stop({idle & x==0, busy & x<=1});".

- The output of states currently has three forms:
  <name>.print;  -- List of states as inequalities.
  <name>.save_gen_fp(<filename>) -- Saves states as list of
  vertices in floating point numbers. For output with "graph".
  <name>.save_con_fp(<filename>) -- Saves states as list of
  constraints in floating point numbers. For further processing with
  floating point polyhedral tools.

- The documentation of the PHAVer language as well as the help
  produced by "phaver -h" is not up-to-date. Please refer to the
  examples for the current syntax.

We apologize for the inconvenience.