# HyLaGI

## Overview †

- HyLaGI is an implementation of HydLa.
- HyLaGI features
- error-free simulation
- symbolic execution
- automatic case analysis

## How to use HyLaGI †

- HyLaGI requires Mathematica (the latest version is recommended, at least above Mathematica 9.0)
- HyLaGI can be used if Mathematica can be located.
- That is, if Mathematica is invoked by the "math" command, HyLaGI will work.
- If a command name other than "math" is used, change the command name after the linkname in the "--mathlink" option.

- Please download HyLaGI from Download Page.
- Extract the downloaded archive to any place where you want to locate HyLaGI and change your current directory to it.
- Execute a HydLa program by typing the following command:
./hylagi <program_path> [<options>]

- For example, you can simulate examples/bouncing_particle.hydla (included by the HyLaGI archive) like below:
./hylagi examples/bouncing_particle.hydla -t 10 -p 20 --fnd

- "-t" stands for the time limit.
- "-p" stands for the number of phases to simulate.
- "--fnd" stands for the nondeterministic mode.
If you want to simulate only one case, you can remove this option.

(In fact, the option has no effect for this example program)

- For example, you can simulate examples/bouncing_particle.hydla (included by the HyLaGI archive) like below:

- If you want to know more options of HyLaGI, please type
./hylagi -h

## ASSERT statement †

- HyLaGI features bounded model checking of HydLa programs.
- We can specify the condition to be checked by adding a line of an $\texttt{ASSERT}$ statement to a HydLa program.
- An $\texttt{ASSERT}$ statement should be in the following form.
$\texttt{ASSERT}(condition).$

- The $condition$ part allows a constraint that is available as a guard, like $x = y$.

- An $\texttt{ASSERT}$ statement should be in the following form.

Last-modified: 2021-02-24 (Wed) 10:09:42 (244d)