The current folder contains examples to discretize hybrid autoamta
(written in the input hydi form) and write the correspondent discrete
infinite-state transition system in SMV format (actually, in the input
  language of nuXmv, https://nuxmv.fbk.eu/)

README: this file.
global_time.cmd: run discretization using global time semantic
local_time.cmd: run discretization using global time semantic

Example to run the discretization:
../../hycomp -pre cpp -source global_time.cmd <hydi_file>

NOTE:
- The script writes the file tmp.smv in the current folder.
To change the file name just change the name passed to the -o argument
to the hycomp_write_global_fsm commmand in the global_time.cmd or the
 local_time.cmd files. 
- The output uses defines to use less space.
To have a readable output set the option 'daggifier_enabled "0"' in the cmd file.


REFERENCES
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction. EUROMICRO-SEAA 2011: 275-278
Sergio Mover, Verification of Hybrid Systems using Satisfiability Modulo Theories, PhD Thesis (https://es-static.fbk.eu/people/mover/paper/mover_phd_thesis.pdf)