SpaceEx State Space Explorer

SpaceEx v0.9.4 released, new features and bugfixes

This latest update fixes a number of known bugs and provides a few new features.

New Features

The following features have been added:

  • a new "Interval" output format shows the reachable intervals for all output variables, globally and for each reachable location,
  • user-definable template directions, superposition of several direction options (e.g., box plus uniform),
  • improved verbose output and error messages, including textual output of whether or not the forbidden states are reachable, and a hierarchical performance profile for debug verbosity levels,
  • the virtual machine server can be updated without downloading the new virtual machine as a whole,
  • binary command line executables are now available for certain versions of Linux and Mac OS X.

Defining User-Provided Template Directions

User-defined template directions are specified as a conjunction of linear constraints (like invariants or guards). The direction is the normal vector of the constraint (pointing to the outside). E.g., the three directions (x=1, y=-2, z=0), (x=0, y=0, z=1), (x=0, y=0, z=-1) are specified by the option

--directions "{ x-2*y<=1 & z==1 }"

(note the quotes and curly braces). The inhomogeneous term has no impact at the moment, but is reserved for future use. If more than one --directions options is given, the union of all provided directions is used. In the web interface, use the "additional options" field in the "Advanced" options tab.

Further enhancements and bugfixes

  • improved web interface for small screens, enlarged and resizable text boxes
  • now correctly handles transitions that have no labels (they do not synchronize with any other transition)
  • now correctly handles uncontrolled variables
  • now correctly parses floating point numbers in models (scientific notation)
  • fixed a bug in clustering that lead to erroneously empty sets
  • fixed a bug in the web interface that rejected output variables with an underscore character.