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

- 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.

* 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("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 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 --nd < --- [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. -- "--nd" 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$.