Readme for Distributable associated with "Benchmark Generator for Stratified Controllers of Tank Networks"
ARCH Workshop 2015



There are three parts associated with the distributable:

1. There is a suite of benchmarks in the SX (SpaceEx XML) format. This is in the benchmark-suite directory.

2. There is a benchmark generator script which was used to create these benchmarks from a description file. This is in the benchmark-generator directory.

3. There is a benchmark converter which uses Hyst to convert SX benchmarks into the input formats of other hybrid-systems reachability tools. This is in the benchmark-converter directory.


Each subdirectory has its own README with more specific instructions.


Results:

(1) Validation of network flattening in Hyst: 

the non-flattened model file:

\tank_benchmark_arch2015\benchmark-suite\samples\sample\sample.xml
\tank_benchmark_arch2015\benchmark-suite\samples\sample\sample.cfg

computes the same reachable states (using SpaceEx) as the flattened model (created with Hyst; number of discrete jumps in .cfg manually modified):

\tank_benchmark_arch2015\benchmark-converter\paper_images\sample\sample_flattened.xml
\tank_benchmark_arch2015\benchmark-converter\paper_images\sample\sample_flattened.cfg
