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 no arguments:

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

OutputType:
	-f1.2 Flow* format
	-f1.2.2b Flow* format
	-d dReach format
	-h HyCreate2 format
	-hsim HyCreate2 format
	-qbmc Python QBMC (Testing) format
	-s SpaceEx format
Optional Model Transformation Passes:
	-pass_pi [(modename|)pt1;inv_dir1|pt2;inv_dir2|...] (point/invariant direction is a comma-separated list of reals) Pseudo-Invariant at Point Pass
	-pass_pi_sim [time1;time2;...] Pseudo-Invariant Simulation Pass
	-pass_time_scale [multiplier;ignorevar] Time Scale Pass
	-pass_sub_constants Substitute Constants
	-pass_simplify Simplify Expressions Pass
	-pass_split_disjunctions Split Guards with Disjunctions
	-pass_remove_unsat Remove Modes with (Simple) Unsatisfiable Invariants Pass
	-pass_merge_urgent Merge Urgent Modes Pass
	-shorten Shorten Mode Names Pass
	-regularize (<num jumps>;<delta>;<epsilon>) Regularization (eliminate zeno behaviors) Pass

-v Enable verbose printing
-debug Enable debug printing (even more verbose)
-p Output version of the model that produces a plot
-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)
CFGFilename: The automaton's config file. Will be derived from the XML filename if not explicitly stated (*.cfg)






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 -f1.2.2b -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).


