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 is described in this paper to appear at HSCC 2015:

http://www.taylortjohnson.com/research/bak2015hscc.pdf

Hyst takes model files specified as hybrid automata in the SpaceEx XML format and converts to other representations, while attempting to preserve semantics (which differ across tools). Hyst currently supports transformation to dReach, Flow*, HyCreate, and through some additional Matlab scripts, MathWorks Simulink/Stateflow models (particularly continuous-time Stateflow charts).

Hyst also supports a variety of model transformation passes (optimizing passes to improve results while maintaining equivalence, e.g., like sound abstractions, but some of these are really just syntactic sugar to improve analysis results in some tools). For details on one of these, see the paper on pseudo-invariants: http://stanleybak.com/files/research/cyphy2014/bak_cyphy2014_paper.pdf

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


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)

Example:
java -jar Hyst.jar -v -d Chemical_Akzo\Chemical_Akzo.xml Chemical_Akzo\Chemical
_Akzo.cfg -o Chemical_Akzo\Chemical_Akzo_hyst.drh

OutputType:
	-f1.2 Flow* format
	-f1.2.2b Flow* format
	-d dReach format
	-h HyCreate2 format
	-hsim HyCreate2 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)
