This is supplementary material for the submission at
Applied Verification for Continuous and Hybrid Systems (ARCH) 2016 Workshop
Catgory: Benchmark Submission
Title: Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis (Benchmark Proposal)
Authors: Omar Ali Beg, Ali Davoudi, and Taylor T. Johnson

In this archive:
1) "examples" folder includes two benchmarks subfolders, i.e.:
  a. PLL (use pll.xml and pll_spaceex.cfg for reachability analysis)
  b. FWR (use fwr.xml and fwr_spaceex.cfg for reachability analysis)
2) "lib" folder contains an executable Jar file of Hyst
3) "src/matlab" includes all source codes for the Hyst translation tool

To run the Hyst tool for conversion from spaceex to slsf, do the following:

1) Open Matlab
2) Move to the folder where you extracted the files
3) Make "src/matlab" as current directory in Matlab
4) Run the following command (where you enter a meaningful relative path to your model):
	
  Example call for fwr: 	

     SpaceExToStateflow('..\..\beg_arch2016_benchmark\examples\fwr\fwr.xml')

  This produces a Stateflow model on following location (might take some seconds, especially when the

  Simulink libraries have not been loaded yet):
  
  ..\..\beg_arch2016_benchmark\src\matlab\output_slsf_models