HydLaWiki
HyLaGI
Start:
#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 requires Mathematica (the latest version is recom...
-- HyLaGI can be used if Mathematica can be located.
-- That is, if Mathematica is invoked by the "math" comma...
--- If a command name other than "math" is used, change t...
+Please download HyLaGI from [[Download]] Page.
+Extract the downloaded archive to any place where you wa...
+Execute a HydLa program by typing the following command:
>
./hylagi <program_path> [<options>] ~
<
-- For example, you can simulate examples/bouncing_partic...
>
./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...
~ (In fact, the option has no effect for this example p...
- 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 ...
-- An $\texttt{ASSERT}$ statement should be in the follow...
>
$\texttt{ASSERT}(condition).$
<
-- The $condition$ part allows a constraint that is avail...
End:
#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 requires Mathematica (the latest version is recom...
-- HyLaGI can be used if Mathematica can be located.
-- That is, if Mathematica is invoked by the "math" comma...
--- If a command name other than "math" is used, change t...
+Please download HyLaGI from [[Download]] Page.
+Extract the downloaded archive to any place where you wa...
+Execute a HydLa program by typing the following command:
>
./hylagi <program_path> [<options>] ~
<
-- For example, you can simulate examples/bouncing_partic...
>
./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...
~ (In fact, the option has no effect for this example p...
- 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 ...
-- An $\texttt{ASSERT}$ statement should be in the follow...
>
$\texttt{ASSERT}(condition).$
<
-- The $condition$ part allows a constraint that is avail...
Page:
