- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* Hyroseとは [#y08cb072]
- HydLaプログラムのシミュレータである
- 数式処理を用いて, 誤差のないシミュレーションを可能とする
- 記号実行を可能として、パラメータを含むシステムを扱える
- パラメータによってシステムの振る舞いが定性的に異なる際の場合分けが可能である
- 有限時間に対する性質検証が可能である
- HydLaプログラムに対するシミュレーション, パラメータ解析, 有界モデル検査を高信頼に行うことが可能である
* インストール方法 [#cee9a99e]
[[Download]]ページからHyroseをダウンロード後, 数式処理ソフトウェアの利用方法に書いてある準備を行えば使用可能
* 使用法 [#z98de6fd]
- HyroseにHydLaプログラムを入力すると, シミュレーション結果が出力される
- 出力は, 標準出力への出力の他にJSON形式でも出力される
- 出力されるファイル名は, <プログラム名>.hydatという形となる
** オプションと意味 [#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)については場合分けが発生した時点までのシミュレーション結果と共に選択されなかったと表示される)
--nd : 全解探索を有効にする
有効にしない場合, 場合分けが発生すると自動的に一つの場合(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
--tm arg (=n) : 時間計測を行う.
n : 時間計測を行わない(デフォルト)
s : 時間計測を行い, 標準の出力型式で時間計測結果を表示する
c : 時間計測を行い, csv形式で時間計測結果を表示する
--csv arg csv file name for "--tm c":
empty - standard out
--csv arg : 時間計測を行いcsv形式で出力する(--tm c)の場合において, 出力するcsvファイルの名前を指定する
このオプションが空の場合, 標準出力に出力する
-O [ --optimization-level ] arg (=0) optimization level:
-O [ --optimization-level ] arg (=0) : 最適化のレベルを指定する(デフォルトは0)
--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_mode arg : 分析モードを有効にする
empty : 制約の分析を行わない
use : 分析ファイルを使用する
output : 制約を分析し, 結果をファイルに出力する
simulate : 制約を分析し, 分析結果をシミュレーションに利用する
--analysis_file arg analysis file name
empty - standard out or standard in
--analysis_file arg : 分析ファイルを指定する
empty : 標準出力や標準入力となる
-o [ --output_name ] arg file name for hydat output (if empty ./hydat/<program_name>.hydat)
-o [ --output_name ] arg : hydat形式でシミュレーション結果を出力する際のファイル名を指定する
empty : ./hydat/<program_name>.hydat に出力される
-t [ --time ] arg simulation time for the model
empty: infinity
-t [ --time ] arg : シミュレーションの時間制限を指定する(Max Time)
empty : 時間の制限はない
--ignore_warnings ignore warnings.
Warnings are mainly caused by errors of calculations
--ignore_warnings : 主に計算において起きた警告を無視する
-p [ --phase ] arg (=-1) simulation limit for number of phases in model
positive value: number of phases
negative value: infinity
-p [ --phase ] arg (=-1) : シミュレーションのフェーズ制限を指定する(Max Phase)
positive value : そのフェーズまでのシミュレーションとなる
negative value : フェーズの制限はない
-a [ --approx ] simulate with approximation
-a [ --approx ] : アフィン近似を用いたシミュレーションを行う
-c [ --change ] change next PP time
-c [ --change ] : 特定の場合に次の離散変化時刻を変更可能にする
-e [ --epsilon ] arg (=-1) epsilon mode
-e [ --epsilon ] arg (=-1) : epsilonモードを有効にする
--timeout_calc arg (=-1) timeout for each calculation in backend(second)
negative or zero - infinity
--timeout_calc arg (=-1) : バックエンドの計算において, timeoutを指定する
negative or zero : timeoutの制限はない
--fail_stop stop all simulation cases when assertion fails
--fail_stop : assert違反が起きた場合に, 全てのシミュレーションを停止する
--math_name arg (=math) name of mathematica command
--math_name arg (=math) : Mathematicaのコマンドを指定する
* 数式処理ソフトウェアの利用方法 [#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- &
<
