* Hyroseとは [#y08cb072]
- HydLaプログラムのシミュレータである
- 数式処理を用いて, 誤差のないシミュレーションを可能とする
- 記号実行を可能として、パラメータを含むシステムを扱える
- パラメータによってシステムの振る舞いが定性的に異なる際の場合分けが可能である
- 有限時間に対する性質検証が可能である
- HydLaプログラムに対するシミュレーション, パラメータ解析, 有界モデル検査を高信頼に行うことが可能である
* インストール方法 [#cee9a99e]
[[Download]]ページからHyroseをダウンロード後, 数式処理ソフトウェアの利用方法に書いてある準備を行えば使用可能
* 使用法 [#z98de6fd]
** オプションと意味 [#ub30e628]
-h [--help] : Hyroseのヘルプを表示する
--version : Hyroseのバージョンを表示する
-d [--debug] : Hyroseのデバッグモードを有効にする
--parse_only : HydLaプログラムのパースのみを行う
--dump_parse_tree : HydLaプログラムのパース結果を出力する
--dump_module_set_list : HydLaプログラムの解候補となるモジュール集合の集合をリスト型式で出力する
--dump_relation_graph : HydLaプログラムの変数や制約の関係を出力する
--dump_in_progress : 各フェーズの計算が終わるごとにそのフェーズの結果の出力する
(本来は, シミュレーションが全て終了したときに結果が表示される)
--search arg (=d) : 全解探索時の探索方法を指定する
d : 深さ優先探索(Depth First Search) (デフォルト)
b : 幅優先探索(Breadth First Search)
-s [ --solver ] arg (=m) : バックエンドで使用するソルバを指定する
m : Mathematica
r : Reduce
--nd : 全解探索を有効にする(有効にしない場合, 場合分けが発生すると自動的に一つの場合(Case)が選択されそのケースについてのシミュレーションが進んでいく. 選択されなかった場合(Case)については場合分けが発生した時点までのシミュレーション結果と共に選択されなかったと表示される)
--in : インタラクティブモードを有効にする
--find_unsat_core : unsat coreを発見する
--use_unsat_core : unsat coreを用いたシミュレーションを行う
--ha : HydLaプログラムのHA(Hybrid Automaton)への変換を行う
--hs : HA(Hybrid Automaton)を用いたシミュレーションを行う
--parallel : 並列処理モードを有効にする
--pn arg (=2) : 並列処理の個数を設定する(デフォルトは2)
--reuse : シミュレーションにおける再利用を有効にする
--tm arg (=n) : 時間計測を行う. 引数はn(時間計測を行わない)とs(標準の出力型式で時間計測結果を表示する)
time measurement:
n - not measured
s - output standard format
c - output csv format
--csv arg csv file name for "--tm c":
empty - standard out
-O [ --optimization-level ] arg (=0) optimization level:
--analysis_mode arg analysis mode
empty - don't analyze constraint
use - use analysis file
output - analyze constraint and output to file
simulate - analyze constraint and simulate using analysis result
--analysis_file arg analysis file name
empty - standard out or standard in
-o [ --output_name ] arg file name for hydat output (if empty ./hydat/<program_name>.hydat)
-t [ --time ] arg simulation time for the model
empty: infinity
--ignore_warnings ignore warnings.
Warnings are mainly caused by errors of calculations
-p [ --phase ] arg (=-1) simulation limit for number of phases in model
positive value: number of phases
negative value: infinity
-a [ --approx ] simulate with approximation
-c [ --change ] change next PP time
-e [ --epsilon ] arg (=-1) epsilon mode
--timeout_calc arg (=-1) timeout for each calculation in backend(second)
negative or zero - infinity
--fail_stop stop all simulation cases when assertion fails
--math_name arg (=math) name of mathematica command
* 数式処理ソフトウェアの利用方法 [#s7a4a3b3]
- 現在のHyroseでは, 求解時に数式処理ソフトウェアとしてMathematicaやREDUCEを用いている
- これらを利用するために, それぞれ下記の準備を行い, 使用するソフトウェアをsolverオプションにて指定する
** Mahtematica [#ad3804e7]
- バージョン7以降のインストールが必要(8を推奨)
-- Mathematica8でないとエラーの発生する例題も確認されている(2011/12/21)
- Mathematicaのパスが通っていれば使用可能
-- 具体的には, math コマンドによってMathematicaが起動可能であればよい
--- math コマンド以外で起動する場合には, 「--mathlink」オプションによってlinkname後のコマンド名をmathから該当名に変更すればよい
--- GUI環境なら, 起動するMathematicaの実行ファイルを毎回指定することができる
** Reduce [#bddfe27a]
- 20101007版(それ以降には未対応)のインストールが必要
- REDUCEを数式処理ソルバとして使用する場合, 以下の手順に従う
+ REDUCEのインストール手順
-- Windows系OS
--- sourceforgeのサイトからソースコード(reduce-windows64-20101007.zip または reduce-windows32-20101007.zip)をダウンロードして解凍する
--- (64bit版のREDUCEを実行するにはmingw-w64-gcc-4.6.3-runtime-2.0.1-shared-ada-20120322.7zのbin/ のDLLが必要)
-- linux系OS
--- sourceforgeのサイトからソースコード(reduce-algebra-20101007.tar.bz2)をダウンロードして, 実行ファイルを作成する
--- ソケット通信時にsleep関数が原因のボトルネックが存在するため, パッチを当てて対処する必要がある
>
+ 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/
+ (reduce-algebra-20101007/ディレクトリに filepatch.txt をコピー)
+ patch -d csl/cslbase/ < patch.txt
+ ./configure --with-csl --without-gui
+ make
<
--- このmakeによって/cslbuild/[各OSの名前]/csl/reduce に実行ファイルが生成される
+ REDUCEによるHyrose実行手順
-- hydla実行ファイルと同じディレクトリの sr.sh を使って, REDUCEの起動, 終了と共にHyroseを実行する
-- [REDUCE_PATH]に生成したreduceのパスを設定すること
-- windows系の場合, cygwinを使って実行する
--- 例としてREDUCEの解凍場所を「C:\reduce-i686-pc-windows-20101007\」にした場合, [REDUCE_PATH]には「/cygdrive/c/reduce-i686-pc-windows-20101007/」と書く
--- 実行例
> sh sr.sh examples/bouncing_particle.hydla -t 1
<
--- [補足] linux版のREDUCEサーバは非同期通信に対応しているため、裏で起動しておけばsr.shなしでhyroseを実行出来る
--- サーバ起動例
> [REDUCE_PATH]/reduce -w -F- &
<