- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* Hyrose [#v70ac10c]
- Hyrose is the implementation of HydLa.
- Hyrose can simulate Hybrid Systems without calculation error by using the formula manipulation.
- Hyrose can simulate systems with symbolic parameters and uncertainties.
- Hyrose can search for all solutions trajectories using non-deterministic execution.
- Hyrose can perform bounded model checking.
* How to install Hyrose [#xa82de43]
After downloading Hyrose from [[Download]] Page, you should prepare a formula manipulation system and read the section "How to use the formula manipulation".
* How to use Hyrose [#a488d397]
- You input the HydLa program into Hyrose, you can get the result of simulation.
- You can get the result of simulation in the form of standard output or JSON.
- The name of JSON result is "<program>.hydat".
** Options [#yaa98c5a]
- If you want to know what kinds of option is in Hyrose, you perform Hyrose as following.
- "hyrose -h[--help]"
* How to use formula manipulation systems [#q42613e6]
- Hyrose uses Mathematica or REDUCE for constraint solving.
- To use them, please follow the instructions below and specify the software by the solver option.
** Mahtematica [#ta181443]
- Hyrose requires version 7 or up. Version 8 is recommended.
-- We have seen models that can be solved only with Mathematica 8. (2011/12/21)
- Hyrose can be used if Mathematica can be located.
-- That is, if Mathematica is invoked by the "math" command, Hyrose will work.
#author("2021-02-24T19:09:42+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 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.
--- HIDE allows you to specify the Mathematica execution file also.
** Reduce [#s36d2ad9]
- Hyrose requires Version 20101007; later versions will not work.
- In order to use REDUCE as a constraint solver, proceed as follows:
+ Installing REDUCE
-- Windows
--- Download the source code (reduce-windows64-20101007.zip OR reduce-windows32-20101007.zip) from sourceforge and unzip it.
--- In order to run the 64-bit version, a DLL contained in the bin/ folder of mingw-w64-gcc-4.6.3-runtime-2.0.1-shared-ada-20120322.7z .
-- Linux
--- Download the source code (reduce-algebra-20101007.tar.bz2) from sourceforge and create an executable.
--- To circumvent the performance bottleneck caused by 'sleep' in socket communicatino, apply the following patch:
+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:
>
+ wget http://jaist.dl.sourceforge.net/project/reduce-algebra/reduce-algebra-20101007.tar.bz2
+ bzip2 -dc reduce-algebra-20101007.tar.bz2 | tar xvf -
+ cd reduce-algebra-20101007/
+ Copy filepatch.txt to reduce-algebra-20101007/
+ patch -d csl/cslbase/ < patch.txt
+ ./configure --with-csl --without-gui
+ make
./hylagi <program_path> [<options>] ~
<
--- an executable file will be built in /cslbuild/[OS-name]/csl/reduce .
+ How to run Hyrose with REDUCE
-- The shellscript sr.sh in the directory of the HydLa executable will invoke Hyrose as well as RECUDE.
-- Set the path of the REDUCE executable in the [REDUCE_PATH] field.
-- In Windows, invoke Hyrose under Cygwin.
--- For example, if REDUCE is unzipped at C:\reduce-i686-pc-windows-20101007\, [REDUCE_PATH] should be set to /cygdrive/c/reduce-i686-pc-windows-20101007/.
--- Example
> sh sr.sh examples/bouncing_particle.hydla -t 1
-- 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
<
--- [Appendix] Since the REDUCE server on Linux supports asynchronous communication, Hyrose can be invoked without sr.sh if the REDUCE server is running background.
--- How to invoke a server (example):
> [REDUCE_PATH]/reduce -w -F- &
-- "-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)
- 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$.
