Release of SpaceEx v0.9.5 with Simulator Scenario

SpaceEx has been extended with a basic simulator scenario. It computes trajectories for a given number of points in the set of initial states. Our current goal for the simulator is to assist with the modeling process, and to help users evaluate the difference between actual model behavior and the approximation produced by the reachability algorithms.

Currently still in its alpha version, the simulator has a number of limitations:

• It does not support nondeterminism in the differential equations. Nondeterministic inputs to the differential equations as well as transition assignments are ignored.
• It resolves nondeterminism in jumps by computing for each trajectory the first and the last point that can take the jump, plus one point at the time halfway between.
• Currently, it does not handle auxiliary (non-state) variables in the invariants or guards.

Further improvements and bug fixes for version 0.9.5:

• SpaceEx now parses a rudimentary subset of the CIF format. CIF files must be in the CIF ASCII format and have the file extension ".cif".
• The web interface has been updated and improved.
• Variables with const-dynamics (parameters) are now properly handled.
• Error messages in the parser have been improved.
• Error messages and warnings in case of empty or universe sets have been improved.
• bugfix: negation of arithmetic expressions led to wrong results