Readme for executable models associated with "Benchmark: Nonlinear Reachability Analysis Benchmarks from Numerical Analysis"
ARCH Workshop 2015

There is a benchmark converter that uses Hyst (more details: http://verivital.com/hyst/ ) to convert SX benchmarks into the input formats of other hybrid systems reachability tools. This is in the root directory as Hyst.jar and has its own readme called README_HYST.txt. For brevity, Hyst may be executed on the Chemical Akzo problem described in the paper to convert from SX to the dReach format using:

java -jar Hyst.jar -v -d Chemical_Akzo\Chemical_Akzo.xml Chemical_Akzo\Chemical_Akzo.cfg -o Chemical_Akzo\Chemical_Akzo_hyst.drh

To convert all the examples, execute from a console in the root directory: python hyst_all_benchmarks.py

The input SX files follow the naming convention: benchmarkname.xml for the XML and benchmarkname.cfg, where these files are in each of the benchmark directories (e.g., Chemical_Akzo\Chemical_Akzo.xml and Chemical_Akzo\Chemical_Akzo.cfg); refer to the file hyst_all_benchmarks.py to see all the names.

To convert from SX to the MathWorks Simulink/Stateflow (SLSF) model, execute in Matlab (from the subfolder sx2slsf):

SpaceExToStateflow('Chemical_Akzo.xml', 'Chemical_Akzo.cfg', '--folder', 'Chemical_Akzo')

To convert all the examples, execute: sx2slsf\sx2slsf_all_benchmarks.m

For completeness, two versions of Hyst are included, Hyst.jar is the latest version, while some earlier experiments conducted on this test set used a previous version (Hyst-1.13.jar). To execute the old version, just use java -jar Hyst-1.13.jar instead of java -jar Hyst.jar.

Each benchmark's executable model files (in the SX and other formats already converted) and results appears in an appropriately named subfolder, for example, the Chemical Akzo problem is in the folder \Chemical_Akzo.

To reproduce our results, the easiest way for most users is probably to execute the Simulink/Stateflow models, which are included in each benchmark's folder as, e.g., Chemical_Akzo.mdl for the Chemical Akzo problem.

Hyst by default cannot create SLSF models, but relies on some additional Matlab scripts to call the SLSF APIs to generate the SLSF models, as discussed above. More details on this are available in the README_HYST_SX2SLSF.txt here: 

http://swt.informatik.uni-freiburg.de/tool/spaceex/ha2slsf

