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

Stanley Bak, (stanleybak [at] gmail.com) 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.

If you run into any issues, please don't hesitate to contact the authors. If you want to add support for your reachability or falsification tool, please don't hesitate to contact the authors.


GUI USAGE:

Hyst can be run through a GUI or using the command line. To use the GUI, after building Hyst.jar simply run it as an executable .jar file with no arguments. Additionally, depending on your OS you may be able to just double click the icon to run the GUI (on Linux you must set it as executable).

$ java -jar Hyst.jar


CHECKING COMMAND-LINE USAGE: 

You can run it as an executable .jar file with the -help flag to see command-line usage (no GUI):

$ java -jar Hyst.jar -help

This will show you the Hyst version as well as the flags for the various printers and transformation passes. Run the tool with -verbose or -debug is there is any trouble converting to try to get more insight into the Error.


CONVERTING AN EXAMPLE: 

To convert from a SpaceEx model, you run Hyst, provide the proper flag for the format you want to output, and the path to the SpaceEx .xml and, if named differently the .cfg file. You can also provide an output filename with the -o flag (stdout will be used otherwise, which may be incompatible with model formats that require multiple files).

$ java -jar Hyst.jar -flowstar examples/toy/toy.xml

In this case -flowstar indicates we want a model in the Flow* format (see the usage above). The .cfg file will be assumed to be examples/toy/toy.cfg since it is not explicitly specified. Since no filename is given using the -o flag, the output will be printed to stdout.


HYCREATE2:

java -jar Hyst.jar examples/heaterLygeros/heaterLygeros.xml -hycreate -o heaterLygeros.hyc2

This will convert the heater/thermostat example described in the paper to the HyCreate2 format, and write the result to the file heaterLygeros.hyc2.

FLOW*:

java -jar Hyst.jar examples/heaterLygeros/heaterLygeros.xml -flowstar -o heaterLygeros.model

DREACH:

NOTE: dReach (as of this writing) requires files to have the extension .drh to execute.

java -jar Hyst.jar examples/heaterLygeros/heaterLygeros.xml -dreach -o heaterLygeros.drh

SPACEEX:

You may want to convert from a SpaceEx model back to SpaceEx to run some transformation passes or just to do flattening.

java -jar Hyst.jar examples/heaterLygeros/heaterLygeros.xml -spaceex -o heaterLygeros.drh


EXAMPLES AND RESULTS DIRECTORY:

Several examples have been included which can be converted in the examples directory. The result shows the result of converting the models and running them with the various tools using the default settings (not all tools complete on all models).

