HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models 
http://verivital.com/hyst/

Stanley Bak, http://stanleybak.com
Sergiy Bogomolov, http://swt.informatik.uni-freiburg.de/staff/bogom
Taylor T. Johnson, http://www.taylortjohnson.com/

Hyst has been tested on Windows and Linux using Java 1.7.


CHECKING USAGE: 

You can check the usage by running Hyst as an executable .jar file with the -help argument:

$ java -jar Hyst.jar -help
Hyst v1.17
Usage:
hyst [OutputType] (args) XMLFilename(s) (CFGFilename)

OutputType:
	-flowstar Flow* format
	-dreach dReach format
	-hycreate HyCreate2 format
	-hycreate_sim HyCreate2 format
	-qbmc Python QBMC (Testing) format
	-spaceex SpaceEx format
	-z SMT-LIB printer format
Optional Model Transformation Passes:
	-pass_pi Pseudo-Invariant at Point Pass [(modename|)pt1;inv_dir1|pt2;inv_dir2|...] (point/invariant direction is a comma-separated list of reals)
	-pass_pi_sim Pseudo-Invariant Simulation Pass [time1;time2;...]
	-pass_scale_time Scale Time Pass [multiplier;ignorevar]
	-pass_sub_constants Substitute Named Constants for Values Pass [no param]
	-pass_simplify Simplify Expressions Pass [no param]
	-pass_split_disjunctions Split Guards with Disjunctions [no param]
	-pass_remove_unsat Remove Unsatisfiable Modes Pass [no param]
	-shorten Shorten Mode Names Pass [no param]
	-regularize Regularization (eliminate zeno behaviors) Pass [<num jumps>;<delta>;<epsilon>]

-help show this command-line help text
-v Enable verbose printing
-debug Enable debug printing (even more verbose)
-novalidate skip internal model validation (may result in Exceptions being thrown)
-o [filename] output to the given filename
XMLFilename: The SpaceEx XML automaton to be processed (*.xml)






CONVERTING EXAMPLES: 

An example of converting the benchmark into different tools is included here in the example_minimal directory. This example can be converted using the -v flag to see output while the conversion is taking place.  When running the tools, they may require manual tweaking of the generated models. This is especially true for the tool parameters such as time step size and number of jumps (since these parameters are model specific). Lastly, the tools themselved may not be able to handle some of the aspects of the models, so you may need to reduce the time-bound, number of jumps, or otherwise adjust model parameters.

A custom version of Flow* was used to run the models, which is included in the flowstar1.2.2b-bak folder. This was due to a bug which restricted the lengths of the mode names to 100 characters.

To convert the minimal tank example to SpaceEx you can run:

java -jar Hyst.jar -v -s -o converted/minimalSpaceEx.xml example_minimal/minimal.xml

This produces the output files in the converted directory, which can then be run by SpaceEx (after slight changes to the configuration file, see the paper_images folder for the final model files). 


To get the output in Flow* format, do:

java -jar Hyst.jar -v -flowstar -o converted/minimalFlowstar.model example_minimal/minimal.xml

Again, the final model used in the paper has slight settings modifications (see the final models in the paper_images folder).


