# Backup diff of HyLaGI vs current(No. 2)

- List of Backups
- View the diff.
- View the source.
- Go to HyLaGI.
- 1 (2015-01-21 (Wed) 07:35:17)
*2 (2017-03-02 (Thu) 03:21:30)*- 3 (2017-03-17 (Fri) 03:33:06)
- 4 (2017-03-18 (Sat) 00:34:37)

- The added line is THIS COLOR.
- The deleted line is THIS COLOR.

#author("2017-03-23T14:52:17+09:00","default:Uedalab","Uedalab") #mathjax * Overview [#v70ac10c] - HyLaGI is an implementation of HydLa. - HyLaGI features -- error-free simulation -- symbolic execution -- automatic case analysis * How to use HyLaGI [#xa82de43] +HyLaGI needs Mathematica (the latest version is recommended, at least above Mathematica 7.0) +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. +Type command like below, then you can simulate your HydLa program. +Execute a HydLa program by typing the following command: > ./hylagi <program_name> [<options>] ~ ./hylagi <program_path> [<options>] ~ < -- For example, you can simulate examples/bouncing_particle.hydla (included by the HyLaGI archive) like below. -- 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 --nd < -- "-t" stands for time limit. -- "-t" stands for the time limit. -- "-p" stands for the number of phases to simulate. -- "--nd" stands for nondeterministic mode. -- "--nd" stands for the nondeterministic mode. ~ If you want to simulate only one case, you can remove this option. ~ (In fact, this option has no effect for this example program) - If you want to know other options of HyLaGI, please type ~ (In fact, the option has no effect for this example program) - If you want to know more options of HyLaGI, please type > ./hylagi -h < * ASSERT statement [#g6769c02] - 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$.