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.
